Skip to content
LogoLogo

Security invariants

  1. Every value a rule judges is welded to context_root (structural: no unwelded accessor exists; weld-coverage lint proves it per build).
  2. Phase is determined by VK selection in W, never by a witness the policy can influence or a policy-readable public.
  3. A phase-1/2 policy cannot read sender_private leaves (type-level).
  4. 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.
  5. fiState is written only by the pool, only after a successful transition, only for the fi_index whose signature covered the publics.
  6. Only the bound recipient FI can resolve (fi_index == hold.recipient_fi_index, and fi_index is inside the signed publics).
  7. attestation_in at phase 1/2 equals what the phase-0 policy emitted.
  8. Every hash has a distinct domain tag; the tag table is mirrored and pinned across Noir, Rust, TS.
  9. VK hashes are reproducible from source plus pinned toolchain.
  10. No policy can brick its own FI: satisfiability lint across golden shapes and schema ids is a build failure, not a warning.
  11. Accept and reject records are byte-for-byte indistinguishable in calldata and events (leakage test replays both and diffs).
  12. 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.
  13. A wrapper proof cannot be replayed under a different FI index (fi_index in signed publics; possession proof at admit).
  14. Registry root window does not delay revocation (revoked[] checked directly).