feat(v2-grammar): re-port phases E/F-H/I/J onto upstream extern API (refs #80)

[hyperpolymath]

Refs #80.

Re-implements the genuinely-net-new v2-grammar phases on the upstream Extern { abi, items, span } + cross-module-registry API (Phase D already landed in #78; hello.eph is v2-only and dropped per the issue).

Phases

• E — function-decl annotations + tuple/let-pair destructuring
• F — implicit in (let-lin chains); legacy explicit in still compiles
• G/H — abstract extern types, Unit alias, Bytes → i32 handle
• I — cross-module imports via new src/ephapax-cli/src/import_resolver.rs
• J — bridge.eph + hypatia-port end-to-end compile

Tests

All green, no regressions:

• phase_e 4 · phase_f 4 · phase_gh 3 · phase_i 1 · phase_j 1
• parser 61 · typing 73 · desugar 18 · surface 9 · ephapax-cli integration/conformance/contract/property/wasm suites

Recovery note

This work existed only as uncommitted working-tree state when the local .git object store corrupted (19 zero-byte loose objects + corrupt index, likely a WSL crash mid-write). History was repaired from origin (all branches were pushed), the index rebuilt from disk, and hypatia-scan.yml/Cargo.lock kept at the canonical #82 baseline rather than the pre-sync working-tree version. A backup of the corrupt .git is archived under .claude/.

Ref branch wip/v2-grammar-2026-05-16 preserved on origin. Companion to hyperpolymath/standards#66.

Joint-close note: #80 carries major + requirements-target — per the estate joint-close rule this PR uses Refs #80 (NOT Closes) and must NOT auto-close #80 on merge. Whoever squash-merges MUST ensure the final squash commit message says Refs #80 (the original commit headline still reads "(closes #80)" — strip that keyword in the merge UI). #80 closes only on explicit user agreement, mirrored via the "Awaiting joint close" board column.

🤖 Generated with Claude Code

[hyperpolymath]

⚠️ Joint-close policy fix applied (cross-session). This PR's title and body said Closes #80, but #80 is labelled major + requirements-target. Per the estate joint-close rule that auto-closes a requirements-target issue on merge, which is not allowed. I changed the title and body to Refs #80.

Action required at merge: the underlying commit headline still reads (closes #80). On squash-merge GitHub's default message concatenates commit messages, so the closing keyword can still land on main and auto-close #80. Whoever merges must edit the squash commit message in the merge UI so it reads Refs #80 (no closing keyword). #80 stays OPEN; it closes only on explicit user agreement, mirrored via the "Awaiting joint close" board column. The implementation/tests in this PR are not in question — only the close semantics.

[github-actions]

🔍 Hypatia Security Scan

Findings: 27 issues detected

Severity	Count
🔴 Critical	7
🟠 High	5
🟡 Medium	15

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Issue in quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Admitted leaves proof hole (1 occurrences, CWE-704)",
    "type": "admitted",
    "file": "/home/runner/work/ephapax/ephapax/formal/Semantics.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "Coq admit tactic leaves goal unproven (2 occurrences, CWE-704)",
    "type": "coq_admit_tactic",
    "file": "/home/runner/work/ephapax/ephapax/formal/Semantics.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "believe_me undermines formal verification (1 occurrences, CWE-704)",
    "type": "believe_me",
    "file": "/home/runner/work/ephapax/ephapax/src/formal/Ephapax/Formal/RegionLinear.idr",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "assert_total bypasses totality checker (1 occurrences, CWE-704)",
    "type": "assert_total",
    "file": "/home/runner/work/ephapax/ephapax/src/formal/Ephapax/Formal/RegionLinear.idr",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "expect() in hot path (1 occurrences, CWE-754)",
    "type": "expect_in_hot_path",
    "file": "/home/runner/work/ephapax/ephapax/src/ephapax-repl/src/lib.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "from_raw constructs types from raw pointers without safety checks (1 occurrences, CWE-676)",
    "type": "from_raw",
    "file": "/home/runner/work/ephapax/ephapax/src/ephapax-vram-cache/src/lib.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "unwrap() without prior check -- DoS via panic (8 occurrences, CWE-754)",
    "type": "unwrap_without_check",
    "file": "/home/runner/work/ephapax/ephapax/src/ephapax-vram-cache/benches/cache_bench.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "expect() in hot path (5 occurrences, CWE-754)",
    "type": "expect_in_hot_path",
    "file": "/home/runner/work/ephapax/ephapax/src/ephapax-typing/src/lib.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "unsafe block -- requires SAFETY comment (3 occurrences, CWE-676)",
    "type": "unsafe_block",
    "file": "/home/runner/work/ephapax/ephapax/src/ephapax-interp/src/lib.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence