feat: EchoResidueCell — Agda mirror of 007's Holding/Spent once-only discipline

[hyperpolymath]

What

A new module proofs/agda/EchoResidueCell.agda — the Agda mirror of 007's ResidueCell (Holding/Spent) once-only reversal discipline, the operational half that EchoReversibilityBridge (#249) deferred as "runtime bookkeeping".

007's Idris2 spec (EchoResidueLinear.idr) enforces once-only via the linear quantity (1 e : Echo f y). Agda has no such quantity under --safe, so this module enforces it via the state machine instead — which is exactly how 007's runtime (the rung-3b residue cell) does it.

The mirror

This module	Idris EchoResidueLinear.idr
ResidueCell f y = holding (Echo f y) | spent	data ResidueCell … = Holding (1 e) | Spent
takeForReverse : ResidueCell f y → Maybe A	takeForReverse … : Maybe a
consume : ResidueCell f y → ResidueCell f y (Holding→Spent)	the cell-state effect of reverse
holding-reverses	holdingReverses
spent-does-not-reverse	spentDoesNotReverse
once-only — takeForReverse (consume c) ≡ nothing	the (1 e) linear-consumption guarantee

once-only is the headline: after consume, a residue replays at most once — the state-machine form of linear consumption, and the operational content of 007's cross-handler once-only property that the rung-3b static check could only approximate by presence. All proofs are refl (definitional).

Honest scope

Captures the once-per-cell discipline. It does not model linear NON-DUPLICATION (nothing stops a caller copying a holding cell before consuming) — that needs the (1 e) quantity / an @0-style erasure encoding, and remains the documented next slice. Stated explicitly in the module preamble and the MAP.adoc scope note.

Discipline

• --safe --without-K, zero postulates, no funext.
• Wired into All.agda (next to EchoReversibilityBridge); 7 headlines pinned in Smoke.agda.
• Classified up front in echo-kernel-note.adoc (Tier 2) + MAP.adoc (the 007-bridge section) — sh scripts/kernel-guard.sh PASS (applying the lesson from feat: EchoReversibilityBridge — discharge 007 L10 reversibility obligations #249).
• Verified on latest main: EchoResidueCell.agda, Smoke.agda, and All.agda all agda --safe --without-K exit 0 (captured locally).

🤖 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