Skip to content

feat(typecheck): non-copyable echoes are linear — overwrite/drop discipline#55

Merged
hyperpolymath merged 1 commit into
mainfrom
claude/confident-shannon-xf0Td
Jun 4, 2026
Merged

feat(typecheck): non-copyable echoes are linear — overwrite/drop discipline#55
hyperpolymath merged 1 commit into
mainfrom
claude/confident-shannon-xf0Td

Conversation

@hyperpolymath

Copy link
Copy Markdown
Owner

Summary

Implements the echo↔reversibility language feature you approved (design: overwrite/drop discipline; scope: echoes). It type-enforces the symmetry the Idris bridge proved — reversible ⟺ no residue; irreversible ⟺ an echo — so a residue can no longer be silently thrown away.

A non-copyable echo is now linear (consumed exactly once):

  • the existing affine rule already forbade a second use;
  • this adds the other half — it must be consumed (projected via echo_visible/echo_witness) at least once before it is reassigned (overwrite) or goes out of scope (drop).

Discarding a non-copyable residue without consuming it is now a type error: "an irreversible step must account for an echo of what it loses."

What changed

  • lib/typecheck.ml — a live_echoes tracker beside affine_used: binding a non-copyable echo arms it; using/projecting consumes it; SAssign and function-exit raise if a still-live residue would be discarded; SIf/SForRange snapshot it like the affine set.
  • Scope & boundary (deliberately narrow, still "no rhino"): non-copyable echo bindings only. Copyable echoes (echo[i64,i64]) and the reversible primitives (incr/decr/swap/^=) are exempt — they lose nothing. Echo still does not participate in reversibility balancing; the connection is one-directional (loss ⇒ must-capture), not a new reversibility mechanism. Generalising to other non-copyable carriers (structs/arrays) is a possible follow-up.
  • Tests — +3 conformance cases: drop without consume rejected, overwrite live value rejected, overwrite after consume ok. Suite 24 → 27, all green. Existing programs are unaffected (verified up front: nothing in the tests or examples reassigns or drops a non-copyable echo).
  • docs/echo-alignment.md — records the landed discipline + its boundary.

Verify

dune build && dune runtest   # 27 conformance tests

(Idris ABI proofs untouched; the ci.yml gate from #52 builds + type-checks them on this PR too.)

🤖 Draft — opened for review.

https://claude.ai/code/session_01GJatEm2TVFSTBEkKXmserJ


Generated by Claude Code

…ipline

Implements the echo<->reversibility connection in the constrained-form type
checker (design: "overwrite/drop discipline", scope: echoes). A non-copyable
echo is now LINEAR -- consumed exactly once. The existing affine rule already
forbade a second use; this adds the other half: it must be consumed (its
residue projected via echo_visible/echo_witness) AT LEAST once before it is

  - reassigned (overwrite), or
  - allowed to go out of scope (drop).

Discarding a residue without consuming it is a type error -- the type-level
form of "an irreversible step must account for an echo of what it loses".

- lib/typecheck.ml: `live_echoes` tracker beside `affine_used`; binding arms it,
  use/projection consumes it, reassignment and function-exit check it; branches
  and loops snapshot it like the affine set.
- Scope/boundary: non-copyable echo bindings only. Copyable echoes
  (echo[i64,i64]) and reversible primitives (incr/decr/swap/^=) are exempt --
  they lose nothing. Echo still does NOT participate in reversibility balancing
  (the connection is one-directional, loss => must-capture; "no rhino" intact).
- tests: +3 conformance cases (drop rejected; overwrite-live rejected;
  overwrite-after-consume ok). Suite 24 -> 27, all green; existing programs
  unaffected (verified: nothing reassigns or drops a non-copyable echo).
- docs/echo-alignment.md: records the landed discipline.

https://claude.ai/code/session_01GJatEm2TVFSTBEkKXmserJ
@github-actions

github-actions Bot commented Jun 4, 2026

Copy link
Copy Markdown

🔍 Hypatia Security Scan

Findings: 55 issues detected

Severity Count
🔴 Critical 6
🟠 High 4
🟡 Medium 45

⚠️ Action Required: Critical security issues found!

View findings
[
  {
    "reason": "Issue in governance.yml",
    "type": "missing_timeout_minutes",
    "file": "governance.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in hypatia-scan.yml",
    "type": "missing_timeout_minutes",
    "file": "hypatia-scan.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in mirror.yml",
    "type": "missing_timeout_minutes",
    "file": "mirror.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in scorecard.yml",
    "type": "missing_timeout_minutes",
    "file": "scorecard.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in secret-scanner.yml",
    "type": "missing_timeout_minutes",
    "file": "secret-scanner.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in instant-sync.yml",
    "type": "secret_action_without_presence_gate",
    "file": "instant-sync.yml",
    "action": "peter-evans/repository-dispatch",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Repository has 5 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): SASTID -- SAST -- 0 day(s) old",
    "type": "CSA001",
    "file": "no file associated with this alert",
    "action": "review",
    "rule_module": "code_scanning_alerts",
    "severity": "medium"
  },
  {
    "reason": "Code scanning (Scorecard): TokenPermissionsID -- Token-Permissions -- 0 day(s) old",
    "type": "CSA001",
    "file": ".github/workflows/hypatia-scan.yml",
    "action": "update",
    "rule_module": "code_scanning_alerts",
    "severity": "high"
  },
  {
    "reason": "Code scanning (Scorecard): TokenPermissionsID -- Token-Permissions -- 0 day(s) old",
    "type": "CSA001",
    "file": ".github/workflows/scorecard.yml",
    "action": "update",
    "rule_module": "code_scanning_alerts",
    "severity": "high"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

@hyperpolymath hyperpolymath marked this pull request as ready for review June 4, 2026 05:49
@hyperpolymath hyperpolymath merged commit b2e58ca into main Jun 4, 2026
21 checks passed
@hyperpolymath hyperpolymath deleted the claude/confident-shannon-xf0Td branch June 4, 2026 05:49
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants