diff --git a/.github/workflows/abi-verify.yml b/.github/workflows/abi-verify.yml new file mode 100644 index 00000000..cb62e025 --- /dev/null +++ b/.github/workflows/abi-verify.yml @@ -0,0 +1,57 @@ +# SPDX-License-Identifier: PMPL-1.0-or-later +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# abi-verify.yml — machine-checks the Ephapax Rust↔SPARK ABI seam. +# +# The seam (src/abi/Ephapax/ABI/{Types,Foreign,Invariants}.idr) states +# the correctness-critical invariants E1–E6 (see PROOF-NEEDS.md and +# RUST-SPARK-STANCE.adoc). Some properties have discharged proofs in +# the broader formalisation (cited from Invariants.idr — e.g. +# `splitLinearCoverage`, `noEscapeTheorem`); the rest are explicit +# erased OWED obligations. +# +# This gate exists so the discharged proofs cannot silently regress +# and an OWED postulate cannot quietly become a `believe_me`. Mirrors +# the proof-of-work `abi-verify.yml` (snazzybucket/idris2 container, +# the estate-standard image). HARD GATE. + +name: ABI Seam Verification + +on: + pull_request: + paths: + - 'src/abi/**' + - '.github/workflows/abi-verify.yml' + push: + branches: [main] + paths: + - 'src/abi/**' + +permissions: + contents: read + +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +jobs: + idris2-abi: + name: Idris2 ABI seam (ephapax-abi.ipkg) + runs-on: ubuntu-latest + container: + image: snazzybucket/idris2:latest # estate-standard Idris2 image + steps: + - name: Checkout repository + uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4 + + - name: Build (typecheck) the ABI seam + working-directory: src/abi + run: | + idris2 --version + # --build typechecks every module in the .ipkg in dependency + # order. A real regression (ill-typed lemma, a discharged + # proof that stops reducing, a stray `?hole`/`believe_me`) + # fails here. The intentional erased OWED postulates are + # well-typed and do NOT fail the build — they are tracked in + # PROOF-NEEDS.md, not hidden. + idris2 --build ephapax-abi.ipkg diff --git a/RUST-SPARK-STANCE.adoc b/RUST-SPARK-STANCE.adoc new file mode 100644 index 00000000..b1c87612 --- /dev/null +++ b/RUST-SPARK-STANCE.adoc @@ -0,0 +1,182 @@ +// SPDX-License-Identifier: PMPL-1.0-or-later += Rust/SPARK Stance — ephapax +:toc: macro +:toclevels: 2 + +toc::[] + +== Summary + +This repository implements a dyadic-linear programming language. The +implementation is a 19-crate Rust pipeline (surface parser → discipline +checker → IR → WASM backend, with a Zig FFI token buffer). Per the +estate language policy +(`standards/rhodium-standard-repositories/spec/LANGUAGE-POLICY.adoc` +§Terminology), *"Rust" means "Rust/SPARK"*: Rust is the primary +implementation language now, but the project is *designed to admit +SPARK/Ada verification modules* across a stable, Idris2-typed +boundary, with Zig as the FFI layer. Rust here is never the ABI/API/FFI +layer. + +Before this PR (2026-05-20) the crate had a `formal/` Coq metatheory + +a `src/formal/` Idris2 region/linearity metatheory + a `src/abi/` +directory that did not exist — no named seam, no SPARK admission path, +no stance doc. The `src/abi/` package below brings the project into +structural compliance; the remaining proof work is tracked in +`PROOF-NEEDS.md` and standards#134. + +== What is correctness-critical here + +This is a programming language whose claimed properties are *linear-type +consumption*, *region safety*, *GC-freedom*, and *type preservation*. +The boundaries where these can be silently broken are: the discipline +check (typing pass), the IR lowering (qualifier erasure), the WASM +backend (lowering to a different operational model), and the Zig FFI +(non-typed integer marshalling). + +[cols="1,2,3",options="header"] +|=== +| Audit framing | Real counterpart | Where in code + +| Type preservation +| `well_typed t T && t ⇒ t' → well_typed t' T` +| `formal/Semantics.v::preservation` (currently **`Admitted`** — + earlier in-file comment claiming "Qed, closed 2026-04-27" was + unsubstantiated; `coqc` rejects the proof script with remaining + open goals — see ephapax#92). + +| Linear consumption +| Every linear binding used exactly once across a context split +| `src/formal/Ephapax/Formal/Qualifier.idr::splitLinearCoverage` + (DISCHARGED, MERGED 2026-05-19 via ephapax#85 — head/position form). + Cross-control-flow form (conditionals, pattern-match arms, region + exit) OWED. + +| Region safety +| Values scoped to `r` never escape `r` at runtime +| `src/formal/Ephapax/Formal/RegionLinear.idr::noEscapeTheorem` + (DISCHARGED — real proof, narrow form: `NoRegionInType r (Scoped r a) + -> Void`). Operational form OWED. + +| GC-freedom +| No runtime collector needed — every heap value's lifetime is + statically bounded by an enclosing region +| `src/formal/Ephapax/Formal/RegionLinear.idr::noGCExtract` + (**VACUOUS** — body is `(ne, lc)`, just returns its inputs; flagged + in seam, real content OWED). + +| WASM compilation correctness +| Lowering preserves typing + semantics +| `src/ephapax-wasm/` (no formalisation today — entire compiler + metatheory OWED). +|=== + +== The seam + +[cols="1,3",options="header"] +|=== +| File | Role + +| `src/abi/Ephapax/ABI/Types.idr` +| Idris2 boundary types — faithful total models of `Qual`, `Ty`, `Term`, + `CtxEntry`/`TypeCtx`, `SExpr`, `WasmExpr`, `RegionId`. Constructor + order is ABI-significant and matches the Rust enums in + `src/ephapax-syntax/`, `src/ephapax-typing/`, `src/ephapax-ir/`, + `src/ephapax-wasm/`. + +| `src/abi/Ephapax/ABI/Invariants.idr` +| Type-level statements of invariants E1–E6. **E2 head-form is + DISCHARGED** at `Ephapax.Formal.Qualifier.splitLinearCoverage` + (cited). **E3 narrow-form is DISCHARGED** at + `Ephapax.Formal.RegionLinear.noEscapeTheorem` (cited). E1 + (preservation) is OWED on the Coq side and remains `Admitted`. + E2 control-flow generalisation, E3 operational form, E4 + (no-runtime-GC), E5 (WASM compilation), E6 (IR lowering) are stated + as erased postulates so the obligations are explicit and discoverable. + Authoritative per-ID status: `PROOF-NEEDS.md` § Invariant register. + +| `src/abi/Ephapax/ABI/Foreign.idr` +| Zig/WASM-FFI boundary: u32/i32 range obligations for marshalling + (function indices, local indices, literal magnitudes), the stable + C-ABI `CompileResult` codes, and the contract tying a `CompileOk` + return to an E5 `WasmTyped` certificate. + +| `src/abi/ephapax-abi.ipkg` +| Idris2 package mapping the `Ephapax.ABI.*` namespace to the source + tree. Without this package the modules would not load + (`import Ephapax.ABI.Types` would fail), so the seam would be + structurally present but never machine-checked. +|=== + +The seam is machine-checked: `idris2 --build ephapax-abi.ipkg` (run +from `src/abi/`) typechecks all three modules, and a future +`.github/workflows/abi-verify.yml` (filed alongside this seam) enforces +it on every change to `src/abi/**`. The stated obligations therefore +cannot silently regress, and an OWED postulate cannot quietly become +a `believe_me`. + +== Bounds encoding choice (Integer, not Nat) + +`Foreign.idr` uses `Integer` for the u32/i32 bounds, not `Nat`. This +is a deliberate carry-over from `proof-of-work#63`: a `Nat` constant +of `2^32` placed under an `LT n bound` predicate inside a data +constructor's type forces the Idris2 0.8.0 elaborator to reduce the +literal to ~4×10⁹ `S` constructors during the data declaration's +elaboration, which hangs `--build` indefinitely. The boundary +predicate is `So (natToInteger n < bound)` instead — propositionally +equivalent (the Rust `u32` round-trips to precisely the Nats with +`natToInteger n < 2^32`) but without unary expansion. Do not rewrite +back to `LT n bound`. + +== SPARK/Ada admission path + +The boundary is the Idris2 seam above. A future SPARK/Ada +re-implementation of any of: + +* the discipline checker (would discharge a refined E2), +* the IR lowering (would discharge E6), +* the WASM backend (would discharge E5), + +sits on the far side of `Foreign.compileOkImpliesWasmTyped` without +changing the contract: it must return `CompileOk` only when it can +produce a `WasmTyped (compile t) T` certificate. No SPARK code exists +yet; the seam exists so it *can* be added without redesign, which is +exactly what §Terminology requires of a "designed to admit SPARK/Ada" +Rust project. + +== Honest gaps + +* `formal/Semantics.v::preservation` is **`Admitted`** — the proof + script at L3215–L3326 leaves residual open goals (`coqc` 8.18.0 + rejects `Qed.` with "Attempt to save an incomplete proof"). PR#87 + (earlier today) propagated an in-file comment's "Qed, closed + 2026-04-27" claim into ROADMAP + PROOF-NEEDS without running the + build; **the comment was the lie**. ephapax#92 (open) reverts that + doc drift and marks the source `Admitted.` honestly so the Coq CI + goes green. +* `src/formal/Ephapax/Formal/RegionLinear.idr::regionSafetyExtract` + and `noGCExtract` are **vacuous wrappers** — body is the input + unchanged (`= ne`, `= (ne, lc)`). The proofs are sound (no escape + hatches) but the *content* is vacuous: they don't establish region + safety or GC-freedom, they just extract a witness already given. + The honest seam invariants E3 (operational region-no-escape) and + E4 (no-runtime-GC) are therefore OWED, not "complete". +* No formalisation of WASM lowering exists anywhere in the repo. E5 + is the highest-leverage compiler-correctness gap. +* `ephapax-parse-tests.ipkg` fails on origin/main + (`testLexPositions` / `parseWithBuf` undefined). Independent of the + seam, flagged here for awareness — separate issue. + +== References + +* `standards/rhodium-standard-repositories/spec/LANGUAGE-POLICY.adoc` + §Terminology, §"Rust is never the ABI" +* `PROOF-NEEDS.md` (this repo) — invariant ledger and priorities +* `ROADMAP.adoc` (this repo) — Coq/Idris2 dual formalisation status +* Estate exemplar seam: `proof-of-work/src/abi/{Types,Foreign,Invariants}.idr` + + `RUST-SPARK-STANCE.adoc` +* standards#134 — estate proof-debt sub-issue tracking ephapax +* ephapax#85 — `splitLinearCoverage` discharge (MERGED 2026-05-19) +* ephapax#88 — `idris2/src/*.idr` SPDX headers (OPEN) +* ephapax#92 — `Qed.` → `Admitted.` on `preservation` (OPEN — companion + to this PR; the doc-honesty fix this stance doc cites) diff --git a/src/abi/Ephapax/ABI/Foreign.idr b/src/abi/Ephapax/ABI/Foreign.idr new file mode 100644 index 00000000..15a9628d --- /dev/null +++ b/src/abi/Ephapax/ABI/Foreign.idr @@ -0,0 +1,132 @@ +||| SPDX-License-Identifier: PMPL-1.0-or-later +||| Ephapax ABI: FFI Boundary Obligations +||| +||| The Zig/WASM-FFI side of the Ephapax ABI seam. The Rust pipeline +||| uses fixed-width integers across two boundaries: +||| 1. Zig FFI token buffer (`Ephapax.Parse.ZigBuffer` in the Idris2 +||| Parse package) — `u32` offsets/lengths into the input source. +||| 2. WASM lowering (`src/ephapax-wasm/`) — `u32` function indices, +||| `u32` local indices, `i32` literal values. +||| +||| The Idris2 model in Types.idr uses `Nat` for these. This module +||| states the range obligations that the boundary must discharge when +||| marshalling between the Rust representation and the typed model, +||| plus the C-ABI result codes any FFI entry-point should expose. +||| +||| Per LANGUAGE-POLICY.adoc §Terminology and §"Rust is never the ABI": +||| the boundary is Idris2 (this seam) + Zig (FFI). Rust/SPARK is the +||| application logic on one side; a future SPARK/Ada code generator +||| could sit on the other side of THIS contract without changing it. + +module Ephapax.ABI.Foreign + +import Ephapax.ABI.Types +import Ephapax.ABI.Invariants +import Data.Nat +import Data.So + +%default total + +-------------------------------------------------------------------------------- +-- Fixed-width range obligations +-- +-- Bounds are `Integer`, not `Nat` — the proof-of-work `Foreign.idr` +-- learned the hard way (PR proof-of-work#63, 2026-05-20) that a `Nat` +-- bound of 2^32 forces the Idris2 0.8.0 data-constructor elaborator to +-- reduce the literal under `LT n bound` inside the constructor's type, +-- which expands ~4×10^9 `S` ctors and hangs `--build`. The boundary +-- predicate is therefore expressed as `So (natToInteger n < bound)`, +-- propositionally equivalent (the Rust `u32` round-trips to precisely +-- the Nats with `natToInteger n < 2^32`) but does not trigger unary +-- expansion. Do not rewrite back to `LT n bound`. +-------------------------------------------------------------------------------- + +||| u32 upper bound (2^32). WASM function indices, local indices and +||| Zig token-buffer offsets/lengths crossing the FFI must fit; the +||| Rust types guarantee this, the Idris2 Nat model does not, so the +||| obligation is made explicit here. +public export +u32Max : Integer +u32Max = 4294967296 + +||| Proof-carrying "this Nat fits in a u32". +public export +data InU32 : Nat -> Type where + MkInU32 : (n : Nat) -> So (natToInteger n < Foreign.u32Max) -> InU32 n + +||| i32 signed-range upper bound (2^31). WASM `i32.const` literals must +||| fit; the magnitude bound below is the absolute value (sign is +||| tracked separately by the producer). +public export +i32Max : Integer +i32Max = 2147483648 + +public export +data InI32Magnitude : Nat -> Type where + MkInI32Mag : (n : Nat) -> So (natToInteger n < Foreign.i32Max) -> InI32Magnitude n + +||| A WASM function index is FFI-marshalable iff it fits in u32. +public export +MarshalableFuncIdx : FuncIdx -> Type +MarshalableFuncIdx fi = InU32 fi + +-------------------------------------------------------------------------------- +-- C-ABI result codes for compile/typecheck entry points +-------------------------------------------------------------------------------- + +||| Stable C integer result for a typecheck/compile call across the FFI. +||| Constructor order is ABI-significant. +public export +data CompileResult : Type where + CompileOk : CompileResult -- typecheck + lowering succeeded + CompileTypeError : CompileResult -- discipline check rejected the term + CompileRegionError : CompileResult -- region-safety check rejected the term + CompileLowerError : CompileResult -- IR/WASM lowering failed (should never + -- happen on a well-typed term — E6) + CompileMalformed : CompileResult -- input failed surface parse + +public export +compileResultToInt : CompileResult -> Nat +compileResultToInt CompileOk = 0 +compileResultToInt CompileTypeError = 1 +compileResultToInt CompileRegionError = 2 +compileResultToInt CompileLowerError = 3 +compileResultToInt CompileMalformed = 4 + +public export +compileResultFromInt : Nat -> Maybe CompileResult +compileResultFromInt 0 = Just CompileOk +compileResultFromInt 1 = Just CompileTypeError +compileResultFromInt 2 = Just CompileRegionError +compileResultFromInt 3 = Just CompileLowerError +compileResultFromInt 4 = Just CompileMalformed +compileResultFromInt _ = Nothing + +||| Round-trip proof for the result-code mapping (the one property +||| fully dischargeable here, by case analysis). +public export +compileResultRoundTrip : + (r : CompileResult) -> compileResultFromInt (compileResultToInt r) = Just r +compileResultRoundTrip CompileOk = Refl +compileResultRoundTrip CompileTypeError = Refl +compileResultRoundTrip CompileRegionError = Refl +compileResultRoundTrip CompileLowerError = Refl +compileResultRoundTrip CompileMalformed = Refl + +-------------------------------------------------------------------------------- +-- The FFI contract any compile entry-point must honour +-------------------------------------------------------------------------------- + +||| The boundary obligation: a `CompileOk` result handed back across the +||| FFI must be backed by an E5 `WasmTyped (compile t) T` certificate +||| for the submitted term. This ties the C-ABI return value to the +||| Idris2 compiler-correctness statement. The Rust does not yet +||| *produce* the witness (PROOF-NEEDS.md E5); the type records exactly +||| what is owed. +public export +0 compileOkImpliesWasmTyped : + (g : TypeCtx) -> (t : Term) -> (T : Ty) -> + (r : CompileResult) -> + r = CompileOk -> + WellTyped g t T -> + WasmTyped (compile t) T diff --git a/src/abi/Ephapax/ABI/Invariants.idr b/src/abi/Ephapax/ABI/Invariants.idr new file mode 100644 index 00000000..409e8a3b --- /dev/null +++ b/src/abi/Ephapax/ABI/Invariants.idr @@ -0,0 +1,206 @@ +||| SPDX-License-Identifier: PMPL-1.0-or-later +||| Ephapax ABI: Correctness-Critical Invariants +||| +||| Type-level statements of the invariants the Ephapax compiler +||| pipeline must uphold at its trust boundaries (typing pass, IR +||| lowering, WASM emit, FFI marshal). Each invariant is stated as an +||| Idris2 type/proposition. Where the property is a discharged proof +||| elsewhere in the repo, it is cited; where it is OWED or PARTIAL, +||| it is marked as an erased postulate and tracked in PROOF-NEEDS.md. +||| +||| Naming: this seam lists the invariants whose breach silently +||| corrupts compiled programs — the language-implementation analogue +||| of proof-of-work's I1–I7 verifier-soundness register. +||| +||| Authoritative per-ID status: PROOF-NEEDS.md § Invariant register. +||| This file is the type-level statement of those obligations. + +module Ephapax.ABI.Invariants + +import Ephapax.ABI.Types + +%default total + +-------------------------------------------------------------------------------- +-- E1. Type preservation +-- +-- Source: formal/Semantics.v `preservation`, +-- formal/Typing.v step-respects-typing supporting lemmas. +-- +-- Statement (informal): if `well_typed t T` and `t ⇒ t'` then +-- `well_typed t' T`. Currently `Admitted` in Coq — the proof script at +-- formal/Semantics.v L3215–L3326 leaves residual open goals +-- (`coqc` 8.18.0 rejects the `Qed.` with "Attempt to save an incomplete +-- proof"). This Idris2 seam states the obligation; discharge happens on +-- the Coq side. +-------------------------------------------------------------------------------- + +||| Abstract typing relation. The Coq formalisation `formal/Typing.v` +||| carries the inductive `well_typed` (`HasType`) judgement; this is +||| its seam-level abstraction. +public export +data WellTyped : TypeCtx -> Term -> Ty -> Type where + -- Intentionally abstract: the seam states the obligation, not the + -- judgement's rules (those live in formal/Typing.v). A SPARK/Ada side + -- consuming the seam only needs the *interface* of `WellTyped`, not + -- its constructors. + +||| Abstract one-step reduction. Mirrors the Coq `step` relation in +||| formal/Semantics.v. Like WellTyped, declared abstractly at the seam. +public export +data Step : Term -> Term -> Type where + +||| E1 (OWED — Coq side). If `t` is well-typed at `T` in `g` and steps +||| to `t'`, then `t'` is also well-typed at `T` in `g`. **The Coq +||| `preservation` theorem in formal/Semantics.v is currently Admitted** +||| (see PROOF-NEEDS.md L1–L18). The Idris2 seam states the obligation +||| so a SPARK/Ada implementation sees what is owed. +public export +0 typePreservation : + (g : TypeCtx) -> (t, t' : Term) -> (T : Ty) -> + WellTyped g t T -> Step t t' -> WellTyped g t' T + +-------------------------------------------------------------------------------- +-- E2. Linear-binding consumption coverage +-- +-- Source: src/formal/Ephapax/Formal/Qualifier.idr `splitLinearCoverage` +-- (DISCHARGED, MERGED 2026-05-19 via ephapax#85). +-- +-- Statement: in any context split (e.g. across a `let` boundary or a +-- pair-elimination), every linear binding in the original context +-- appears in exactly one side of the split. The discharged version +-- proves this for arbitrary positions in the context (not just the +-- head, the form `nonDiminishment` had). The general form across +-- *control-flow* paths (effect handlers, region exit, exceptions) +-- remains OWED. +-------------------------------------------------------------------------------- + +||| E2 (PARTIAL — head/position form DISCHARGED, control-flow form OWED). +||| The position-form discharge lives in +||| `src/formal/Ephapax/Formal/Qualifier.idr` as `splitLinearCoverage` +||| (a real proof, no escape hatches). At the seam we only state the +||| OWED control-flow generalisation: a linear binding consumed in one +||| branch of a conditional / one arm of pattern-match / one exit of +||| a region must also be consumed in every other branch. +public export +0 linearConsumptionAcrossControlFlow : + (g : TypeCtx) -> (t : Term) -> (T : Ty) -> + WellTyped g t T -> Type + +-------------------------------------------------------------------------------- +-- E3. No region escape (narrow form discharged) +-- +-- Source: src/formal/Ephapax/Formal/RegionLinear.idr `noEscapeTheorem` +-- (DISCHARGED, real proof — case analysis on NoRegionInType). +-- +-- The discharged form proves the narrow case +-- `NoRegionInType r (Scoped r a) -> Void` +-- (a value scoped to r cannot itself claim "no region r appears in my +-- type"). The general statement — values scoped to r never appear +-- outside r's lexical extent at runtime — is OWED at the operational- +-- semantics level (it needs E1 type-preservation as a lemma). +-------------------------------------------------------------------------------- + +||| Abstract "term references region r" predicate. Mirrors the Rust +||| typing pass's region-membership check. +public export +0 ReferencesRegion : RegionId -> Term -> Type + +||| E3 (OWED — operational form). If a region-block exits with result +||| value `v` and the region `r` is no longer in scope, then `v` does +||| not reference `r` at runtime. The static form +||| (`noEscapeTheorem` on types) is discharged in +||| `Ephapax.Formal.RegionLinear.noEscapeTheorem`; the operational +||| form rests on E1 type-preservation across `ERegion` reduction. +public export +0 regionNoRuntimeEscape : + (r : RegionId) -> (body, result : Term) -> + Step (ERegion r body) result -> + ReferencesRegion r result -> Void + +-------------------------------------------------------------------------------- +-- E4. Vacuous wrappers in formal/ — flagged, NOT a seam invariant +-- +-- Source: src/formal/Ephapax/Formal/RegionLinear.idr +-- `regionSafetyExtract`, `noGCExtract`. +-- +-- ROADMAP.adoc / PROOF-NEEDS.md cite these as "regionSafetyTheorem" / +-- "noGCTheorem" being complete. Their bodies are tautological wrappers: +-- regionSafetyExtract r ctx t ne lc = ne +-- noGCExtract r ctx t ne lc = (ne, lc) +-- — they return their inputs unchanged. The proofs are sound (no +-- escape hatches) but the *content* is vacuous: they don't establish +-- region safety, they just extract a witness that was already given. +-- +-- The honest seam invariants are E3 (real no-escape, OWED at the +-- operational level) and a NEW E4 (below) for the GC-freedom property +-- that `noGCExtract` only names. Both are OWED; the wrappers should be +-- separately replaced or honestly demoted (tracked, NOT in this seam). +-------------------------------------------------------------------------------- + +||| E4 (OWED). Operational GC-freedom: no run-time garbage collector is +||| needed because every heap-allocated value's lifetime is statically +||| bounded by an enclosing region. The current Idris2 `noGCExtract` +||| tautologically returns its inputs and does not establish this. +public export +0 noRuntimeGC : + (g : TypeCtx) -> (t : Term) -> (T : Ty) -> + WellTyped g t T -> Type + +-------------------------------------------------------------------------------- +-- E5. WASM compilation correctness +-- +-- Source: src/ephapax-wasm/ (compile_term : Term → WasmExpr). +-- +-- Invariant: the Rust WASM backend's lowering preserves typing and +-- semantics. No Idris2 or Coq counterpart for `compile_term` exists in +-- the repo today (the formalisation stops at the source language); the +-- entire claim is OWED. +-------------------------------------------------------------------------------- + +||| Abstract WASM typing judgement (would mirror the WebAssembly spec's +||| validation rules). +public export +0 WasmTyped : WasmExpr -> Ty -> Type + +||| Abstract compilation function. The Rust `compile_term` lives in +||| src/ephapax-wasm/; the seam states the obligation, not the algorithm. +public export +0 compile : Term -> WasmExpr + +||| E5 (OWED). If a source term is well-typed at `T`, its WASM +||| compilation is also well-typed at `T`. No formalisation of +||| `compile` exists in this repo today (neither Idris2 nor Coq); +||| this is the highest-leverage compiler-correctness gap. +public export +0 wasmCompilationPreservesTyping : + (g : TypeCtx) -> (t : Term) -> (T : Ty) -> + WellTyped g t T -> WasmTyped (compile t) T + +-------------------------------------------------------------------------------- +-- E6. IR lowering correctness +-- +-- Source: src/ephapax-ir/ (lower : Term → SExpr). +-- +-- The IR lowering is qualifier-erasing (the S-expression form drops +-- linear/affine annotations because the discipline check has already +-- run). Invariant: lowering preserves *operational* semantics — every +-- reduction in the source corresponds to a reduction in the IR. +-- OWED; the IR has no formalisation today. +-------------------------------------------------------------------------------- + +||| Abstract IR-level reduction. +public export +0 SStep : SExpr -> SExpr -> Type + +||| Abstract IR lowering function. +public export +0 lowerIR : Term -> SExpr + +||| E6 (OWED). Source reduction implies IR reduction: every step in the +||| source operational semantics corresponds to one (or more) steps in +||| the IR. No formalisation today. +public export +0 irLoweringPreservesSemantics : + (t, t' : Term) -> Step t t' -> + (s' : SExpr ** SStep (lowerIR t) s') diff --git a/src/abi/Ephapax/ABI/Types.idr b/src/abi/Ephapax/ABI/Types.idr new file mode 100644 index 00000000..b0fe128d --- /dev/null +++ b/src/abi/Ephapax/ABI/Types.idr @@ -0,0 +1,158 @@ +||| SPDX-License-Identifier: PMPL-1.0-or-later +||| Ephapax ABI: Boundary Types +||| +||| Idris2 statements of the data types that the Ephapax Rust pipeline +||| moves across its trust boundaries (typing, IR, WASM compilation, +||| Zig FFI token buffer). These mirror Rust types in: +||| - src/ephapax-syntax/ (Term, Type, Qualifier) +||| - src/ephapax-typing/ (Discipline, TypeEnv) +||| - src/ephapax-ir/ (SExpr) +||| - src/ephapax-wasm/ (WasmExpr, FuncIdx) +||| +||| This module is the ABI/FFI seam mandated by +||| standards/rhodium-standard-repositories/spec/LANGUAGE-POLICY.adoc +||| §Terminology: the Rust here is "Rust/SPARK" and must be DESIGNED to +||| admit SPARK/Ada modules across an Idris2-typed boundary. Nothing in +||| the Rust crates is itself the ABI; this file is. +||| +||| Verification scope: this file is a faithful, total Idris2 model of +||| the boundary data. The existing formalisation in `src/formal/` deals +||| with region/linear-type metatheory, but did not previously expose a +||| named ABI seam — this module fills that gap. + +module Ephapax.ABI.Types + +import Data.List +import Data.String +import Decidable.Equality + +%default total + +-------------------------------------------------------------------------------- +-- Qualifier (mirror of Rust enum Qual, src/ephapax-syntax/ qualifier) +-------------------------------------------------------------------------------- + +||| Resource qualifier on a binding. Mirrors the dyadic-type-system +||| `Qual` enum: `Linear` = exactly-once, `Affine` = at-most-once, +||| `Unrestricted` = unrestricted use. Constructor order is ABI- +||| significant. +public export +data Qual : Type where + Linear : Qual + Affine : Qual + Unrestricted : Qual + +public export +DecEq Qual where + decEq Linear Linear = Yes Refl + decEq Affine Affine = Yes Refl + decEq Unrestricted Unrestricted = Yes Refl + decEq Linear Affine = No (\case Refl impossible) + decEq Linear Unrestricted = No (\case Refl impossible) + decEq Affine Linear = No (\case Refl impossible) + decEq Affine Unrestricted = No (\case Refl impossible) + decEq Unrestricted Linear = No (\case Refl impossible) + decEq Unrestricted Affine = No (\case Refl impossible) + +-------------------------------------------------------------------------------- +-- Region identifier (mirror of src/formal/Ephapax/Formal/Region.idr RegionId) +-------------------------------------------------------------------------------- + +||| A region identifier — named, depth-tagged scope. Re-stated at the +||| seam (rather than imported from Ephapax.Formal.Region) so the ABI is +||| self-contained: a SPARK/Ada side need not depend on the metatheory +||| package to read the seam. +public export +record RegionId where + constructor MkRegionId + name : String + depth : Nat + +-------------------------------------------------------------------------------- +-- Types (mirror of Rust enum Type, src/ephapax-syntax/types) +-------------------------------------------------------------------------------- + +||| Ephapax types. Constructor order is ABI-significant. `TArrow` carries +||| the qualifier of the function value itself (the binder's qualifier +||| lives on the binder). `TScoped` is the region-bound type — the +||| metatheory's `Scoped r a` (`src/formal/Ephapax/Formal/Region.idr`). +public export +data Ty : Type where + TUnit : Ty + TBool : Ty + TInt : Ty + TString : Ty + TArrow : (q : Qual) -> (dom : Ty) -> (cod : Ty) -> Ty + TPair : (l : Ty) -> (r : Ty) -> Ty + TScoped : (region : RegionId) -> (inner : Ty) -> Ty + +-------------------------------------------------------------------------------- +-- Terms (mirror of Rust enum Term, src/ephapax-syntax/) +-------------------------------------------------------------------------------- + +||| Ephapax surface terms. Constructor order is ABI-significant. The +||| interpreter (src/ephapax-interp/), the typing pass (src/ephapax-typing/) +||| and the IR lowering (src/ephapax-ir/) all walk this shape. +public export +data Term : Type where + EVar : (name : String) -> Term + ELit : (value : String) -> Term + ELam : (q : Qual) -> (param : String) -> (paramTy : Ty) -> (body : Term) -> Term + EApp : (fn : Term) -> (arg : Term) -> Term + ELet : (q : Qual) -> (name : String) -> (rhs : Term) -> (body : Term) -> Term + EPair : (l : Term) -> (r : Term) -> Term + ERegion : (region : RegionId) -> (body : Term) -> Term + +-------------------------------------------------------------------------------- +-- Typing context (mirror of Rust struct TypeEnv, src/ephapax-typing/) +-------------------------------------------------------------------------------- + +||| A typing context entry: name × qualifier × type. The Rust +||| `TypeEnv` is a `Vec<(String, Qual, Type)>` walked left-to-right by +||| the discipline checker. +public export +record CtxEntry where + constructor MkCtxEntry + name : String + qual : Qual + ty : Ty + +public export +TypeCtx : Type +TypeCtx = List CtxEntry + +-------------------------------------------------------------------------------- +-- IR S-expressions (mirror of Rust enum SExpr, src/ephapax-ir/) +-------------------------------------------------------------------------------- + +||| The Ephapax IR is an S-expression intermediate form between the +||| surface AST and the WASM backend. The shape is intentionally simpler +||| than `Term` (no qualifier annotations — those are erased after +||| type-checking, and the IR is the "discipline-erased" form). +public export +data SExpr : Type where + SAtom : (token : String) -> SExpr + SList : (children : List SExpr) -> SExpr + +-------------------------------------------------------------------------------- +-- WASM expressions (mirror of Rust src/ephapax-wasm/ minimal surface) +-------------------------------------------------------------------------------- + +||| WebAssembly function index — bounded `u32`. The range obligation is +||| discharged at the Foreign boundary (see Foreign.idr `InU32`). +public export +FuncIdx : Type +FuncIdx = Nat + +||| Minimal WASM expression surface. The real Rust backend emits a much +||| richer set (control flow, memory ops, table refs); the ABI only +||| names the constructs whose typing/semantics must be preserved by +||| the lowering, so the compiler-correctness invariant E6 has somewhere +||| to live without committing to a particular emit form. +public export +data WasmExpr : Type where + WI32Const : (value : Nat) -> WasmExpr + WLocalGet : (idx : Nat) -> WasmExpr + WLocalSet : (idx : Nat) -> (rhs : WasmExpr) -> WasmExpr + WCall : (fn : FuncIdx) -> (args : List WasmExpr) -> WasmExpr + WBlock : (body : List WasmExpr) -> WasmExpr diff --git a/src/abi/ephapax-abi.ipkg b/src/abi/ephapax-abi.ipkg new file mode 100644 index 00000000..42bb04c7 --- /dev/null +++ b/src/abi/ephapax-abi.ipkg @@ -0,0 +1,22 @@ +-- SPDX-License-Identifier: PMPL-1.0-or-later +-- Build/typecheck package for the Ephapax Rust↔SPARK ABI seam. +-- +-- The seam modules are namespaced `Ephapax.ABI.*`; Idris2 requires the +-- on-disk path to mirror the module path, so the sources live under +-- `src/abi/Ephapax/ABI/`. This package makes the seam machine-checked; +-- CI (`.github/workflows/abi-verify.yml`) runs `idris2 --build` on +-- every change to `src/abi/**` so the stated obligations cannot +-- silently rot into `believe_me` or get out of sync with the Rust +-- pipeline. + +package ephapax-abi +version = 0.1.0 +authors = "Jonathan D.A. Jewell (hyperpolymath)" +license = "PMPL-1.0-or-later" +sourcedir = "." + +modules = Ephapax.ABI.Types + , Ephapax.ABI.Invariants + , Ephapax.ABI.Foreign + +depends = base