Module fixpoint_encoding

Expand description

Encoding of the refinement tree into a fixpoint constraint.

Modules§

Answer
ConstDeps
ConstEnv 🔒
ExprEncodingCtxt
FixpointCheckError
FixpointCtxt
FunEnv 🔒: Determines which Flux functions are uninterpreted in the constraint generated for an item.
KVarDecl 🔒
KVarEncodingCtxt 🔒: The purpose of a KVarEncodingCtxt is to mark which kvars appear in the constraint, so we only declare those in fixpoint. Kvars may not be in the constraints because we optimized them away.
KVarGen
KvarSolutionTrace
LocalVarEnv 🔒: Environment used to map from rty::Var to a fixpoint::LocalVar.
ParsedResult
SexpParseCtxt 🔒
SolutionTrace: A very explicit representation of Solution for debugging/tracing/serialization ONLY.
SortDeps
SortEncodingCtxt: Keep track of all the data sorts that we need to define in fixpoint to encode the constraint.
SuggestionCtxt 🔒
TagIdx

bv_size_to_fixpoint 🔒
const_to_fixpoint 🔒
crate_rank 🔒: The position of krate in a topological order of all crates, i.e., every crate comes after all the crates it depends on. The local crate goes last.
lean_task_key: Returns the cache key used for a function-body lean query. It is distinct from the key of the corresponding fixpoint query, so a lean entry is never mistaken for a fixpoint result.
parse_data_ctor 🔒
parse_data_proj 🔒
parse_global_var 🔒
parse_kvid 🔒
parse_local_var 🔒
parse_param 🔒
parse_weak_kvar 🔒
parse_wkvars 🔒
record_lean_task 🔒: Records that the lean files for the task with the given hash have been generated. The proof starts out as LeanStatus::Invalid and is marked as valid once it has been checked.

ClosedSolution
ConstMap 🔒
FixQueryCache
FixpointSolution
FunDeclMap
InterpretedConst: A type for rust constants that have a concrete interpretation
PossibleSolutions
Solution: A type to represent Solutions for KVars