Guards: one predicate algebra, four polarities

Everything that constrains a turn is the same kind of object: a decidable predicate over the proposed step. dregg calls this algebra Pred, and it shows up in four polarities that are usually four separate mechanisms in other systems:

• a caveat — imposed on delegated power ("this token only works before Friday, only on slot 3");
• a program constraint — maintained on yourself ("my expiry slot is monotone; my committee root is immutable");
• a precondition — required of a turn ("only if the witness hash matches the commitment");
• an intent demand — wanted of the world ("I will sign whatever turn gives me ≥ N of asset A").

One algebra, four places to stand. A predicate is either first-party (decidable right now against the old/new state) or witnessed (a registered verifier discharges it — a third-party discharge, a range proof, a zero-knowledge statement). The same predicate the executor evaluates is compiled to circuit obligations, so what you can install and what the proof enforces are one mechanism.

The constraint grammar

Cell programs are built from this constraint vocabulary — each kind a small, decidable shape over the cell's slots:

Beyond single-slot shapes, the relational closure admits any affine relation over the post-state (head ≤ tail + capacity, Σ slots = const) as the same Pred object — no new atom per shape (Authority/RelationalClosure.lean, e.g. ofFieldLteOther_eq). Bounded quantifiers compile down to the same closure with a proven constraint budget (QuantifiedPredicate.compile_sound, andFold_budget).

The coordination dial

Guards carry a price tag, and the system computes it rather than hiding it. Two concurrent turns can merge without coordination exactly when their guards are confluence-stable — the invariant survives merging independently-taken steps. A guard that is not confluence-stable forces ordering: it is the system telling you that what you asked for costs consensus. The classifier is a theorem, not advice:

• ConfluenceClassifier.keeps_iff_coordinationFree — a guard preserves confluence iff it runs coordination-free;
• monotone_keeps — monotone thresholds are free;
• bounded_forces_ordering — upper bounds force ordering.

The disclosure dial

The second dial is how much a guard reveals while being checked. The principle: what the proof does not need, it does not ask to see. The ladder, from most to least disclosed:

• cleartext — the predicate reads the values directly;
• committed — values live behind Pedersen commitments; conservation checks homomorphically without opening them (PrivatePredicate.private_conservation_checks_homomorphically, committed_iff_cleartext — committed and cleartext judgments agree);
• range-proved — only the bound is disclosed, not the value (RangeProof.disclosure_only_the_bound, committed_inequality_via_range);
• jointly garbled — two parties evaluate a shared gate over private inputs; each learns the verdict and nothing else (GarbledJoint.garbled_input_private, joint_turn_private_gate).

Grounding

• cell/src/program.rs — the canonical constraint enum the table above is generated from; cell/src/blueprint.rs documents what programs deliberately cannot see.
• metatheory/Dregg2/Authority/{RelationalClosure,QuantifiedPredicate,ConfluenceClassifier,PrivatePredicate}.lean and metatheory/Dregg2/Crypto/{RangeProof,GarbledJoint}.lean — the theorems named above.
• metatheory/Dregg2/Laws.lean — the Predicate ⊣ Witness Galois connection the whole algebra sits on.

← 2 · Cells & substances · 4 · Receipts & Q →