Cairn.Claims.Registry
lean/Cairn/Claims/Registry.lean
The claim registry: an environment extension holding one entry per claim declared by the
claim commands, in this module and every module it imports. The commands consult it for the
compile-time checks; lake exe ledger and lake exe claims read it from the imported
environment.
Compile time only (imports Lean); see Cairn.Claims for why that matters.
Imports Lean, Cairn.Claim
Structures 2
Entry : Type
One claim as the registry records it.
info : ClaimInfo
scope : StringThe package scope the claim was declared in (cairn.claims.scope).
ns : Lean.NameThe namespace the claim was declared in; claims% and moves% collect by it.
decl : Lean.NameinfoDecl : Lean.NameThe ClaimInfo constant.
module : Lean.Namestatement : Array Lean.NameDeclarations whose definitions are the claim's formal statement. The ledger hashes them (and what they unfold to in Cairn's own modules) to notice a change of meaning.
evidence : Array (String × Lean.Name)
The evidence: a role (sound press, reaches, step, …) and the theorem proving it.
triggers : Array StringMoves: the triggers answered, and whether controls are keyed.
keyed : Boolpasses : Array ClaimId
Flows: the claim ids of the moves the witness passes through, in order.
machine : Option Lean.NameFlows and invariants: the machine they are stated against.
check : Option StringAssumptions: the runnable check that gathers evidence for it (a check name in the trusted
fuzzer's report, build/fuzz/trusted.json; docs/fuzz.md, "Trusted base").
State : Type
clashes : Array (Entry × Entry)
Pairs of imported claims with the same id (modules that never import each other).
here : Array Entry
Entries declared in this module, in order.
Definitions 14
scope : Lean.Option StringThe package whose claims a module declares: ^301 in a module built with scope yap is the
claim yap^301. Ids are unique within a scope, never across scopes, so a package's ids are its
own and the ids of the packages it depends on can't collide with them. Set once per package, in
its lakefile: leanOptions := #[⟨weak.cairn.claims.scope, "yap"⟩] (weak., because Lake passes it to every module, including those that don't import the claim commands). Cairn's own modules use the default, cairn`.
scopedRef (scope : String) (id : ClaimId) : String
A claim's full name, scope^N (cairn^1005, yap^301).
name : ClaimKind → String
ofName? : String → Option ClaimKind
ref (e : Entry) : String
scope^N.
label (e : Entry) : String
add (st : State) (e : Entry) : State
registry : Lean.SimplePersistentEnvExtension Entry State
sealedExt : Lean.EnvExtension (Lean.NameSet × Lean.NameSet)
Namespaces collected in this module by moves% (first) and claims% (second). A move
declared in the first afterwards would never be dispatched, and a claim declared in the second
would be missing from the app's claims, so the commands refuse both.
lt (a b : Entry) : Bool
Order by scope, then id.
entries (env : Lean.Environment) : Array Entry
Every claim in every scope, by scope and then id.
lookup? (env : Lean.Environment) (scope : String) (id : ClaimId) : Option Entry
clashes (env : Lean.Environment) : Array (Entry × Entry)
allEntries (env : Lean.Environment) : Array Entry
Every entry, including both sides of any clash, for tools that report on the whole set.
Instances 2
instInhabitedEntry : Inhabited Entry
instInhabitedState : Inhabited State