skylabs.prelude.addr
skylabs.prelude.avl
skylabs.prelude.base
skylabs.prelude.bitsN
skylabs.prelude.bool
skylabs.prelude.bytestring
skylabs.prelude.bytestring_core
skylabs.prelude.compare
skylabs.prelude.dummy
skylabs.prelude.error
skylabs.prelude.fin
skylabs.prelude.fin_map_dom
skylabs.prelude.fin_maps
skylabs.prelude.fin_sets
skylabs.prelude.finite
skylabs.prelude.finite_prod
skylabs.prelude.fun_maps
skylabs.prelude.functions
skylabs.prelude.gmap
skylabs.prelude.hw_types
skylabs.prelude.interrupts
- Configurations of the interrupt lines attached to devices
- The IntConfig value before the first assign_int
- Interrupt signals generated by devices
skylabs.prelude.lens
skylabs.prelude.letstar
skylabs.prelude.list
skylabs.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.
skylabs.prelude.listset_nodup
skylabs.prelude.name
- Copyright (C) 2023 BlueRock Security, Inc.
- All rights reserved.
- SPDX-License-Identifier: LGPL-2.1 WITH BedRock Exception for use
- over network, see repository root for details.
skylabs.prelude.named_binder
skylabs.prelude.notations
skylabs.prelude.numbers
- Small extensions to stdpp.numbers.
- Natural numbers nat
- Facts about comparison
- Positives positive
- Natural numbers N
- Integers
skylabs.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
skylabs.prelude.page
skylabs.prelude.parray
skylabs.prelude.parsec
skylabs.prelude.prelude
skylabs.prelude.propset
skylabs.prelude.pstring
skylabs.prelude.pstring_string
skylabs.prelude.relations
skylabs.prelude.reserved_notation
- 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.