This file defines the Cedar encoder, which translates a list of boolean Terms into a list of SMT assertions. Term encoding is trusted.

We will use the following type representations for primitive types:

• TermType.bool: builtin SMT Bool type
• TermType.string: builtin SMT String type
• TermType.bitvec n: builtin SMT (_ BitVec n) type

We will represent non-primitive types as SMT algebraic datypes:

• TermType.option T: a parameterized SMT algebraic datatype of the same name, and with the constructors (some (val T)) and (none). For each constructor argument, SMTLib introduces a corresponding (total) selector function. We will translate Term.some nodes in the Term language as applications of the val selector function.
• TermType.entity E: we represent Cedar entities of entity type E as values of the SMT algebraic datatype E with a single constructor, (E (eid String)). Each entity type E gets an uninterpreted function f: E → Record_E that maps instances of E to their attributes. Similarly, each E gets N uninterpreted functions g₁: E → Set E₁, ..., gₙ: E → Set Eₙ that map each instance of E to its ancestor sets of the given types, as specified by the memberOf relation in the schema.
• TermType.Record (Map Attr TermType): we represent each record term type as an SMT algebraic datatype with a single constructor. The order of arguments to the constructor (the attributes) is important, so we fix that to be the lexicographic order on the attribute names of the underlying record type. We use the argument selector functions to translate record.get applications. We can't use raw Cedar attribute names for argument names because they may not be valid SMT identifiers. So, we'll keep a mapping from the attribute names to their unique SMT ids. In general, we'll name SMT record types as "R<i>" where <i> is a natural number and attributes within the record as "R<i>a<j>", where <j> is the attribute's position in the constructor argument list.

Similarly to types and attributes, all uninterpreted functions, variables, and Terms are mapped to their SMT encoding that conforms to the SMTLib syntax. We keep track of these mappings to ensure that each Term construct is translated to its SMT encoding exactly once. This translation invariant is necessary for correctness in the case of record type declarations, UF names, and variable names; and it is neccessary for compactness in the case of terms. In particular, the resulting SMT encoding will be in A-normal form (ANF): the body of every s-expression in the encoding consists of atomic subterms (identifiers or literals).

structure Cedar.SymCC.EncoderState : Type

• terms : Batteries.RBMap Term String fun (x1 x2 : Term) => compareOfLessAndEq x1 x2
• types : Batteries.RBMap TermType String fun (x1 x2 : TermType) => compareOfLessAndEq x1 x2
• uufs : Batteries.RBMap UUF String fun (x1 x2 : UUF) => compareOfLessAndEq x1 x2
• enums : Batteries.RBMap Spec.EntityType (List String) fun (x1 x2 : Spec.EntityType) => compareOfLessAndEq x1 x2

def Cedar.SymCC.instReprEncoderState.repr : EncoderState → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Cedar.SymCC.instReprEncoderState : Repr EncoderState

Equations

• Cedar.SymCC.instReprEncoderState = { reprPrec := Cedar.SymCC.instReprEncoderState.repr }

def Cedar.SymCC.Encoder.enumId (E : String) (n : Nat) : String

Equations

• Cedar.SymCC.Encoder.enumId E n = toString E ++ toString "_m" ++ toString n

def Cedar.SymCC.Encoder.smtLibMaxCodePoint : Nat

The maximum Unicode code point supported in SMT-LIB 2.7. Also see num_codes in cvc5: https://github.com/cvc5/cvc5/blob/b78e7ed23348659db52a32765ad181ae0c26bbd5/src/util/string.h#L53

Equations

• Cedar.SymCC.Encoder.smtLibMaxCodePoint = 196607

def Cedar.SymCC.Encoder.encode (ts : List Term) (εnv : SymEnv) (produceModels : Bool := false) : SolverM EncoderState

Once you've generated Asserts with one of the functions in Verifier.lean, you can use this function to encode them as SMTLib assertions.

To actually solve these SMTLib assertions, you want to combine this encode action with other SolverM actions, such as Solver.check-sat at a minimum.

Then you can run any SolverM action act with act |>.run solver, where solver is a Solver instance you can construct using functions in Solver.lean.

Note that encode itself first resets the solver in order to define datatypes etc.

Equations

• One or more equations did not get rendered due to their size.