Summary
method:strip_prefix postconditions are emitted correctly by the kit-side RPC, but the producer bridge is absent from the final target proof. The two expected CLI closures therefore stay unproven even though the caller-side contracts and method:expect bridges are present.
Evidence
- Local kit RPC emits the
method:strip_prefix producer bridge with argTerm = method:strip_prefix(digest,"blake3-512:") for the audited signer-seed sites.
- Decoded cold target proof contains caller contracts for
deterministic_signer_seed with the expected panic loci:
cmd_emit.rs:531, producer line 530
cmd_mint.rs:2439, producer line 2438
- Decoded cold target proof contains synthetic contracts
digest_strip_prefix__emit_signer_seed and digest_strip_prefix__mint_signer_seed with post = is_some(result).
- Decoded cold target proof contains the caller-side
method:expect bridges at cmd_emit.rs:531 and cmd_mint.rs:2439.
- Decoded cold target proof does not contain the corresponding
method:strip_prefix producer bridge.
Impact
The strip_prefix +2 closure is gated on a downstream mint/proof-inclusion or verifier bundle-scoping fix. The kit-side arg0_literal work was reverted because it has no working consumer until this bridge reaches the final proof.
Relates to #1901; this is the same producer-bridge-into-caller-bundle question in a smaller form.
Summary
method:strip_prefixpostconditions are emitted correctly by the kit-side RPC, but the producer bridge is absent from the final target proof. The two expected CLI closures therefore stay unproven even though the caller-side contracts andmethod:expectbridges are present.Evidence
method:strip_prefixproducer bridge withargTerm = method:strip_prefix(digest,"blake3-512:")for the audited signer-seed sites.deterministic_signer_seedwith the expected panic loci:cmd_emit.rs:531, producer line530cmd_mint.rs:2439, producer line2438digest_strip_prefix__emit_signer_seedanddigest_strip_prefix__mint_signer_seedwithpost = is_some(result).method:expectbridges atcmd_emit.rs:531andcmd_mint.rs:2439.method:strip_prefixproducer bridge.Impact
The strip_prefix +2 closure is gated on a downstream mint/proof-inclusion or verifier bundle-scoping fix. The kit-side
arg0_literalwork was reverted because it has no working consumer until this bridge reaches the final proof.Relates to #1901; this is the same producer-bridge-into-caller-bundle question in a smaller form.