bedrock.prelude.addr

bedrock.prelude.avl

• • Canonicalize proofs

bedrock.prelude.base

• • Missing from Coq's stdlib
• Small extensions to stdpp.base
  • Monads
  • Pairwise disjointness
  • Typeclass operations
  • Comparisons

bedrock.prelude.bitsN

bedrock.prelude.bool

bedrock.prelude.bytestring

bedrock.prelude.bytestring_core

bedrock.prelude.compare

• • Generic comparison

bedrock.prelude.dummy

bedrock.prelude.error

• • Errors

bedrock.prelude.fin

• Inductive-like interface.

bedrock.prelude.fin_map_dom

bedrock.prelude.fin_maps

bedrock.prelude.fin_sets

• Small extensions to stdpp.fin_sets.

bedrock.prelude.finite

bedrock.prelude.functions

bedrock.prelude.gmap

bedrock.prelude.hw_types

bedrock.prelude.interrupts

• Configurations of the interrupt lines attached to devices
• The IntConfig value before the first assign_int
• Interrupt signals generated by devices

bedrock.prelude.lens

bedrock.prelude.letstar

• Syntax for straight-line CPS function calls

bedrock.prelude.list

• Small extensions to stdpp.list.
  • Quantifiers and equivalence
  • Type-level list quantifier
  • Teach set_solver to reason about more list operations, similarly to set
  • Basic theory about the ap/<*> combinator for lists.

bedrock.prelude.list_numbers

• - x - x
• - 0 - x
• - x - 0
• - bool_decide (x - y = 0) (it becomes bool_decide (x = y))
• - x + 0
• - 0 + x
• - x `min` x
• - x `min` y = x
• - x `min` y = y
• - x `max` x
• - x `max` y = x
• - bool_decide (R x x) for any reflexive relation R
• - bool_decide (x < x)
• Those lemmas, in combination with definition by case of insertZ and lookupZ,
• help normalize the list indices and conditions about list indices.

bedrock.prelude.listset_nodup

bedrock.prelude.named_binder

bedrock.prelude.notations

bedrock.prelude.numbers

• Small extensions to stdpp.numbers.
• Natural numbers nat
• Facts about comparison
• Positives positive
• Natural numbers N
• Integers
  • Alignment to powers of two
  • N_to_Qp

bedrock.prelude.option

• Theory for is_Some_proj
• Lift basic relation typeclasses from RelationClasses
• Lift bundled relation typeclasses from RelationClasses
• Lift basic relation typeclasses from stdpp.base
• Lift bundled relation typeclasses from stdpp.base
  • Define a partial equivalence relation from an observation

bedrock.prelude.page

bedrock.prelude.parsec

bedrock.prelude.prelude

bedrock.prelude.propset

• Small extensions to stdpp.sets.

bedrock.prelude.relations

bedrock.prelude.reserved_notation

• • Monads
  • Iris big ops
• We stick with the levels and associativity used in Iris' big ops
• notation. Compared to that notation, we:
• - add an optional break and indentation after binders
• (significantly improving readability)
• - use **, /\, \/, |-> instead of ∗, ∧, ∨, ↦
• (slightly improving typeability)
• TODO: Upstream the formatting box changes.
  • Comparisons

bedrock.prelude.sets

• Small extensions to stdpp.sets.

bedrock.prelude.stdpp_ssreflect

bedrock.prelude.sts

• Mapping event types
• Hiding internal events
• Binary parallel composition

bedrock.prelude.sum

bedrock.prelude.tc_cond_type

bedrock.prelude.telescopes

bedrock.prelude.under_rel_proper

bedrock.prelude.wrap

bedrock.prelude.axioms.funext

bedrock.prelude.elpi.basis

bedrock.prelude.elpi.derive

bedrock.prelude.elpi.derive_test

bedrock.prelude.elpi.derive.bitset

bedrock.prelude.elpi.derive.common

bedrock.prelude.elpi.derive.countable

bedrock.prelude.elpi.derive.eq_dec

bedrock.prelude.elpi.derive.finite

bedrock.prelude.elpi.derive.finite_type

bedrock.prelude.elpi.derive.inhabited

bedrock.prelude.elpi.derive.lens

bedrock.prelude.tactics.base_dbs

• This file declares some Dbs for our developments.

bedrock.prelude.tactics.proper

• Tactics for Proper instances

bedrock.prelude.tactics.telescopes

• Telescopes