circomlib Decoder Underconstraint PoC (Evidence-First)

This repository provides a triage-ready, reproducible PoC for underconstraint in:

• /home/teycir/zk/cat5_frameworks/circomlib/circuits/multiplexer.circom
• Component: Decoder(w)

Submission pack

• QUICKSTART.md: one-command execution flow and output locations.
• EXECUTIVE_SUMMARY.md: concise issue, proof, and remediation summary.
• REAL_IMPACT_SUMMARY.md: impact bounded to demonstrated evidence.
• docs/REAL_WORLD_USAGE_EVIDENCE.md: verified downstream users and dependency pins.
• docs/CVSS_ASSESSMENT.md: contextual CVSS profiles for triage.

What is proven

1. Same input can admit two valid output sets at Decoder component scope.
2. Z3 Picus matrix (counter/first, weak/strong) repeatedly reports underconstraint with explicit counterexamples.
3. SMT models independently reproduce satisfiable dual-output behavior.
4. A control policy (success == 1) makes the dual-output search unsatisfiable in SMT.

Quick start

cd /home/teycir/Repos/circomlib-exploit
./scripts/run-full-underconstraint.sh

Extended run and sync instructions:

• QUICKSTART.md

Primary output directory:

• 4-impact-demonstration/evidence/circomlib_decoder/

Key outputs:

• REALISM_VALIDATION_SUMMARY.md
• ZERO_WIGGLE_EVIDENCE.md
• ZERO_WIGGLE_EVIDENCE.json

Repository structure

circomlib-exploit/
├── 1-vulnerability-proof/
├── 2-target-analysis/
├── 3-counterexample-construction/
├── 4-impact-demonstration/evidence/circomlib_decoder/
├── 5-mitigation-analysis/
├── docs/
└── scripts/

Scope constraints

• This PoC is component-focused (Decoder).
• Wrapper-level/system-level exploitability is integration-dependent.
• Real bug, real usage, but currently no confirmed unmitigated deployment found in the analyzed public targets.
• No realistic end-to-end attack path is claimed without downstream evidence.
• Claims are intentionally evidence-bounded.
• Archived scaffold leftovers are preserved under legacy-template/.