bedrock.lang.cpp

bedrock.lang.algebra.authset

• CMRA: Auth/frag splits on sets, with strengthening
• AuthSet.frag (s : propset A)
• AuthSet.auth (s : propset A)
• ✓ (AuthSet.frag s1 ⋅ AuthSet.auth s2) <-> s1 ⊆ s2; and
• AuthSet.frag s ~~> AuthSet.frag s' when s' ⊆ s (removing elements
  • Removing elements from a frag set is frame preserving.

bedrock.lang.algebra.base

bedrock.lang.algebra.big_op

• Big ops
  • set_seq
  • Powers and big ops
  • Powers encoded as big ops

bedrock.lang.algebra.coGset

• The union CMRA
• The disjoint union CMRA

bedrock.lang.algebra.dfrac_agree

bedrock.lang.algebra.excl_auth

• Extension to excl_auth

bedrock.lang.algebra.frac_auth

• Extension to frac_auth

bedrock.lang.algebra.gset_bij

bedrock.lang.algebra.list

bedrock.lang.algebra.monoid

• Powers in monoids

bedrock.lang.algebra.restrict

bedrock.lang.algebra.telescopes

bedrock.lang.base_logic.invariants

bedrock.lang.base_logic.iprop_invariants

bedrock.lang.base_logic.iprop_own

bedrock.lang.base_logic.iprop_prop

• iProp satisfies Ghostly and HasUsualOwn

bedrock.lang.base_logic.monpred_invariants

• • Internal model of invariants

bedrock.lang.base_logic.monpred_own

bedrock.lang.base_logic.mpred

bedrock.lang.base_logic.mpred_prop

• Mpred satisfies Ghostly and HasUsualOwn

bedrock.lang.base_logic.own_instances

bedrock.lang.base_logic.upred_entailsN

bedrock.lang.base_logic.lib.auth_set

• Spec building block: auth/frag propsets with weakening

bedrock.lang.base_logic.lib.mono_list

• Well-typed ghost state for mono list.

bedrock.lang.base_logic.lib.spectra

• Top-level theorem
• Singleton and Constructor Requesters/Committers

bedrock.lang.base_logic.lib.spectra_iprop

• Top-level theorem for iProp

bedrock.lang.base_logic.lib.spectra_mpred

• Top-level theorem for mpred

bedrock.lang.bi.ChargeCompat

bedrock.lang.bi.atomic1

bedrock.lang.bi.atomic_commit

• Atomic commits

bedrock.lang.bi.atomic_read

bedrock.lang.bi.atomic_update

• Small improvements to atomic updates

bedrock.lang.bi.atomic_update_properties

• Atomic accessors and atomic updates
  • Laterable assertions
  • Except at zero
• Atomic accessors
• Atomic updates

bedrock.lang.bi.big_op

• • Lists
  • Powers in BIs
• Avoid exotic goals like Timeless emp, Affine True when n a
• non-zero constructor.

bedrock.lang.bi.cancelable_invariants

bedrock.lang.bi.derived_laws

bedrock.lang.bi.embedding

• Composing embeddings

bedrock.lang.bi.entailsN

• Step-indexed entailment

bedrock.lang.bi.errors

bedrock.lang.bi.fractional

• Simple extensions to iris.bi.lib.fractional

bedrock.lang.bi.fupd_iff

• Bidirectional fancy updates

bedrock.lang.bi.includedI

• Internal inclusion

bedrock.lang.bi.invariants

• • Proof mode integration
  • Derived properties

bedrock.lang.bi.laterable

bedrock.lang.bi.linearity

bedrock.lang.bi.monpred

• • Discrete BI indices and discrete BI index elements

bedrock.lang.bi.monpred_entailsN

bedrock.lang.bi.na_invariants

bedrock.lang.bi.observe

• Observations

bedrock.lang.bi.only_provable

• Properties of only_provable.
• We don't register instances
• - @FromAffinely PROP [| P |] ⌜P⌝
• - @IntoAbsorbingly PROP ⌜P⌝ [| P |]
• as they would interact poorly with, e.g., iSplit, changing
• goals like [| P |] ** Q into subgoals involving bi_pure
• rather than only_provable.

bedrock.lang.bi.own

bedrock.lang.bi.prelude

• Notation for functions in the Iris scope. To upstream,
  • Big op notation

bedrock.lang.bi.prop_constraints

• Convenience wrappers for common PROP-constraint bundles

bedrock.lang.bi.spec

bedrock.lang.bi.split_andb

• Splitting and combining booleans on &&

bedrock.lang.bi.split_andb_tests

bedrock.lang.bi.split_frac

• Splitting and combining fractions
  • Operations on fractions
  • Splitting fractions
  • Combining fractions

bedrock.lang.bi.split_frac_tests

bedrock.lang.bi.telescopes

bedrock.lang.bi.wand_borrow

bedrock.lang.bi.weakly_objective

bedrock.lang.bi.spec.constant

• Spec building block: logical constants

bedrock.lang.bi.spec.contender_token

• Spec building block: Contender tokens

bedrock.lang.bi.spec.exclusive

• Spec building block: Exclusive tokens

bedrock.lang.bi.spec.frac_splittable

• Spec building block: fractional ownership

bedrock.lang.bi.spec.knowledge

bedrock.lang.bi.spec.nary_classes

bedrock.lang.cpp.code_notations

bedrock.lang.cpp.compile

bedrock.lang.cpp.logic

bedrock.lang.cpp.mparser

bedrock.lang.cpp.notations

bedrock.lang.cpp.parser

bedrock.lang.cpp.primitives

bedrock.lang.cpp.reserved_notation

bedrock.lang.cpp.semantics

bedrock.lang.cpp.specs

bedrock.lang.cpp.syntax

bedrock.lang.cpp.algebra.cfrac

• Const/mutable fractions
  • OFE
  • CMRA
  • Backwards compatibility

bedrock.lang.cpp.arith.builtins

bedrock.lang.cpp.arith.operator

• Semantics of arithmetic and pointer operators: support operators.

bedrock.lang.cpp.arith.types

bedrock.lang.cpp.arith.z_to_bytes

bedrock.lang.cpp.bi.cfractional

• Fractional predicates at type cQp.t
  • Properties of CFractional
  • Backwards compatibility
  • IPM instances
  • Observations from validity

bedrock.lang.cpp.bi.cfractional_tests

bedrock.lang.cpp.bi.spec

bedrock.lang.cpp.bi.split_cfrac

• Splitting and combining const/mutable fractional things
  • Operations on const/mutable fractions
  • Splitting const/mutable fractions
  • Combining const/mutable fractions

bedrock.lang.cpp.bi.split_cfrac_tests

bedrock.lang.cpp.bi.spec.cfrac_splittable

• Spec building block: const/mutable fractional ownership

bedrock.lang.cpp.bi.spec.typed

bedrock.lang.cpp.logic.arr

bedrock.lang.cpp.logic.atomics

bedrock.lang.cpp.logic.atomics_derived

bedrock.lang.cpp.logic.builtins

• • Wp Semantics for builtins
  • Endianness
  • Builtin functions

bedrock.lang.cpp.logic.call

bedrock.lang.cpp.logic.const

bedrock.lang.cpp.logic.core_string

bedrock.lang.cpp.logic.cptr

bedrock.lang.cpp.logic.cstring

• cstrings

bedrock.lang.cpp.logic.destroy

• • Destroying primitives
  • Invoking destructors
  • Destroying structures and unions
  • Arrays and values
  • Destroying temporaries

bedrock.lang.cpp.logic.dispatch

• reflecting virtual function dispatch in the logic.
• implementation and the downcast for this pointer.

bedrock.lang.cpp.logic.entailsN

bedrock.lang.cpp.logic.expr

• Semantics of expressions
• (expressed in weakest pre-condition style)
• Weakest pre-condition for expressions
• String Literals
• Unary Operators
• Binary Operators
• Casts
• Cderived2base
• of the "then" and "else" expressions (which must be the same).
• We express this with 4 rules, one for each of wp_lval,
• wp_operand, wp_xval, and wp_init.
• Function calls
• Member calls
• Operator Calls

bedrock.lang.cpp.logic.func

• • Weakest precondition of a constructor: Initial construction step.
  • Aggregate identity
  • Binding parameters
  • The weakest precondition of a function
  • The weakest precondition of a method
  • Weakest precondition of a constructor
  • Weakest precondition of a destructor

bedrock.lang.cpp.logic.heap_pred

bedrock.lang.cpp.logic.initializers

• • Default initilalization
  • Expression initialization

bedrock.lang.cpp.logic.layout

bedrock.lang.cpp.logic.mpred

bedrock.lang.cpp.logic.new_delete

• Weakest pre-condition for new and delete expressions
• The semantics of new and delete expressions (including their array forms)
• are *very* complex in C++. This is due to a litany of corner cases such as:
• - the need to pair allocation and de-allocation functions
• - the existance of placement new
• - the need to handle alignment as well as size.
• - the potential for padding bytes.
• - the potential to merge allocations. (BRiCk does not attempt to support this)
• NOTE It is important that these rules are sound, but less important that
• they are complete. When in doubt, we err on the side of caution and under-specify
• the behavior of various constructs.
• If you run into code that requires addditional semantic specification, please file
• an issue.
• <https://eel.is/c++draft/new.delete.placement1>.
• NOTE: placement <new> is more subtle than the rule described here
• because it can be used to construct an object over an existing
• object.
• the form delete p; - where p is a non-null pointer to an object whose
• most-derived destructor is defined in the current translation unit.

bedrock.lang.cpp.logic.object_repr

bedrock.lang.cpp.logic.operator

• Pointer comparison operators

bedrock.lang.cpp.logic.path_pred

bedrock.lang.cpp.logic.pred

• • Deducing pointer equalities

bedrock.lang.cpp.logic.pred_paradoxes

bedrock.lang.cpp.logic.raw

bedrock.lang.cpp.logic.rep

bedrock.lang.cpp.logic.rep_defs

• assert properties of the heap

bedrock.lang.cpp.logic.rep_proofmode

• Proof mode instances
• Instances for _at
• Instances for _offsetR
• Instances for pureR

bedrock.lang.cpp.logic.stmt

• Attribute Evaluation
• Expression Evaluation
• Declarations
• Blocks
• if
• while
• for
• do
• return
• break
• continue
• switch

bedrock.lang.cpp.logic.string

• cstrings and zstrings
  • Notes
• cstring.t and cstring.WF - Well Formed BS.ts (bytestrings) as a Carrier Type for C++ Strings
• cstring.R - Fixed Sized Strings
• cstring.bufR - Dynamic Sized Strings Backed by Fixed Sized Character Arrays

bedrock.lang.cpp.logic.translation_unit

bedrock.lang.cpp.logic.vbyte

bedrock.lang.cpp.logic.wp

• Regions
• prvalue
  • boolean operands
• xvalues
• Statements

bedrock.lang.cpp.logic.wp_notations

bedrock.lang.cpp.logic.z_to_bytes

bedrock.lang.cpp.logic.zstring

• zstrings

bedrock.lang.cpp.logic.heap_pred.aggregate

bedrock.lang.cpp.logic.heap_pred.any

bedrock.lang.cpp.logic.heap_pred.block

bedrock.lang.cpp.logic.heap_pred.everywhere

bedrock.lang.cpp.logic.heap_pred.least

bedrock.lang.cpp.logic.heap_pred.null

bedrock.lang.cpp.logic.heap_pred.prelude

bedrock.lang.cpp.logic.heap_pred.prim

• • reference_to

bedrock.lang.cpp.logic.heap_pred.simple

• • Object derivations
  • alignedR
  • derivationR

bedrock.lang.cpp.logic.heap_pred.tptsto

bedrock.lang.cpp.logic.heap_pred.uninit

bedrock.lang.cpp.logic.heap_pred.valid

bedrock.lang.cpp.logic.lib.agree

• Copyright (C) 2022 BlueRock Security, Inc.
• All rights reserved.
• SPDX-License-Identifier: LGPL-2.1 WITH BedRock Exception for use over network, see repository root for details.

bedrock.lang.cpp.logic.lib.auth_frac

• Copyright (C) 2022 BlueRock Security, Inc.
• All rights reserved.
• SPDX-License-Identifier: LGPL-2.1 WITH BedRock Exception for use over network, see repository root for details.

bedrock.lang.cpp.logic.lib.dfrac_agree

• Copyright (C) 2022 BlueRock Security, Inc.
• All rights reserved.
• SPDX-License-Identifier: LGPL-2.1 WITH BedRock Exception for use over network, see repository root for details.

bedrock.lang.cpp.model.inductive_pointers

bedrock.lang.cpp.model.inductive_pointers_utils

bedrock.lang.cpp.model.simple_pointers

bedrock.lang.cpp.model.simple_pointers_utils

bedrock.lang.cpp.model.simple_pred

bedrock.lang.cpp.mparser.expr

• • Template-only derived expressions emitted by cpp2v
  • Template-only derived variable declarations emitted by cpp2v

bedrock.lang.cpp.mparser.prelude

bedrock.lang.cpp.mparser.stmt

• • Template-only derived variable declarations emitted by cpp2v

bedrock.lang.cpp.mparser.tu

• • Template-only top-level declarations emitted by cpp2v

bedrock.lang.cpp.mparser.type

bedrock.lang.cpp.parser.decl

• Derived declaration helpers emitted by cpp2v

bedrock.lang.cpp.parser.expr

• Derived expressions emitted by cpp2v

bedrock.lang.cpp.parser.lang

bedrock.lang.cpp.parser.name

• Derived names emitted by cpp2v

bedrock.lang.cpp.parser.notation

bedrock.lang.cpp.parser.prelude

bedrock.lang.cpp.parser.reduction

bedrock.lang.cpp.parser.stmt

bedrock.lang.cpp.parser.type

• Derived types emitted by cpp2v

bedrock.lang.cpp.semantics.bswap

bedrock.lang.cpp.semantics.builtins

bedrock.lang.cpp.semantics.cast

• • Primitive Conversions

bedrock.lang.cpp.semantics.cast_operator

• • Binary Operator Static Semantics

bedrock.lang.cpp.semantics.characters

bedrock.lang.cpp.semantics.dispatch

bedrock.lang.cpp.semantics.genv

• global environments
  • One Definition Rule

bedrock.lang.cpp.semantics.heap_types

bedrock.lang.cpp.semantics.intensional

bedrock.lang.cpp.semantics.operator

• Operator semantics
• Unary Operators
• Binary Operators
  • Arithmetic Operators
  • bitwise operators
  • Shifting Operators
  • comparison operators

bedrock.lang.cpp.semantics.promotion

• Type-level semantics of type promotions
  • Integral Promotion
  • Arithmetic Promotion

bedrock.lang.cpp.semantics.ptrs

• • Allocation IDs.
• Pointers.
• Pointer offsets.
  • Concrete pointer offsets.
  • offset Congruence
  • ptr Congruence
  • same_address lemmas
  • same_address_bool lemmas
  • same_alloc lemmas

bedrock.lang.cpp.semantics.sub_module

• Sub-module
• Definitions for decidability
  • Inclusion of types (GlobDecl)
  • Inclusion of ObjValue
  • Inclusion on translation_unit
• Decidability

bedrock.lang.cpp.semantics.subtyping

bedrock.lang.cpp.semantics.types

• sizeof
• alignof

bedrock.lang.cpp.semantics.val_wrap

bedrock.lang.cpp.semantics.values

• Raw bytes
• Values
  • Notation wrappers for val

bedrock.lang.cpp.specs.arg_errors

bedrock.lang.cpp.specs.classy

bedrock.lang.cpp.specs.cpp_specs

bedrock.lang.cpp.specs.elaborate

bedrock.lang.cpp.specs.functions

• Wrappers to build function_spec from a WithPrePost
• this pointer needs to be adjusted before a call.

bedrock.lang.cpp.specs.spec_notations

bedrock.lang.cpp.specs.wp_spec_compat

bedrock.lang.cpp.syntax.compare

• • Name maps

bedrock.lang.cpp.syntax.core

• • Function types
  • Templates
  • Function names and qualifiers
  • Atomic names
  • Structured names
  • Types
  • Expressions
  • Casts
  • Notations
  • C++ with structured names
  • Derived forms
  • Dependent names, types, and terms

bedrock.lang.cpp.syntax.decl

• • Type Declarations
  • Value Declarations

bedrock.lang.cpp.syntax.expr_notations

bedrock.lang.cpp.syntax.extras

bedrock.lang.cpp.syntax.handler

• Handlers for simple AST traversals
  • Basic handlers

bedrock.lang.cpp.syntax.mcore

• • C++ with templates

bedrock.lang.cpp.syntax.mtraverse

• Traversals on template language syntax

bedrock.lang.cpp.syntax.mtyped

bedrock.lang.cpp.syntax.name_notation

bedrock.lang.cpp.syntax.namemap

• • Name maps

bedrock.lang.cpp.syntax.notations

bedrock.lang.cpp.syntax.overloadable

• • Unary, dependent expression constructor names
  • Binary, dependent expression constructor names

bedrock.lang.cpp.syntax.preliminary

• Type Preliminaries
  • Type qualifiers
  • Calling Conventions
  • Function Arities, i.e. variadic functions or not
  • Character types
  • Integer types
  • Floating point types
• Expression Preliminaries
  • Evaluation Order
  • Atomic Builtins
  • Builtins
  • Dispatch type, i.e. virtual or static
  • Value categories
  • The way an operator call is desugared

bedrock.lang.cpp.syntax.prelude

bedrock.lang.cpp.syntax.pretty

bedrock.lang.cpp.syntax.stmt

bedrock.lang.cpp.syntax.stmt_notations

bedrock.lang.cpp.syntax.supported

bedrock.lang.cpp.syntax.templates

• • Template pre-instances
  • Template instances
  • Templated values
  • Template TUs

bedrock.lang.cpp.syntax.translation_unit

• • Type Declarations
  • Value Declarations
  • Initializers
  • Aliases
  • Translation units

bedrock.lang.cpp.syntax.type_notations

bedrock.lang.cpp.syntax.typed

bedrock.lang.cpp.syntax.types

• • Qualifier normalization
  • Smart constructors
  • Erasing qualifiers
  • Qualifier simplification tactic
  • Type normalization
  • Qualifier-aware type operations
  • Heap Types

bedrock.lang.cpp.syntax.typing

bedrock.lang.cpp.syntax.untemp

• Converting untemplated code between lang.temp and lang.cpp

bedrock.lang.cpp.syntax.name_notation.parser

• • A parser for C++ names.

bedrock.lang.cpp.syntax.name_notation.printer

bedrock.lang.cpp.syntax.name_notation.test_cases

bedrock.lang.cpp.syntax.name_notation.test_roundtrip

bedrock.lang.proofmode.fancy_updates

bedrock.lang.proofmode.own_obs

• Observations from ownership
• Planning

bedrock.lang.proofmode.proofmode

bedrock.lang.si_logic.algebra

• Internal properties of CMRAs

bedrock.lang.si_logic.bi