[P1] stapeln: 20 idris_crash + 10 believe_me + chainCommutative regression

[hyperpolymath]

Crypto repo: 10 believe_me, 20 idris_crash, 45 partial, 5 assert_total. Fix chainCommutative regression (2026-04-19); land String-bridge postulate elimination. 13 tracked postulates that are genuine hardness assumptions stay.

Sub-issue of #124. PRs Refs hyperpolymath/standards#124. Joint-close only on explicit agreement.

🤖 Generated with Claude Code

[hyperpolymath]

PR hyperpolymath/stapeln#52 opened (Refs, not Closes).

Reconciliation: 0 genuine believe_me (raw 10 = comments/docstrings). 20 idris_crash = documented Idris2-0.8 postulate idiom — genuine crypto-hardness (ed25519/sha256/replay/tamper) + Zig-FFI runtime stubs — correctly stay (matches audit's 'stapeln crypto axioms genuine').

Genuine fix landed: chainCommutative regression (2026-04-19) RESOLVED & idris2-verified. Sharpened root cause: blocker was verifyChain being recursive + partial (no clause reduces in conversion, not even verifyChain h []=True), not merely the if. Refactored verifyChain → non-recursive allValid∘map verifyPair; proven via total boolCommTrue; dependent proofs untouched; full cerro-torre.ipkg green. PROOF-NEEDS reconciled (13→12).

Remaining (keeps #129 open): String-bridge elimination — ImporterProofs.idr string-primitive postulates need a bridge postulate to the proven List-Char equivalents in StringLemmas.idr (charsPrefixOf etc.); scoped in PROOF-NEEDS §'Path to eliminating String postulates'. Genuine, separate engineering.

[hyperpolymath]

PR hyperpolymath/stapeln#53 opened (String-bridge arm; independent of #52).

Both genuine #129 engineering arms now landed & idris2-verified:

• chainCommutative regression RESOLVED → stapeln#52 (verifyChain refactor + boolCommTrue).
• String-bridge → stapeln#53: 2 minimal documented axioms (isPrefixOfBridge, unpackAppend) discharge extractionSafety/symlinkSafety/zipSlipPrevention as real proofs (3 ad-hoc → 2 fundamental, boj-server-class). Full cerro-torre.ipkg green.

Reconciliation summary for #129: 0 genuine believe_me; 20 idris_crash = documented postulate idiom (genuine crypto-hardness + Zig-FFI runtime stubs, correctly stay); 2 genuine debts found & fixed. Remaining 3 ImporterProofs postulates (normalizedIsSafe/absolutePathRejection/ociLayoutEnforcement) scoped in PROOF-NEEDS as deeper infra. #129 substantively complete — ready for joint-close on your agreement once #52/#53 reviewed.