test(c5.1): real-AffineScript-emitted .wasm fixtures + regenerate workflow (closes typed-wasm#35 part 2)

[hyperpolymath]

Summary

Closes the C5.1 ask in typed-wasm#35 part 2 with a 4-fixture corpus of real affinescript-emitted .wasm bytes paired with the .affine sources that produced them. Companion to tests/cross_compat.rs (the synthetic-fixture parity oracle): this suite cross-checks the verifier against bytes a real producer actually emits.

What this adds

• tests/fixtures/c5_real/ — 8 files + README.adoc:

  #	Fixture	Verdict	Exercises
  01	clean_linear	Ok(())	@linear consumed exactly once
  02	shared_borrow_twice	Ok(())	ref Int read twice (allowed)
  03	partial_drop	LinearNotUsed + LinearDroppedOnSomePath	own Int consumed in then-branch only
  04	excl_alias	ExclBorrowAliased	mut Int aliased

  Captured 2026-05-27 against affinescript HEAD 21edc159caee06a930cb7339b3e729ed5627b823, OCaml 4.14.2 opam switch, default affinescript compile options.

• tests/cross_compat_real.rs — 5 tests asserting the verifier reaches the expected verdict on each vendored .wasm. Includes a sanity test that flags any missing fixture file.

• .github/workflows/c5-regenerate.yml — PR-gated regeneration workflow: installs OCaml, checks out affinescript at the pinned SHA, builds the compiler, re-emits each .wasm from source into a scratch dir, and byte-diffs against the vendored bytes. Drift in affinescript codegen surfaces as a failed check with a remediation message. Only runs on PRs touching the fixture directory or the workflow itself (heavy job — not appropriate per-PR).

Why vendored bytes (not build-at-PR-time)

The verifier crate's CI today doesn't build affinescript. Provisioning OCaml + opam + the affinescript deps on every PR would be a heavy gate for what is fundamentally a parity check. Vendored bytes is the standard pattern (wasm-tools, wabt, etc) — fast, auditable, and the regenerate workflow catches drift if affinescript's codegen ever changes.

Coverage

cross_compat.rs       (synthetic) — 10 tests — parity oracle (unchanged)
cross_compat_real.rs  (real)      —  5 tests — cross-check against
                                              real affinescript output

Gaps deferred to follow-ups (documented in fixtures README)

• Duplicate-Linear violation fixture. The affinescript source-level borrow checker correctly rejects double-move; producing a real .wasm with a Linear param loaded twice needs either a source-level escape hatch (none exists) or a hand-built fixture outside C5.1.
• Multi-module fixtures (cross-module Linear-call clean / Linear-twice; isolated vs shared memory pair). Need a multi-module affinescript build harness; tracked separately.

Test plan

• cargo test --test cross_compat_real — 5 pass
• cargo test — 47 pass (42 prior + 5 new)
• Local round-trip: each .affine source → affinescript compile → .wasm → verify_from_module → expected verdict
• CI green on this PR
• c5-regenerate workflow validates the pinned SHA actually emits these bytes (first regenerate run is the proof)

Refs typed-wasm#35 (this is part 2)
Refs typed-wasm#34 (parent issue)

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 23 issues detected

Severity	Count
🔴 Critical	6
🟠 High	8
🟡 Medium	9

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Action actions/upload-artifact@v4 needs attention",
    "type": "unpinned_action",
    "file": "release.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action actions/download-artifact@v4 needs attention",
    "type": "unpinned_action",
    "file": "release.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "believe_me undermines formal verification (1 occurrences, CWE-704)",
    "type": "believe_me",
    "file": "/home/runner/work/typed-wasm/typed-wasm/src/abi/TypedWasm/ABI/SessionProtocol.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/typed-wasm/typed-wasm/src/abi/TypedWasm/ABI/SessionProtocol.idr",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "believe_me undermines formal verification (1 occurrences, CWE-704)",
    "type": "believe_me",
    "file": "/home/runner/work/typed-wasm/typed-wasm/src/abi/TypedWasm/ABI/Echo.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/typed-wasm/typed-wasm/src/abi/TypedWasm/ABI/Echo.idr",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "believe_me undermines formal verification (1 occurrences, CWE-704)",
    "type": "believe_me",
    "file": "/home/runner/work/typed-wasm/typed-wasm/src/abi/TypedWasm/ABI/ResourceCapabilities.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/typed-wasm/typed-wasm/src/abi/TypedWasm/ABI/ResourceCapabilities.idr",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "believe_me undermines formal verification (1 occurrences, CWE-704)",
    "type": "believe_me",
    "file": "/home/runner/work/typed-wasm/typed-wasm/src/abi/TypedWasm/ABI/ModuleIsolation.idr",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence