v2 (c) Neutral reversal bridge: Echo types gate reversibility with a retained residue (Lean + Rust)

[hyperpolymath]

Implements the v2 (c) Neutral reversal bridge end-to-end (proofs + typechecker + runtime), per ADR-0007 D5/D6. This is the rung that makes Echo types actually gate the language's reversal forms beyond the Safe/group case — the user's core "echo types in the typesystem" ask.

The idea

The reversible { } -> tok token is exactly what unlocks the Neutral tier. A self-referential step like x += x is not total erasure — its original value is recoverable from a retained residue (Bennett's trick). So:

• reverse { } and tokenless reversible { } → Safe-only (no residue to invert from).
• reversible { } -> tok → residue policy: admits Safe + Neutral, rejects only Breaking.
• Self-reference is reclassified Breaking → Neutral. In the addition-only group every overwrite can be tokenised, so Breaking never arises here — it's now reserved for future non-group / idempotent (tropical) systems (D6).

Lean (jtv_proofs/) — lake build green, 0 sorry/admit/axiom

• JtvTheorems: RevOp.execBackwardWithToken + rev_forward_backward_with_token — restoring x from the saved token recovers the full state at every variable, unconditionally, even for self-referential x += x (the case that defeats rev_forward_backward). Plus rev_backward_naive_fails_self_ref — proves the naive - inverse genuinely fails (0 ≠ 1), so the token is necessary.
• JtvEcho: admissibleWithResidue (+_iff), admissible_implies_admissibleWithResidue (Safe-only ⊂ residue), neutral_residue_only, join_admissibleWithResidue, and block soundness blockEcho_admissibleWithResidue / breaking_blocks_residual_reversal.

Rust (crates/jtv-core/) — cargo test + clippy -D warnings green

• echo.rs: self-ref Breaking → Neutral; Echo::admissible_with_residue.
• typechecker.rs: split gate — check_echo_admissible_with_residue for reversible { } -> tok; Safe-only otherwise.
• reversible.rs: RecordedOp::Snapshot records the overwritten value and inverts by restoring it (runtime counterpart of execBackwardWithToken), not the wrong naive subtraction.

Tests (all green)

99 lib + integration tests pass. New: self_reference_is_neutral, block_neutral_when_any_self_reference, residue-admissibility; typechecker admits self-ref with token / rejects without (and reverse{} rejects); runtime residue round-trip recovery test_neutral_self_reference_recovered_via_residue.

Next rung after this: (b) Echo as a first-class function effect; and number-system semantics (gap-005, the D6 tier classification). The DataExpr.neg open tension (D2) also remains.

https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742

---

Generated by Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 54 issues detected

Severity	Count
🔴 Critical	0
🟠 High	27
🟡 Medium	27

View findings

[
  {
    "reason": "No test directory or test files found",
    "type": "no_tests",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper",
    "action": "flag",
    "rule_module": "honest_completion",
    "severity": "high",
    "deduction": 20
  },
  {
    "reason": "Issue in secret-scanner.yml",
    "type": "missing_workflow",
    "file": "secret-scanner.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Workflow executes remote script directly (curl/wget piped to shell). Download, verify checksum/signature, then execute.",
    "type": "download_then_run",
    "file": "proof-regression.yml",
    "action": "verify_download_integrity",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in scorecard.yml",
    "type": "scorecard_wrapper_missing_job_permissions",
    "file": "scorecard.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "unsafe block -- requires SAFETY comment (2 occurrences, CWE-676)",
    "type": "unsafe_block",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper/crates/jtv-cli/src/rsr_check.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "unwrap() without prior check -- DoS via panic (10 occurrences, CWE-754)",
    "type": "unwrap_without_check",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper/crates/jtv-core/benches/interpreter_bench.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "unwrap() without prior check -- DoS via panic (6 occurrences, CWE-754)",
    "type": "unwrap_without_check",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper/crates/jtv-core/benches/parser_bench.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "Download-and-execute pattern (curl|wget pipe to shell) -- verify integrity before execution (3 occurrences, CWE-494)",
    "type": "shell_download_then_run",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper/setup.sh",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "Js.Array2 deprecated -- use Array (3 occurrences)",
    "type": "deprecated_api",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper/vscode-extension/src/Extension.res",
    "action": "search_replace",
    "rule_module": "migration_rules",
    "severity": "high"
  },
  {
    "reason": "Js.Promise deprecated -- use Promise (2 occurrences)",
    "type": "deprecated_api",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper/vscode-extension/src/Extension.res",
    "action": "module_replace",
    "rule_module": "migration_rules",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence