Skip to content
Security invariants
- Every value a rule judges is welded to
context_root (structural: no
unwelded accessor exists; weld-coverage lint proves it per build).
- Phase is determined by VK selection in
W, never by a witness the
policy can influence or a policy-readable public.
- A phase-1/2 policy cannot read
sender_private leaves (type-level).
params_commitment is welded to the FI leaf under a registry_root in
the pool's window; state_in is welded to fiState[fi_index] by the
pool.
fiState is written only by the pool, only after a successful
transition, only for the fi_index whose signature covered the publics.
- Only the bound recipient FI can resolve (
fi_index == hold.recipient_fi_index, and fi_index is inside the signed publics).
attestation_in at phase 1/2 equals what the phase-0 policy emitted.
- Every hash has a distinct domain tag; the tag table is mirrored and
pinned across Noir, Rust, TS.
- VK hashes are reproducible from source plus pinned toolchain.
- No policy can brick its own FI: satisfiability lint across golden
shapes and schema ids is a build failure, not a warning.
- Accept and reject records are byte-for-byte indistinguishable in
calldata and events (leakage test replays both and diffs).
- No public commitment opens to a low-entropy preimage without a salt
(params, state, attestation,
vk_root): a brute-force test over the
golden world must fail to recover any of them.
- A wrapper proof cannot be replayed under a different FI index
(
fi_index in signed publics; possession proof at admit).
- Registry root window does not delay revocation (
revoked[] checked
directly).