feat: EchoReversibilityBridge — discharge 007 L10 reversibility obligations

[hyperpolymath]

What

A new module proofs/agda/EchoReversibilityBridge.agda — the constructive discharge of the 007 language's Layer-10 reversibility (echo-residue) phase-2 proof obligations against echo-types as the library of record.

007 models reversibility with an echo residue (reversible as <name> arms a cell holding an Echo f y; reverse <name> consumes it to recover the input), specified in Idris2 (EchoResidue.idr / EchoResidueLinear.idr). Those obligations were informal requirements on 007's checker. This module re-states the interface they describe and proves echo-types' own Echo / EchoTotalCompletion / EchoLinear satisfy it — turning the informal claim into a checked theorem in the source of truth.

The bridge

Headline	Discharges	Proof
ReversibleCompletion f Residue	the interface 007 needs: hold (arm) / takeForReverse (replay) / reverse-recovers (once-only correctness), residue carrier as a parameter	record
echo-reversible : ReversibleCompletion f (Echo f)	Echo f is such a carrier	hold = echo-intro, takeForReverse = proj₁ (= reverseLinear's witness), recovery refl
reversibility-via-totality : Σ B (Echo f) ↔ A	the slogan "irreversible f + residue = reversible representation"	symmetric partner of EchoTotalCompletion.A↔ΣEcho via mk↔ₛ′
capability-can-be-dropped : LEcho linear → LEcho affine	phase-2 "affine capability" (the undo may be dropped)	EchoLinear.weaken
no-recovery-once-dropped	phase-2 "linear consumption / Spent doesn't reverse" (no section of weaken)	EchoLinear.no-section-weaken

Discipline

• --safe --without-K, zero postulates, no funext.
• Wired into All.agda (next to EchoCNOBridge, the other cross-repo 007 bridge).
• Five headlines pinned in Smoke.agda under their own using block with a header comment.
• Verified on the latest main: EchoReversibilityBridge.agda, Smoke.agda, and All.agda all agda --safe --without-K exit 0 (captured locally; absolute-zero fetched at the CI-pinned ref 3ff5cee).

Notes

• The Agda here is the source of truth; 007's Rust checker and Idris2 spec mirror this model. The takeForReverse field is the total Just-branch of 007's takeForReverse : … → Maybe a (the Maybe is runtime Holding/Spent bookkeeping, not part of the type-level correspondence).
• A 007-side doc pointer to this module is a trivial follow-up, best landed after 007#55 merges.

🤖 Generated with Claude Code

https://claude.ai/code/session_018CaSgNjNURC7ocsyjYh9We

---

Generated by Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 6 issues detected

Severity	Count
🔴 Critical	0
🟠 High	3
🟡 Medium	3

View findings

[
  {
    "reason": "No test directory or test files found",
    "type": "no_tests",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "flag",
    "rule_module": "honest_completion",
    "severity": "high",
    "deduction": 20
  },
  {
    "reason": "Nominal-only SAST in echo-types: codeql.yml language matrix contains no language present in the repo and lacks `actions`, so CodeQL records zero results on every commit. Remediation: set the CodeQL matrix to `language: actions`.",
    "type": "StaticAnalysis",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "auto_fix",
    "rule_module": "scorecard",
    "severity": "medium",
    "remediation": "Add CodeQL or equivalent SAST workflow.",
    "scorecard_check": "SAST"
  },
  {
    "reason": "Repository has 6 non-main remote branch(es). Policy: single main branch only.",
    "type": "GS007",
    "file": ".",
    "action": "delete_remote_branches",
    "rule_module": "git_state",
    "severity": "medium"
  },
  {
    "reason": "Code scanning (Scorecard): TokenPermissionsID -- Token-Permissions -- 18 day(s) old [STALE]",
    "type": "CSA001",
    "file": ".github/workflows/scorecard.yml",
    "action": "escalate",
    "rule_module": "code_scanning_alerts",
    "severity": "high"
  },
  {
    "reason": "Code-scanning alert TokenPermissionsID (high) at .github/workflows/scorecard.yml is 18 days old (threshold: 7 days) -- overdue for remediation",
    "type": "CSA003",
    "file": ".github/workflows/scorecard.yml",
    "action": "escalate",
    "rule_module": "code_scanning_alerts",
    "severity": "high"
  },
  {
    "reason": "Code-scanning alert hypatia/code_safety/agda_postulate dismissed as 'false positive' -- ensure dismissal is documented and justified",
    "type": "CSA004",
    "file": "proofs/agda/EchoImageFactorizationPropPostulated.agda",
    "action": "review",
    "rule_module": "code_scanning_alerts",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

[github-actions]

🔍 Hypatia Security Scan

Findings: 6 issues detected

Severity	Count
🔴 Critical	0
🟠 High	3
🟡 Medium	3

View findings

[
  {
    "reason": "No test directory or test files found",
    "type": "no_tests",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "flag",
    "rule_module": "honest_completion",
    "severity": "high",
    "deduction": 20
  },
  {
    "reason": "Nominal-only SAST in echo-types: codeql.yml language matrix contains no language present in the repo and lacks `actions`, so CodeQL records zero results on every commit. Remediation: set the CodeQL matrix to `language: actions`.",
    "type": "StaticAnalysis",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "auto_fix",
    "rule_module": "scorecard",
    "severity": "medium",
    "remediation": "Add CodeQL or equivalent SAST workflow.",
    "scorecard_check": "SAST"
  },
  {
    "reason": "Repository has 6 non-main remote branch(es). Policy: single main branch only.",
    "type": "GS007",
    "file": ".",
    "action": "delete_remote_branches",
    "rule_module": "git_state",
    "severity": "medium"
  },
  {
    "reason": "Code scanning (Scorecard): TokenPermissionsID -- Token-Permissions -- 18 day(s) old [STALE]",
    "type": "CSA001",
    "file": ".github/workflows/scorecard.yml",
    "action": "escalate",
    "rule_module": "code_scanning_alerts",
    "severity": "high"
  },
  {
    "reason": "Code-scanning alert TokenPermissionsID (high) at .github/workflows/scorecard.yml is 18 days old (threshold: 7 days) -- overdue for remediation",
    "type": "CSA003",
    "file": ".github/workflows/scorecard.yml",
    "action": "escalate",
    "rule_module": "code_scanning_alerts",
    "severity": "high"
  },
  {
    "reason": "Code-scanning alert hypatia/code_safety/agda_postulate dismissed as 'false positive' -- ensure dismissal is documented and justified",
    "type": "CSA004",
    "file": "proofs/agda/EchoImageFactorizationPropPostulated.agda",
    "action": "review",
    "rule_module": "code_scanning_alerts",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence