Slice 2: make chapeliser provably-real — CI machine-checks proofs/FFI/Chapel + honest status

[hyperpolymath]

Follow-on to base camp (#26, merged). Goal of this slice: move chapeliser from
"asserted in prose" to machine-verified, and make the docs honest about what
is and isn't checked today.

Provable-real — .github/workflows/provable.yml

The Rust CLI/codegen is already green (63 tests via rust-ci.yml). This adds a
new workflow that verifies everything outside Rust:

Job	What it proves
idris2-proofs	idris2 --check type-checks Types.idr, Layout.idr, Foreign.idr (the dependent-type ABI proofs)
zig-ffi	zig build test compiles + runs the Zig FFI reference impl (Zig 0.14)
codegen-drift	regenerates the golden sample and diffs against the committed tree (fails on drift)
chapel-golden	compiles and runs the generated Chapel via real chpl, asserting 8/8 items conserved

Golden sample — examples/golden/

A minimal end-to-end fixture that closes the STATE.a2ml action "generate +
compile + run":

• echo.toml — deliberately per-item/merge so the generated Chapel pulls in
  no optional modules (no BlockDist/DynamicIters/AtomicObjects) → small,
  stable compile surface.
• generated/ — committed codegen output (reviewable + drift-checked).
• ffi_stub.c — ~60-line C echo implementation of the 12 c_* functions so the
  Chapel can be linked and run without user code.

Honest status — stop claiming what isn't checked yet

• ROADMAP.adoc: Phase 1 (COMPLETE) → (IMPLEMENTED — verification gated in CI); new Phase 1b tracks the four CI jobs (each flips [x] only when green); dropped "compilable" from the bare codegen bullet.
• Test-count fix: the old 15 tests (6 unit + 8 integration + 1 doc) was wrong — actual is 63 (22 + 40 + 1).
• README.adoc: Idris2 "Formal proofs that…" → "proof obligations, machine-checked in CI"; corrected source paths (src/interface/abi, src/interface/ffi); honest pre-alpha Status paragraph.
• STATE.a2ml: blockers / next-actions / maintenance now reflect CI-gated verification (last-result = warn until provable.yml is green).

Why CI is the verifier (not local)

The idris2 / zig / chpl toolchains aren't installable in the dev sandbox
(ziglang.org and the GitHub releases API are network-blocked here; building
idris2 from source is sandbox-restricted). So GitHub runners are the verifier.
Until provable.yml is green, these artifacts are "written", not "verified" —
and the docs now say exactly that. Kept as a draft for that reason: driving
the four jobs to green is the acceptance gate, and a first run may surface real
fixes (e.g. Idris2 DecEq totality, Chapel Time/reduce API specifics) — that
iteration is the "make it real" work.

Follow-up (not blocking): pin action/image refs (actions/checkout,
mlugg/setup-zig, chapel/chapel, idris2-pack) to SHAs per estate policy
once the tags are confirmed working.

🤖 Generated with Claude Code

https://claude.ai/code/session_01Mbq6yKF9RhFai6EQ7WqKhQ

---

Generated by Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 62 issues detected

Severity	Count
🔴 Critical	1
🟠 High	9
🟡 Medium	52

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action actions/checkout@v4 needs attention",
    "type": "unpinned_action",
    "file": "provable.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action actions/checkout@v4 needs attention",
    "type": "unpinned_action",
    "file": "provable.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action mlugg/setup-zig@v1 needs attention",
    "type": "unpinned_action",
    "file": "provable.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action actions/checkout@v4 needs attention",
    "type": "unpinned_action",
    "file": "provable.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action actions/checkout@v4 needs attention",
    "type": "unpinned_action",
    "file": "provable.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in boj-build.yml",
    "type": "missing_timeout_minutes",
    "file": "boj-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_timeout_minutes",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

[github-actions]

🔍 Hypatia Security Scan

Findings: 54 issues detected

Severity	Count
🔴 Critical	1
🟠 High	9
🟡 Medium	44

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action mlugg/setup-zig@v1 needs attention",
    "type": "unpinned_action",
    "file": "provable.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in boj-build.yml",
    "type": "missing_timeout_minutes",
    "file": "boj-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_timeout_minutes",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence