The operation’s intended meaning and laws.
Public proof record build
Authoring meanings
Write the relation first. Choose the machine afterward.
A dregg program says which witnesses, inputs, and state transitions count as one semantic operation. Lean is the source of meaning; specialized provers and fast systems code are implementations of that meaning.
01
The authoring path
Meaning descends. Evidence comes back up.
A guard, parser, rewrite, optimizer, or transition supplies the natural semantic grain.
Arithmetic constraints and public lanes are generated from the formal object.
Untrusted implementations construct witnesses and run the heavy machinery.
The verified relation becomes authorized shared state.
A fast implementation is allowed to be clever. Its accepted language is not allowed to quietly differ from the authored one.
02
Predicate languages
Ask useful questions about a guard before deploying it.
A guard is a regular expression whose leaves are predicates over values rather than characters. Symbolic derivatives, minterm covers, and an adaptive similarity fixpoint decide emptiness and language equivalence over the supported infinite-alphabet fragment.
Field pins and enum membership
symEq, digEq, and symMemberOf compose under negation, conjunction, disjunction, and regular operations.
Policy lists
allOf and anyOf fold into the decided boolean fragment with a semantics proof.
Owner match
A single digFieldEq algebra decides owner-match, mismatch, and contradiction with correlated witnesses.
Mixed correlations and arithmetic
Mixed cross-field pins, reactive fieldEqField, and general StateConstraint/LIA atoms remain outside the general runnable fixpoint.
03
Certificates as programs
Parsing, rewriting, and replay share one bridge.
imported
DFA and VPA certificates
Finite and visibly pushdown recognizers produce derivation objects checked through the common certificate relation.
circuit path
Dyck and CFG parsing
A bounded stack trace proves a genuine derivation and connects the emitted circuit to Lean replay.
semantic history
Hypergraph rewriting
Root-linked steps carry a genuine match-driven replacement history or expose a commitment collision.
bounded primitive
Private graph reduction
A hidden rule, match, substitution, and context can prove a bounded replacement. Full DPO conditions and a scalable authenticated heap remain beyond the present leaf.
04
Choosing a proof organ
Not every meaning wants the same verifier.
Cells and predicates
Use the common executor for capability-gated state transitions and compact policy checks.
Custom VK / AIR
Use a dedicated Lean-authored transition relation for a board game, parser, optimizer, or cryptographic verifier.
Hiding, FHE, and MPC
Choose proof privacy, encrypted evaluation, or distributed custody according to who may see which witness at which stage.