P2b zk-chain — security argument (PRE-AUDIT)#
Status: PREVIEW / novel cryptography — NOT externally audited, NOT production-trusted.
This document is the security argument for the P2b structure-hiding delegation circuit (crates/grantor-zkchain, deed mode == "zk-chain"). It is written to be the first thing an external cryptographer reads. It states precisely what the circuit claims, argues each claim against the actual constraint system, and is deliberately candid about the construction's limits. It is not marketing: nothing here should be read as a certification of soundness. It is the artifact whose review is a hard precondition for production use.
P2b is a from-first-principles construction, not the integration of an audited library. It ships behind a "preview, pending external cryptographic review" label with a single-contributor trusted setup. Until (a) an external cryptographer reviews the circuit and this argument, and (b) a multi-party trusted-setup ceremony replaces the preview parameters, a proof verifying against the shipped verifying key MUST be treated as unauthenticated.
Design spec: docs/superpowers/specs/2026-08-06-capabilities-p2b-structure-hiding-design.md.
1. Scope and threat model#
1.1 What P2b claims#
A single Groth16 proof over the fixed-shape DelegationChainCircuit (N = 8 hops, Merkle depth 20, BN254) attests, to a relying party that verifies it, exactly:
"I know a delegation chain of hidden length
ℓwith1 ≤ ℓ ≤ 8, rooted at a public membershiprootof tenanttenant, where the root delegator is an enrolled member, each hop is an offline EdDSA delegation that monotonically narrows the authority it passes on, the chain was signed for registryepoch, and it confers the effective-grant commitmentg_effon a leaf key I control — and I am answering the fresh publicchallenge."
The verifier learns only the five public inputs (root, g_eff, challenge, tenant, epoch). It does not learn the hop count ℓ, the intermediate delegators' keys, or the intermediate grants.
1.2 The public / private split (the circuit's instance and witness)#
Public inputs, in the exact order the verifier supplies them (DelegationChainCircuit::public_inputs, circuit.rs):
root— the tenant membership-tree root the root delegator is a member of.g_eff— a Poseidon commitment to the effective (leaf) grant.challenge—public_challenge(rp_challenge_string), an anti-replay nonce.tenant— the tenant id (au64lifted toFr).epoch— the delegation-cohort epoch (au64).
Private witnesses: the N_HOPS hop slots (signer_pk, child_pk, grant_commit, signature (R, S), and a real/padding flag is_real), each hop's interned GrantValues, the Merkle (siblings, is_left) path for the root delegator, the leaf secret sk_leaf, and ℓ.
1.3 The adversary#
- A malicious prover / presenter. Writes its own witness generator; is not bound by the SDK helper types; wants a verifying proof for a statement that is false — an effective authority no real chain conferred, membership it does not have, or a chain that widened authority. This is the primary adversary and the target of the gap hunt in §2.1.
- A hostile origin. A web page or service that induces a holder to produce a proof, hoping to harvest, relink, or replay it. Relevant to replay resistance (§2.4) and the origin caveat (§1.5).
- A curious verifier. An honest-but-curious relying party that wants to learn more than the five public inputs — the hop count, the intermediate delegators, the identities in the chain. The target of the structure-hiding argument (§2.3).
1.4 The trust base (assumptions this argument RESTS ON, not proves)#
- Groth16 soundness over BN254 — a verifying proof implies a satisfying witness, under the knowledge-of-exponent / generic-group assumptions Groth16 requires, given a trusted setup whose toxic waste was discarded. The preview setup does NOT satisfy that last clause (§1.5, §3).
- The verifying key
params/vk.binis the honest output of the setup for this exact circuit shape. Pinned in-tree bywire.rs::committed_vk_matches_run_preview_setup. - The BN254 pairing / discrete-log hardness, and Poseidon (the vendored circomlib/iden3 instance) as a collision-resistant hash and as the Schnorr/EdDSA challenge function.
- Baby-JubJub EdDSA (Schnorr-style over the prime-order subgroup) as an unforgeable signature — see §2.1.3 for the one non-standard detail (x-only challenge hashing).
- The on-chain
GrantorRegistryas the source of truth for membership recency, tenant billing status, and the delegation epoch. The off-circuit reads (§2.5) trust it. - arkworks
ark-r1cs-std0.5.0 correctly enforces the gadget semantics it documents — in particular thatEdwardsVar::new_witnessallocates an on-curve, prime-order-subgroup point (§2.1.3 depends on this and it was verified against the crate source).
1.5 Explicitly OUT of scope / preview-gated#
- The trusted setup is a preview, not a ceremony.
params/is produced by a single contributor from a fixed deterministic RNG seed (setup.rs::PREVIEW_SETUP_SEED). The toxic waste is not assumed discarded; anyone who reconstructs the seed can forge proofs that verify againstvk.bin. This is the single largest gap and is a hard production blocker (§3). - No external audit yet. This document has not been reviewed by an external cryptographer. The internal adversarial gap hunt in §2.1 is not a substitute for that review.
- Origin binding is not part of the P2b proof.
verify_delegation_chaindoes not bind an origin into the circuit; azk-chaindeed carries the same holder-side, no-in-proof-origin posture as theagent-zkmint path. Cross-origin harvesting mitigations are a property of the broader sovereign tier, not of this circuit, and are not claimed here. - The tenant is revealed, by design.
rootandtenantare public; P2b hides the chain's internal structure, not which tenant tree it is anchored in (this is P2a-class and inherent). - The
nbpredicate superset is enforced off-circuit (§2.2.4, §2.6). A verifier that stops at the Groth16 check has authenticated what authority (a commitment) but not that a specific request opens it. - Depth is bounded at N = 8. Chains deeper than 8 are refused before proving and use the visible (non-structure-hiding) delegation path instead.
keypair_from_seedis a preview/demo constructor (64-bit seed). It is the only Baby-JubJub keypair constructor exposed across the FFI and has insufficient entropy for production key material (eddsa.rsflags this).
2. Security properties#
Each property is stated, then argued against the constraint system. Constraint locations are cited by file and the composition-carry numbering used in circuit.rs.
2.1 Authority unforgeability#
Claim. A prover cannot produce a verifying proof for an effective grant g_eff that was not actually conferred, by a real monotone-narrowing chain, starting from an enrolled member of tenant under root.
The argument is the conjunction of five bindings; each is necessary, and together they close the path from "an enrolled member's key" to "the public g_eff the guard will enforce."
2.1.1 Root membership (an enrolled member is the root)#
circuit.rs block (B) derives the membership leaf leaf = Poseidon(pk_0.x ‖ pk_0.y) from hop 0's signer key hop_vars[0].signer_pk, recomputes the depth-20 Merkle root from the private (siblings, is_left) path via membership_root_gadget (shared verbatim with MembershipCircuit), and enforces recomputed_root == root. Because the in-circuit Poseidon is bit-identical to semaphore's (poseidon.rs, vendored circomlib constants; structurally pinned by tests/membership_parity.rs against the real semaphore-rs tree, SAT with the true root and UNSAT with a wrong one), a satisfying path exists iff Poseidon(pk_0) is a genuine leaf of the tree whose root is root. Off-circuit, verify_delegation_chain reads root_is_recent(tenant, root), so root must be a currently-valid tenant root (§2.5). The leaf binds both coordinates of pk_0 (carry 5), so the enrolled member is the chain's root delegator — not merely some key sharing an x-coordinate.
2.1.2 The EdDSA hop chain (each hop was authorized offline by its parent)#
Hop 0 is forced real (hop_vars[0].is_real.enforce_equal(TRUE)), so its EdDSA signature is enforced: the enrolled member must have signed the delegation. For every real hop k, enforce_hop_chain (hopchain.rs) enforces eddsa_verify_gadget(signer_pk, R, S, M_k) == TRUE conditioned on is_real (SECURITY CORE A, mutation-gated by the mutate-forged-hop feature; tests/hopchain.rs::forged_single_hop_is_unsat, wrong_key_hop_is_unsat, forged_hop_breaks_chain). Producing a valid (R, S) for a signer key whose discrete log the prover does not know is a Schnorr/EdDSA forgery, hard under §1.4.3–4.
The hops form a genuine, gap-free, ordered path:
- Link — a real hop's
signer_pkequals the previous hop'schild_pk(conditional_enforce_equal(prev_child, is_real)). The delegatee of hopk−1is the signer of hopk. - Monotone real-prefix — a real hop after a padding hop is UNSAT (
(is_real & !prev_real) == FALSE;tests/hopchain.rs::real_hop_after_padding_is_unsat). Real hops are a contiguous prefix; the prover cannot interleave to skip a check. - Chaining hash —
chaining_0 = Poseidon(tenant ‖ epoch), and each hop message folds in its predecessor's, so a hop signed for a different chain position cannot be spliced in (tests/hopchain.rs::spliced_hop_from_other_chain_is_unsat).
Padding cannot smuggle authority (SECURITY CORE B). A padding hop (is_real == false) has its signer_pk, sig_r, sig_s pinned to the sentinel/zero, and — the authority-bearing pins — its child_pk pinned to the identity and its grant_commit pinned to 0 (hopchain.rs, mutation-gated by mutate-padding; tests/hopchain.rs::padding_hop_smuggling_authority_is_unsat, padding_hop_smuggling_delegatee_is_unsat). A hidden slot therefore cannot carry a grant or a delegatee no delegator signed. Carry 4 additionally forbids a real hop from using the identity as its signer or delegatee, closing the "identity signer ⇒ EdDSA trivially satisfiable" hole.
2.1.3 Curve-point well-formedness (why the EdDSA gadget is sound)#
Every Baby-JubJub point in the circuit (signer_pk, child_pk, sig_r) is allocated with EdwardsVar::new_witness. In ark-r1cs-std 0.5.0 the AllocVar<TEProjective> Witness path (verified against the crate source) enforces both:
- on-curve —
d·x²·y² relationviamul_equalsinnew_variable_omit_prime_order_check; and - prime-order subgroup membership — the Witness branch returns a cofactor-cleared point (
8·hfor the witnessedh), which is guaranteed to lie in the prime-order-rsubgroup.
This matters because Baby-JubJub has cofactor 8. Without the subgroup enforcement a malicious prover could witness a mixed-order point and mount a small-subgroup attack against the verification equation [S]·B == R + [h]·A. Because the circuit uses new_witness (not the _omit_prime_order_check variant), A (= signer_pk) and R are prime-order, and the base point B is prime-order by construction (base_point() = generator × cofactor). Reducing S and h mod r is therefore invisible, which is exactly what makes the native signer and the in-circuit verifier agree (eddsa.rs module doc; parity pinned by tests/hopchain.rs::native_signer_matches_incircuit_verify).
Non-standard detail flagged for the auditor. The EdDSA challenge is h = Poseidon(R.x ‖ A.x ‖ M) — it commits to the x-coordinates only of R and A, not the full compressed points (contrast Ed25519, which hashes the full encoded R and A). This argument holds it sound because: (a) A is fully pinned elsewhere — hop 0's A by the two-coordinate membership leaf, every later A by the two-coordinate link to the prior child_pk — so an x-sharing substitute cannot be swapped in; (b) the full R (both coordinates) enters the verification equation, so a valid (R, S) pins R completely; and (c) all points are prime-order. This is a known-shape Schnorr variant, but it is a deviation from standard EdDSA and is called out as a primary item for external scrutiny (§4, item 1).
2.1.4 Grant binding — the narrowed grant IS the signed grant (the soundness crux)#
For each real hop the circuit witnesses the plaintext ArithGrant g and enforces, gated on is_real, Poseidon(g.res_id ‖ g.act_mask ‖ g.exp ‖ g.max_uses ‖ g.nb_commit) == grant_commit (carry 2, circuit.rs). grant_commit is the value the hop's EdDSA message M_k signs (hopchain.rs::hop_message). So the grant the narrowing sub-circuit checks (§2.2) is byte-for-byte the grant the parent delegator actually signed — not a second value that merely looks like it. This is what stops a prover from proving a narrowing over one grant while presenting the signature for another. The operands are range-checked to genuine u64 (carry 3, enforce_u64) so the diff-based ≤ checks in §2.2 cannot be fooled by field wraparound. tests/end_to_end.rs::TAMPER 3 re-signs a widened leaf grant so the only defect is the widening; it is UNSAT, proving the join is present.
2.1.5 g_eff is bound to the guard, and to the chain#
circuit.rs block (D) selects the last real hop (is_last_real = is_real[k] & !is_real[k+1]; exactly one hop qualifies under the monotone prefix), takes its child_pk and grant_commit, and enforces selected_gc == g_eff (public). Block (E) enforces leaf-key ownership, [sk_leaf]·B == selected_child — the presenter must know the secret of the last delegatee. So g_eff is fully determined by the witness: it equals the commitment of the leaf grant, which (§2.2) narrows its parent, which narrows its parent, up to the root grant the enrolled member signed. A prover cannot claim a g_eff the chain did not confer, nor present without the leaf secret. g_eff is the value the off-circuit CapabilityGuard opens and enforces (§2.6).
Conclusion. A verifying proof implies (Groth16 soundness, §1.4.1) a witness satisfying all of the above simultaneously: an enrolled member's key (§2.1.1) that signed the first delegation (§2.1.2), a gap-free signed chain with no smuggled authority (§2.1.2–3), each hop's checked grant equal to its signed grant (§2.1.4), narrowing down to a leaf grant whose commitment is the public g_eff and whose key the presenter controls (§2.1.5). Forgery reduces to breaking Groth16 soundness, EdDSA unforgeability, Poseidon collision resistance, or the trusted setup — the last of which is a preview assumption, not a real one (§3).
2.2 Monotone narrowing soundness#
Claim. No hop can widen the authority it received: for each real hop k ≥ 1, hop k's grant is a legal narrowing of hop k−1's grant, in every field.
circuit.rs block (C) calls enforce_narrows_conditional(parent, g, is_real) (narrowing.rs) for each real hop, where parent is the prior hop's grant. The in-circuit relation mirrors the off-circuit grant_narrows clause-for-clause, modulo the interning contract:
res_id—child.res_id == parent.res_idORparent.res_id == WILDCARD_RES_ID(id 0). A concrete resource pattern must never be interned to id 0 (RP contract, §2.7). The circuit models strictly fewer resource relations than the off-circuit glob grammar, so it can never attest a res-widening the guard would reject. (tests/narrowing.rs::out_of_hierarchy_res_id_is_unsat,wildcard_parent_contains_any_child_res.)act_mask—child_mask & parent_mask == child_mask(no bit set in the child that is clear in the parent), with both masks range-checked to< 2^64. (tests/narrowing.rs::wider_act_is_unsat.)exp,max_uses—child ≤ parentvia a 64-bit range check onparent − child, withNoneinterned toUNBOUNDED_SENTINEL = u64::MAX. An unbounded parent dominates any child; an unbounded child against a bounded parent underflows the range check and is refused — reproducingcaveat_leexactly for u64-domain values. (tests/narrowing.rs::larger_exp_is_unsat,larger_max_uses_is_unsat,unbounded_parent_caveat_dominates_bounded_child.)nb_commit—child.nb_commit == parent.nb_commit(equality only). (tests/narrowing.rs::altered_nb_commit_is_unsat.)
The nb equality-vs-superset split. The off-circuit narrowing rule for the predicate set nb is superset (the child carries every parent predicate, and may add more). That is a set test over predicate values the circuit does not hold — it holds only the opaque commitment. So the circuit enforces the strictly stronger relation nb_commit equality: the predicate set is inherited verbatim. Equality is a completeness gap (it rejects the legal case where a child adds a predicate, changing the commit), never a safety gap: any dropped or altered parent predicate also changes the commit and fails equality, so the circuit never attests an nb-widening. The real superset check against a live request is the off-circuit guard's job (§2.6). Do not relax the in-circuit rule to accept unequal commits without moving the superset test into the circuit.
Because narrowing is transitive and the chain is gap-free (§2.1.2), the leaf grant is a narrowing of the root grant, and g_eff commits to it. The root grant itself is unconstrained by narrowing (the enrolled member is the top of authority within the tenant) — this is intended: a member's delegation confers whatever the member signs, bounded only by what the tenant means by that member's enrollment.
2.3 Structure-hiding / unlinkability#
Claim. The verifier learns only (root, g_eff, challenge, tenant, epoch) — not the hop count ℓ, and not any intermediate delegator's key or grant.
- Padding to N = 8 hides
ℓ. The circuit always proves exactlyN_HOPSslots;ℓis a private witness and padding hops are structurally indistinguishable (SECURITY CORE B makes them carry no authority, but they occupy identical constraint shape). One fixed(pk, vk)serves everyℓ.tests/end_to_end.rsproves the depth-hiding surface: proofs forℓ = 1, 4, 8are byte-for-byte the same size, so the verifier cannot recoverℓfrom the proof. - Everything but the public inputs is a private witness — intermediate
signer_pk/child_pk, the grants, the signatures, the Merkle path,sk_leaf, andℓare allnew_witness. - Groth16 zero-knowledge.
wire.rs::prove_delegationdraws fresh OS entropy for the proof blinders on every call, so the proof reveals nothing about the witness beyond what the public inputs already fix.
Honest limits on unlinkability. g_eff and nb_commit are deterministic Poseidon commitments (no per-presentation randomness). Two presentations conferring the same effective authority under the same tenant therefore carry the same g_eff and are linkable as "same effective authority, same tenant tree"; and because grant fields are low-entropy, an observer who guesses a plausible grant can confirm it opens a given g_eff. Structure-hiding hides ℓ and the intermediates; it does not hide the effective-authority label or the tenant. This is inherent to revealing g_eff (the guard needs it) and root (P2a-class), and is not claimed otherwise.
2.4 Replay resistance#
Claim. A proof produced for one RP challenge does not verify against another.
challenge is a public input. The verifier reconstructs it from its own expected_challenge via public_challenge (wire.rs) — never from the wire — so a proof made for a different challenge string yields a different public-input vector and fails the pairing check (tests/end_to_end.rs::TAMPER 1, wrong challenge ⇒ verify FALSE; and circuit.rs::delegation_groth16_roundtrip returns wrong_challenge_rejected). The circuit also folds challenge into a Poseidon constraint alongside the leaf key (block (F)) so the binding is explicit in R1CS, though Groth16 already binds every public input via the verification pairing regardless. Freshness of the challenge (that it was issued by this RP and not yet consumed) is the RP's ChallengeStore responsibility, off-circuit, exactly as for every other sovereign mode.
2.5 Revocation and billing#
Claim. A revoked member, a bumped epoch, or a lapsed tenant cannot authenticate — all enforced off-circuit, fail-closed.
verify_delegation_chain (sovereign_gate.rs) performs, after the Groth16 check and all ?-propagated so any chain-read error is a refusal:
- Membership recency = revocation —
root_is_recent(tenant, root).rootis a public input the proof is bound to (§2.1.1); when a member is revoked or the tenant tree moves on, the old root ages out of the on-chain recency window and the proof'srootno longer reads recent ⇒StaleRoot. - Epoch cohort revocation —
delegation_epoch(tenant, ZK_CHAIN_EPOCH_LABEL)must equal the proof'sepoch.bumpEpochon that label increments the on-chain counter, instantly invalidating every outstandingzk-chaindeed for the tenant (the epoch is also folded into every hop signature and the chaining IV, so re-delegation is required to re-prove) ⇒EpochRevoked. Note this is a single tenant-wide cohort label: one bump revokes all of the tenant'szk-chaindeeds at once (coarse but intentional). - Billing —
tenant_is_active(tenant)(Active || Grace), mirroring the issuer's own mint gate ⇒TenantInactive.
The gate reads are injected via DeedChainGate, wrapped in CachedGate (short-TTL, never serves a stale "recent"/"active" answer through an RPC outage; the cache maps that are keyed partly by attacker-influenced data are bounded) and optionally QuorumGate (N independent RPC views, unanimity required, so one honest provider vetoes a lie). No new gate method and no contract change: these are the same three ports P0/P1 already use.
2.6 The off-circuit enforcement obligation (nb / request coverage)#
Claim, stated as an obligation. Groth16 verification authenticates what authority g_eff commits to; it does not decide whether a specific request is covered. That is the guard's job and MUST be invoked.
verify_delegation_chain returns g_eff in claims.sub and stops. To authorize a request the RP calls CapabilityGuard::authorize_zk_chain (capguard.rs), which (a) recomputes arith_grant_commit(grant_values) == g_eff to authenticate that the RP's own candidate plaintext grant really is the committed authority — a mismatch is CapabilityDenied — and then (b) runs the same res_matches / action-set / caveats_hold (including the real nb predicate check against the live request) that a P0/P1 effective grant gets. The candidate grant is the RP's own policy, never taken from the request: an untrusted caller supplying its own plaintext could otherwise assert any caveats for a commitment it never proved (nb_commit is opaque; nothing can verify a caller-supplied nb map hashes to it). A relying party that verifies the proof but never calls the guard has authenticated a commitment and enforced nothing — that is a usage error, and the reference MCP server exists to show the correct wiring.
2.7 No cross-tenant / cross-tree confusion#
Claim. A proof valid under one tenant's tree cannot be replayed as membership in another, and the resource/authority namespace cannot be confused across tenants.
root and tenant are pinned public inputs. The proof binds membership to a specific root (§2.1.1); verify_delegation_chain checks that root against tenant's on-chain tree via root_is_recent(cfg.tenant, root) and matches deed.tenant == cfg.tenant and deed.aud == cfg.audience — all from the verifier's own configuration, never the wire. The chaining IV and every hop message fold in tenant and epoch, so signatures are bound to a (tenant, epoch) domain and a chain signed for one tenant does not verify under another. The resource-id namespace is per-RP interning (§2.2, and the interning trust boundary below), so an id means what that RP's table says it means.
The resource-interning trust boundary (RP integration, not circuit soundness). The circuit proves narrowing over the res_id / act_mask / nb_commit values it is handed; the mapping from real resource patterns (globs) and action strings to those field elements is the RP's published interning contract (grantor-sdk-core::zkchain module doc, narrowing.rs module doc). The RP MUST assign a distinct id to each concrete pattern, never intern a concrete pattern to WILDCARD_RES_ID (0), and pre-resolve any glob hierarchy into either id-equality or a wildcard-parent relation. A mis-interning is an RP bug that makes narrowing express the wrong containment; the circuit cannot detect it. This is a documented, tested integration surface, not an under-constraint.
3. The trust gate (requirements before production)#
P2b is preview. The following are hard requirements, not nice-to-haves, before any zk-chain deed may carry real authority:
- External circuit + argument review. An independent cryptographer must review the circuit (
crates/grantor-zkchain/src/*) and this document, with specific attention to the items in §4. The internal gap hunt (§2.1, and the pre-audit report in.superpowers/p2b-security-argument-report.md) is a starting point, not a substitute. - A multi-party trusted-setup ceremony (or migration to a transparent / updatable SNARK) must replace the single-contributor preview parameters. Until then the toxic waste is a live forgery capability: whoever knows the setup randomness can forge any proof.
params/README.mdandsetup.rslabel this; the label is the control today, and it is not sufficient for production. - Production key material.
keypair_from_seed's 64-bit seed must be replaced by full-entropy secret derivation for any real delegator/leaf key. - The reference wiring must be the enforced path. Any RP consuming
zk-chainmust call the off-circuit guard (§2.6); a verify-only integration authenticates authority but enforces no request coverage.
Until every item above is satisfied, a proof verifying against the shipped vk MUST be treated as unauthenticated.
4. Where an auditor should push hardest (weakest parts, honestly)#
In rough priority. None is a known break; each is where this construction is most novel or where the argument is thinnest.
- The x-only EdDSA challenge
h = Poseidon(R.x ‖ A.x ‖ M)(§2.1.3). This deviates from standard EdDSA (which hashes the full compressedRandA). The argument leans onAbeing fully pinned by other constraints, the fullRentering the verification equation, and prime-order enforcement. Confirm there is no ± / rogue-key / malleability subtlety that the reduced binding admits. - The trusted setup. Preview, single-contributor, deterministic seed — a live forgery capability until a ceremony replaces it (§3).
- Poseidon domain separation. The same t=3 Poseidon (
hash2/ sponge-fold) is reused across at least six contexts — membership node, grant commitment, hop message, chaining, EdDSA challenge, and the membership leaf — with no explicit per-context domain tag. The argument that there is no cross-context type-confusion rests on values being consumed only in type-fixed positions plus collision resistance. Adding explicit domain separators is a recommended production hardening; confirm the absence of a concrete collision path in the meantime. (The EdDSA nonce is domain-separated from the challenge by a fixed tag ineddsa.rs::sign, which is the one place it is load-bearing today.) - The membership-leaf encoding shared with the agent tree.
zk-chainroots enroll asPoseidon(pk_0.x ‖ pk_0.y)in the same on-chain treeagent-zkuses. Confirm the leaf preimage requirements keep the two credential types from cross-contaminating (Poseidon preimage resistance is the argument). - The
ℓwitness is decorative.ellis bound only byreal_sum == ellwithella free witness, so it constrains nothing (the structure is enforced by the monotone prefix andis_real[0] == TRUE, not byell). Harmless, but confirm no downstream logic mistakesellfor an independently-constrained value. - Deterministic
g_eff/nb_commit(§2.3) — the linkability and openability limits on effective authority. Confirm these match the product's stated privacy claims and are not oversold as unlinkability.
5. Test and mutation evidence (what backs the arguments above)#
- Membership parity —
tests/membership_parity.rs: in-circuit root == realsemaphore-rsroot (SAT), wrong root UNSAT, full Groth16 round-trip. - Narrowing —
tests/narrowing.rs: one UNSAT test per widening field (act, exp, max_uses, res, nb), plus wildcard and unbounded-sentinel cases; each cross-checks the nativenarrowsoracle. - Hop chain —
tests/hopchain.rs: forged single hop, wrong-key hop, forged hop in a chain, padding smuggling a grant, padding smuggling a delegatee, real-after-padding, spliced hop — all UNSAT. SECURITY CORE A/B are mutation-gated (mutate-forged-hop,mutate-padding): the reject tests regress to SAT (and fail) when the constraint is removed, giving reproducible RED→GREEN evidence that the constraint is load-bearing. - Full circuit —
tests/end_to_end.rs: validℓ=3verifies; wrong challenge, wrong root, widened leaf (re-signed so only the widening is the defect), and forged hop each verify FALSE at the full Groth16 level;ℓ=8works; depth-hiding (ℓ=1,4,8proofs same size). - Wire / vk pin —
wire.rs:committed_vk_matches_run_preview_setuppinsparams/vk.binto the deterministic setup, so a stale or mismatched key cannot hide.
Mutation-proven reject tests are strong evidence a constraint is present and load-bearing. They are not evidence that the set of constraints is complete — that is precisely what the external review in §3 must establish.