feat(proofs/agda): upstream Echo/CNO bridge files from maa-framework vendored copy

[hyperpolymath]

Summary

Upstreams 3 Agda files that exist only in maa-framework's vendored copy of absolute-zero, but self-identify as absolute-zero artefacts.

• proofs/agda/EchoBridgeScaffold.agda — compile-safe interface (Echo Σ-shape, CNOModel), intentionally independent of CNO.agda.
• proofs/agda/EchoBridgeCNO.agda — concrete instantiation from CNO.Program / CNO.eval into the scaffold.
• proofs/agda/README.adoc — describes the directory.

Why now

Discovered during proof-debt classification triage for maa-framework (filed at hyperpolymath/maa-framework#82, with disposition analysis in hyperpolymath/maa-framework#84). The maa-framework re-vendor (hyperpolymath/maa-framework#83) currently uses rsync --filter='P ...' to preserve these files across each sync — once they're upstream, that filter becomes redundant.

The README.adoc literally titles itself "Agda Proofs (absolute-zero)" and the scaffold header says "Echo/CNO Agda bridge scaffold", so the canonical home is here.

Trusted-base impact

The 3-file set has zero postulates and zero axioms. EchoBridgeCNO.agda imports Axiom.Extensionality.Propositional to obtain the Extensionality type, which is then accepted as an explicit module parameter by downstream functions — not postulated. Documented in docs/proof-debt.md under a new "False positives" section to satisfy check-trusted-base.sh's path-enumeration clause.

Test plan

• cd proofs/agda && agda EchoBridgeScaffold.agda typechecks.
• cd proofs/agda && agda EchoBridgeCNO.agda typechecks (may need CNO.agda build prerequisites).
• bash scripts/check-trusted-base.sh . passes (path-enumeration covers the false positive).
• CI green.

Companion

• docs: seed proof-debt.md per standards#203 schema (all 150 markers §(e) vendored) maa-framework#82 — proof-debt schema PR (parallel).
• sync: re-vendor absolute-zero/ subtree to upstream HEAD (trusted-base + 16-commit catch-up) maa-framework#83 — re-vendor PR (parallel; this PR removes its need for rsync --filter='P ...').
• Decide: is absolute-zero/ a deliberate fork or stale vendor copy? maa-framework#84 — fork-vs-vendor disposition issue (open, owner-decision).
• docs(policies): trusted-base reduction policy for proof debt standards#203 — trusted-base reduction policy.
• feat(governance): add check-trusted-base CI enforcement standards#211 — check-trusted-base.sh.

Co-Authored-By: Claude Opus 4.7 (1M context) noreply@anthropic.com

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 64 issues detected

Severity	Count
🔴 Critical	8
🟠 High	16
🟡 Medium	40

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Ada pragma Suppress disables runtime checks (1 occurrences, CWE-704)",
    "type": "ada_pragma_suppress",
    "file": "/home/runner/work/absolute-zero/absolute-zero/examples/ada/balanced_ops.adb",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "User-defined Coq axiom -- not verified by kernel (3 occurrences, CWE-704)",
    "type": "coq_axiom",
    "file": "/home/runner/work/absolute-zero/absolute-zero/proofs/coq/quantum/QuantumMechanicsExact.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "User-defined Coq axiom -- not verified by kernel (29 occurrences, CWE-704)",
    "type": "coq_axiom",
    "file": "/home/runner/work/absolute-zero/absolute-zero/proofs/coq/quantum/QuantumCNO.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "User-defined Coq axiom -- not verified by kernel (2 occurrences, CWE-704)",
    "type": "coq_axiom",
    "file": "/home/runner/work/absolute-zero/absolute-zero/proofs/coq/lambda/LambdaCNO.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "User-defined Coq axiom -- not verified by kernel (1 occurrences, CWE-704)",
    "type": "coq_axiom",
    "file": "/home/runner/work/absolute-zero/absolute-zero/proofs/coq/category/CNOCategory.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "User-defined Coq axiom -- not verified by kernel (13 occurrences, CWE-704)",
    "type": "coq_axiom",
    "file": "/home/runner/work/absolute-zero/absolute-zero/proofs/coq/filesystem/FilesystemCNO.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "User-defined Coq axiom -- not verified by kernel (14 occurrences, CWE-704)",
    "type": "coq_axiom",
    "file": "/home/runner/work/absolute-zero/absolute-zero/proofs/coq/physics/LandauerDerivation.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "User-defined Coq axiom -- not verified by kernel (10 occurrences, CWE-704)",
    "type": "coq_axiom",
    "file": "/home/runner/work/absolute-zero/absolute-zero/proofs/coq/physics/StatMech.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "undefined/error causes runtime crash (2 occurrences, CWE-754)",
    "type": "undefined_error",
    "file": "/home/runner/work/absolute-zero/absolute-zero/examples/haskell/Nop.hs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "believe_me undermines formal verification (7 occurrences, CWE-704)",
    "type": "believe_me",
    "file": "/home/runner/work/absolute-zero/absolute-zero/src/abi/Proofs/DivMod.idr",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence