diff --git a/.machine_readable/root-allow.txt b/.machine_readable/root-allow.txt index 196dbcf..dac3f5b 100644 --- a/.machine_readable/root-allow.txt +++ b/.machine_readable/root-allow.txt @@ -33,6 +33,7 @@ LICENSES/ # REUSE licence texts, dual-licence model (code MPL-2 CHANGELOG.adoc # AsciiDoc is the estate-standard documentation format CITATION.cff # citation metadata; GitHub reads it from the root of the default branch only rsr-template-repo_chora.deed # the repo deed: universal AI entry point; family-7 allocation manifest + ply tree folded in (standards#837 pilot). Filename carries the repo slug (deed dispatch _chora.deed), so repo-init renames it at mint +ULTRAPLAN.md # project plan of record (occupancy-types): thesis, rung contract, ladder, kill criteria, decision log CLAUDE.md # generated arrival pack; the generator, pre-commit and Claude Code all read it from the ROOT (do not hand-edit; edit the a2ml source) ?GEMINI.md # pointer to CLAUDE.md for repos without AGENTS.md yet Justfile # thin; delegates phases to build/just/*.just diff --git a/Justfile b/Justfile index 78b18ce..e57cd09 100644 --- a/Justfile +++ b/Justfile @@ -137,18 +137,19 @@ clean-all: clean # Run all tests test *args: #!/usr/bin/env bash - # A check that cannot fail is not a check. This recipe MUST be replaced at - # mint with the project's real test command; until then it fails loudly - # rather than printing "Tests passed!" over an empty run. - # - # Replace this whole body with one of: - # cargo test --workspace {{args}} - # mix test {{args}} - # zig build test {{args}} - # deno test {{args}} - echo "FAIL: \`just test\` has not been wired to a real test command yet." >&2 - echo " Edit the 'test' recipe in the Justfile before relying on this gate." >&2 - exit 1 + # Project test command (wired at mint per this recipe's instructions): + # the Session IR example suite — accepts, expected-rejection controls and + # expected bounds, with the stepper asserting steps <= certified grade. + PYTHONPATH=src python3 -m session_ir test examples/session_ir/manifest.json {{args}} + +# The ULTRAPLAN §5 gate: proofs + tests + expected-rejection controls + +# checker on fixtures. Missing toolchains fail loudly with fixture requests +# (scripts/check.sh). `just check-ir` is the runnable-only slice. +check: + @bash scripts/check.sh + +check-ir: + @bash scripts/check.sh --runnable-only # Run tests with verbose output test-verbose: diff --git a/README.adoc b/README.adoc index 23a053b..fb695b7 100644 --- a/README.adoc +++ b/README.adoc @@ -24,12 +24,54 @@ image:https://api.thegreenwebfoundation.org/greencheckimage/{{FORGE}}[Green Web, {{PROJECT_DESCRIPTION}} +== This repository: occupancy-types + +Stepwise resource-bounding types: deterministic memory first, network +resources second. This checkout hosts the *Session IR calculus, checker and +Idris spike* (ULTRAPLAN R0-B) and the *stackcert* certificate checker (R1) +on top of the RSR scaffold. + +* Plan of record (thesis, rung contract, kill criteria, decision log): + link:ULTRAPLAN.md[`ULTRAPLAN.md`] +* Operational model (what the grade means): link:docs/OPERATIONAL-MODEL.md[`docs/OPERATIONAL-MODEL.md`] +* Claims-to-files map (with verification status): link:docs/EXPLAINME.adoc[`docs/EXPLAINME.adoc`] +* Vocabulary: link:docs/glossary.adoc[`docs/glossary.adoc`] · + Retractions & blocked runs: link:docs/retraction-ledger.adoc[`docs/retraction-ledger.adoc`] +* The gate: `just check` (= proofs + tests + expected-rejection controls + + checker on fixtures; `just check-ir` runs the toolchain-free slice) + +== Type-family map (estate coherence) + +This repo is one node of the hyperpolymath type-theory family. The shared +map — vocabulary, connection obligations, ownership routing — lives in +https://github.com/hyperpolymath/nextgen-typing[`nextgen-typing`]: +link:https://github.com/hyperpolymath/nextgen-typing/blob/main/docs/TYPE-CONNECTIONS.adoc[TYPE-CONNECTIONS.adoc]. + +* *Question this repo asks* — how do live-state footprints compose, and when + are they reclaimed? (Occupancy/HWM grades; protocol frontier = reclamation.) +* *Boundary* — an occupancy bound is not a cost bound (HWM monoid ≠ max-plus); + a measured live-byte count is not an occupancy grade. Cost grades live in + link:https://github.com/hyperpolymath/tropical-types[tropical-types] + (the ULTRAPLAN name `tropical-resource-typing` resolves there). +* *Not this repo* — echo indices, warrants, residue measures (shared glossary + in TYPE-CONNECTIONS separates all of these from resource grades). + +Quick start (Python 3, stdlib only): + +[source,bash] +---- +PYTHONPATH=src python3 -m session_ir test examples/session_ir/manifest.json +PYTHONPATH=src python3 -m session_ir check examples/session_ir/accept_seq_add.sir +---- + [IMPORTANT] ==== -*This file is a template.* You are reading `README.adoc` from the *RSR template repo* -(or a freshly-cloned copy of it). Run `just repo-init` to replace every `{{PLACEHOLDER}}` -token with your project's details, then delete this admonition. Until you do, the -`{{...}}` markers below are intentional placeholders, not content. +*This file still contains RSR template material.* You are reading `README.adoc` +from the *RSR template repo* scaffold (or a freshly-cloned copy of it). Run +`just repo-init` to replace every `{{PLACEHOLDER}}` token with your project's +details, then delete this admonition. Until you do, the `{{...}}` markers below +are intentional placeholders, not content. Project-specific truth lives in +`ULTRAPLAN.md` and `docs/` (see the section above). ==== == What this is diff --git a/ULTRAPLAN.md b/ULTRAPLAN.md new file mode 100644 index 0000000..a8095f4 --- /dev/null +++ b/ULTRAPLAN.md @@ -0,0 +1,211 @@ + +# ULTRAPLAN — occupancy-types +Stepwise resource-bounding types: deterministic memory first, network resources second. +Version 0.2 · Status: pre-registration · Doc licence CC-BY-4.0 · Code licence MPL-2.0 + +## 0. Thesis + +Types can give checked, composable, worst-case evidence for resources that are currently +estimated by unverified tools plus a safety margin. The instrument is not a new allocator: +it is (a) eliminating dynamic allocation with types proving the bounds, or (b) certifying +trivial allocators (fixed pools, LIFO regions, bounded queues). + +Two facts shape everything: + +1. **Cost vs state.** Cost resources (time, rounds, stack depth) compose with + in sequence + and max across alternatives — tropical. State resources (pool occupancy, buffers, FDs, + credits) are acquired and released; their composition is the high-water-mark (HWM) monoid + (p₁,n₁)·(p₂,n₂) = (max(p₁, n₁+p₂), n₁+n₂), unit (0,0), which is non-commutative. + Both axes are needed; neither is the other. + +2. **Buffer = memory.** Channel windows and arrival/service curves yield buffer grades; + buffer grades are occupancy. This is what makes network and memory one tool rather than two. + +3. **Protocol frontier = reclamation point.** When an endpoint reaches End and is closed, + every buffer whose owner was that session epoch is dead. Live memory is a function of + protocol shape, not of GC. + +## 1. Scope, value, stopping rules + +### 1.1 Where the value is real +Safety-critical / hard-real-time (DO-178C, ISO 26262, IEC 61508; MISRA, JSF, SPARK, ARINC 653) +and sandboxes (wasm pages/fuel, eBPF verifiers). There, constant grades cost nothing extra. + +### 1.2 Non-goals (permanent) +Not an allocator. Not average-case or probabilistic. Not data-dependent grades. Not a surface +language before a certificate checker has a user. Not dependent on K-CUT, Echo, epistemic, or +secret types. No cross-kernel imports. + +### 1.3 Contribution claim (falsifiable) +- Distinct phenomenon: state resources need a sequential, non-commutative grade axis beside + tropical cost grades; certificates are preferable to analyses. +- Characteristic theorems: T1 effect/coeffect coherence; T2 buffer grade commutes with + endpoint projection; T3 one program, two bounds; T4 worst-case-by-construction vs amortised. +- Canonical examples: stack, pool, queue, binary session. +- Project-level stop: if at the R2 gate there is no external consumer for certificates and no + theorem beyond restatement, archive with a ledger entry. + +### 1.4 Grade constancy rule +A grade is a literal or a static parameter fixed at check time. Parametric polymorphism over +grades is allowed if every instantiation is static. Needing anything else is a kill signal. + +## 2. Decisions + +| ID | Decision | Default | +|----|----------|---------| +| D1 | Where code lives | Algebra: tropical-resource-typing. Calculus, checker, spike: this repo | +| D2 | Kernels | Lean 4 for metatheory + verified checker; Idris 2 for QTT spike; Python/Rust for session IR checker | +| D3 | First real target | Session IR (fastest to fail), then Zephyr samples/synchronization on qemu_cortex_m3 | +| D4 | Session IR grade | Communication steps, max-plus (ℕ∪{∞}, max, +, 0) | +| D5 | Drop vs implicit free | Explicit drop for Buf, close for endpoints, both consuming | +| D6 | Recursion in session IR | Omitted in v0; finite unrolled protocols sufficient | +| D7 | Numeric carrier | ℕ/ℤ everywhere; no reals, no Mathlib | + +## 3. Rung contract + +A rung is complete only when all four hold: +1. **Theorem** — composition law + soundness, mechanised, axiom footprint printed +2. **Artefact** — a runnable library or checker, tiny +3. **Ground truth** — measured ≤ certified on every run; tightness ratio reported +4. **Consumer** — one external tool whose output it checks or one external artefact it sizes + +Plus a pre-written kill criterion, a time box, and a ledger entry on failure. + +## 4. The ladder + +### R0-A — HWM Algebra (tropical-resource-typing, Lean 4, 1 week) + +SequentialEffect typeclass + HWM instance + laws + non-commutativity witnesses + +bridge lemma + iteration lemmas. See sibling repo for full task list. + +### R0-B — Session IR + Idris Spike (this repo, 1 week) + +**Phase 0: Operational Model (half day)** +- docs/OPERATIONAL-MODEL.md: machine config (heap, channels, threads, clock), grade meaning + (comm steps, max-plus), memory meaning (linear Buf, explicit drop/close), deterministic + (no GC, no implicit copy), non-readings (not echo, not warrant, not residue) +- Kill test: explain ⊕ = max, ⊗ = + in four sentences without "tropical" + +**Phase 1: Smallest Helpful Checker (2-3 days)** + +IR grammar: +``` +Types: Unit | Buf n | A ⊗ B | S +Sessions: End | !A.S | ?A.S | ⊕{ℓᵢ:Sᵢ} | &{ℓᵢ:Sᵢ} +Terms: unit | drop e | alloc n | pair e₁ e₂ | letpair | + new S | send ep val | recv ep | close ep | + select ℓ ep | case ep {ℓᵢ: x.eᵢ} | let x:A@r = e₁ in e₂ +Judgment: Γ ⊢ e : A | r (r = comm step count, max-plus) +``` + +Grade rules: send/recv/select = 1 + subterms; case = 1 + max branches; let = r₁ + r₂; +alloc/unit/drop/close/pair/letpair = 0 + subterms; new = 0. + +Memory invariant: each Buf and endpoint appears exactly once in linear context or is consumed. + +Examples (≥8): 3+ accept, 3+ reject (double-send, drop-then-send, protocol mismatch, +close-before-End), 2+ with expected bounds (choice max, sequential add). + +Checker: Python or Rust. Parse, type-check syntax-directed, print A|r or specific error. +Stepper: reduce closed programs, count comm steps, assert steps ≤ r. + +Kill test: if errors are inscrutable, or grade can be smaller than a real run, or you needed +Echo/K-CUT to explain it, Phase 1 fails. + +**Idris 2 Spike (2-3 days)** +- Occ indexed state monad with static occupancy/peak indices, linear handles +- Bounded queue example with static peak +- Four expected-rejection controls +- Kill question answer: are constant grades tolerable and tight? + +Kill: bounded-queue example non-trivial only with data-dependent grades → stop, ledger. + +### R1 — stackcert (≤3 weeks) +Stack-depth certificate checker. Lean 4 verified core + parsers. GCC .ci/.su input. +Zephyr fixture with painted-stack ground truth. cert_sound theorem. +See task list T1-T9 in the kickoff prompt. + +Kill: no true positive, no justified budget reduction, no consumer at time box. + +### R2 — Static pools + affine/linear handles (6 weeks) +Calculus with pools, HWMI grades, QTT coeffects. T1 coherence theorem. +Kill: coherence needs useless side conditions, or every example violates grade constancy. +**Project gate after R2.** + +### Phase 2 (within R2) — Protocol cut = reclaim +Session frontier as arena epoch. When endpoint reaches End and is closed, every buffer whose +owner was that session epoch is dead. Live memory = function of protocol shape. +Kill: live-memory bound is merely "max message × window" written in a comment with no +compositional advantage. + +### R3 — Binary session channels with buffer grades (6 weeks) +Buffer occupancy grading composed by HWM. k-bounded async queues. +Kill: realistic protocols need unbounded windows or data-dependent payloads. + +### R4 — Network-calculus curves as grades +Token bucket, rate-latency closed forms over ℕ/ℤ. +Kill: closed forms don't compose with R3 grades without reals. + +### R5 — Multiparty projection +Project global type, grade locally. Does buffer grade commute with projection? +Kill: projection fails to preserve grades on a basic pattern. + +### Phase 5 (any time after R1) — Sit under someone else's tool +Pick one host. Provide a 2-page contract. Kill: host can't take the idea without estate glossary. + +### R6+ — Epistemic credits, echo diagnostics (post hoc only, maybe never) +Not memory management. Annotate traces, don't change drop/send. +Resource grade ≠ echo index ≠ residue measure. + +## 5. Cross-cutting requirements +- Proof purity: Lean — no Mathlib, no sorry, no Classical.choice; Idris — %default total; + Agda (R5+) — --safe --without-K +- Port-and-reprove; cross-reference by module.theorem +- Docs from day one: README.adoc, EXPLAINME.adoc, retraction-ledger.adoc, glossary.adoc +- just check = proofs + tests + expected-rejection controls + checker on fixtures +- Vocabulary discipline: cost grade ≠ occupancy grade ≠ echo index ≠ residue measure ≠ warrant + +## 6. Ground-truth protocol +1. Record toolchain versions, flags, board/QEMU, workload duration, commit SHAs +2. Soundness: measured ≤ certified on every run. Violation = stop + ledger entry +3. Tightness: certified/measured per unit; report distribution +4. Reproducible from just measure; fixtures committed with README + +## 7. Prior art and positioning +| Area | Works | We borrow | Ours | +|------|-------|-----------|------| +| Bounded-space types | Hofmann LFPL; RAML | framing | worst-case-by-construction, constant grades, no LP | +| Regions / ownership | Tofte-Talpin, Rust, WIT | affine handles | T1 coherence with occupancy index | +| Graded types | Granule, Atkey QTT, McBride, Katsumata, Gordon | coeffect + effect structure | HWM as first-class instance; cost/state separation with witnesses | +| Indexed monads | McBride, Atkey | spike encoding | absolute/relative bridge lemma | +| Stack bounding | Regehr et al., AbsInt, cargo-call-stack | the rule | certificate format + verified checker + ground-truth protocol | +| Session types | Honda-Yoshida, Wadler CP, Gay-Vasconcelos | linear binary sessions | comm-step grade + protocol-frontier reclamation | +| Costed sessions | Das-Hoffmann-Pfenning, Bocchi-Yang-Yoshida | latency grading | buffer occupancy grading composed by HWM | +| Network calculus | Cruz, Le Boudec-Thiran, ONERA Coq | closed forms | composition with pool/channel grades | + +## 8. Session report format +Proved (theorem, file, #print axioms) · Tested (positive / expected-rejection) · Measured +(table + command) · Open / blocked · Kill dashboard (per rung) · Retractions · Next task ids + +## 9. Decision log (fill as you go) +| Decision | Choice | Why | Revisit when | +|----------|--------|-----|--------------| +| Session IR grade | comm steps, max-plus | one operational reading | R2/Phase 4 | +| Drop vs implicit free | explicit drop + close | deterministic, checkable leaks | never if examples work | +| Recursion | omitted in v0 | demo first | after 8 examples | +| Multiparty | no | projection is a swamp | R5 | +| Second algebra | no | soup kills errors | R2/Phase 4 | +| Estate imports | none | kernel must stand | Phase 5 contract | +| Session IR checker language | Python 3 stdlib | D2 permits Python or Rust; only Python in the work environment; estate deny-list tension noted | Rust toolchain available | +| `case` binder reading | binder = continuation endpoint, scrutinee consumed | only reading that gives `x` a job; branches merge on linear part | R3 delegation | +| Unrestricted names at merge | Unit names branch-local, may differ | only linear state is a resource | if unrestricted types grow | +| Occ spike storage | `Fin n -> Nat` FIFO (ring layout deferred) | occupancy indices are layout-independent | if a consumer needs ring layout | +| stackcert callee model | lists-as-sets (no Mathlib) | D7 purity | port-and-reprove if Finset needed | +| stackcert dynamic frames | `[dynamic]` byte bound in annotations.toml | "reject without annotation" needs an annotation channel | R1 contract review | +| Proofs registration | spike/stackcert NOT in proofs MANIFEST until toolchains run | `gated` = "must compile"; unverified code must not claim it | T-P2-1 / T-P3-1 | +| docs/OPERATIONAL-MODEL.md stays .md | ULTRAPLAN names the path exactly | gate allowlisted instead (check-no-md-in-docs.sh) | if the plan renames it | +| Family registration | register in nextgen-typing TYPE-CONNECTIONS map (question + boundary + connections) | coherence without code coupling; the map's vocabulary fence IS §5 of this plan | map review | +| Naming errata | "tropical-resource-typing" (D1/R0-A) is the historical name; GitHub canonical is `tropical-types` (redirect); `katagoria`→`ideas-to-alphas` ≠ `kategoria` | name hygiene per nextgen-typing naming note 2026-09-09 | never | diff --git a/docs/EXPLAINME.adoc b/docs/EXPLAINME.adoc index c8ca0f6..ecad9dc 100644 --- a/docs/EXPLAINME.adoc +++ b/docs/EXPLAINME.adoc @@ -8,6 +8,88 @@ image:https://img.shields.io/badge/License-MPL_2.0-blue.svg[License: MPL-2.0,lin This file explains how the key template claims map to real files. += occupancy-types — claims to files + +Project claims (ULTRAPLAN R0-B + R1). Receipts taxonomy: *TESTED* (command +run in the work environment, output recorded in the session report), +*UNVERIFIED* (code + exact commands, toolchain absent — fixture request in +`docs/retraction-ledger.adoc`), *CONJECTURE* (argued, not yet checked). + +== C1. The grade r in Γ ⊢ e : A \| r is a worst-case communication-step bound + +Status: *TESTED*. + +* Checker: `src/session_ir/checker.py` (six rule shapes over + `src/session_ir/syntax.py:MaxPlus`). +* Stepper: `src/session_ir/machine.py` counts steps on the real reduction; + asserts `steps ≤ r`. +* Evidence: `examples/session_ir/manifest.json` — 14/14 green; + `accept_choice_max.sir` certifies 5 and measures 4 (strict); + `accept_choice_expensive.sir` certifies 6 and measures 6 (tight). +* Command: `PYTHONPATH=src python3 -m session_ir test examples/session_ir/manifest.json` + +== C2. Linear uniqueness rejects real memory/protocol bugs + +Status: *TESTED*. + +* Seven expected-rejection controls, each pinning an error class: + double-send, drop-then-send (use-after-drop), protocol mismatch, + close-before-End, double-free, leak, aliasing + (`examples/session_ir/reject_*.sir`, codes asserted in the manifest). +* Command: same as C1 (reject rows). + +== C3. The Phase 0 kill test passes as written + +Status: *TESTED* (mechanically). + +* `docs/OPERATIONAL-MODEL.md` §2.1: four sentences explaining ⊕ = max, + ⊗ = +, banned word absent. +* Command: `bash scripts/check.sh` stage 2 audits the block (sentence count + + banned-word grep). + +== C4. Occ: static occupancy/peak indices + linear handles program a bounded buffer + +Status: *UNVERIFIED* (no `idris2` in the work environment). + +* Code: `src/occ/Occ.idr` (Occ monad, `WithAlloc` linear binder, capacity + `LTE (S n) C`, bounded FIFO `Queue k n`), `src/occ/Demo.idr` + (`producerConsumer : Occ 0 2 2 (Queue 2 2)` — static peak = K = 2). +* Expected-rejection controls: `src/occ/Reject{id,Leak,OverCapacity,UseAfterFree}.idr`. +* Kill question answered provisionally in `src/occ/README.adoc` + (CONJECTURE: constant grades tolerable and tight on this example). +* Commands: `cd src/occ && idris2 --check Occ.idr && idris2 --check Demo.idr`; + `bash src/occ/check-rejections.sh`. + +== C5. stackcert `check` is sound: accepted certificates bound every call path + +Status: *UNVERIFIED* (no `lean` in the work environment). + +* Theorem: `StackcertCore.cert_sound` in `src/stackcert/StackcertCore.lean` + (zero imports; no holes; no Classical.choice). +* `#print axioms` footprint: *not yet available*. After the first successful + `lean StackcertCore.lean` run, the exact output of + `#print axioms StackcertCore.cert_sound` will be pasted here verbatim. + Expected form: `'StackcertCore.cert_sound' depends on axioms: [...]` + with an empty list — this expectation is CONJECTURE until pasted. +* Commands: `bash tests/run_stackcert.sh` (core + fixture + four negative + controls: decremented bound, undeclared recursion, unresolved indirect, + undeclared cycle). + +== C6. Fixtures are real compiler output + +Status: *TESTED* (provenance), fixture measurements *BLOCKED*. + +* `src/stackcert/fixtures/probe.{c,su,ci}` and `cycle.{c,su,ci}` were + generated with `gcc -O0 -fcallgraph-info=su -fstack-usage -c .c` + (host gcc) and committed; regenerate to re-verify provenance. +* Zephyr ground truth (painted-stack HWM on qemu_cortex_m3) is a fixture + request: exact commands in `src/stackcert/README.adoc`; nothing measured + until it runs. + += RSR template claims + +The sections below describe the scaffold this project is built on. + == Central Session Protocol Authority Claim: diff --git a/docs/OPERATIONAL-MODEL.md b/docs/OPERATIONAL-MODEL.md new file mode 100644 index 0000000..4282d32 --- /dev/null +++ b/docs/OPERATIONAL-MODEL.md @@ -0,0 +1,164 @@ + +# OPERATIONAL-MODEL — occupancy-types Session IR (v0) + +Status: ULTRAPLAN R0-B, Phase 0. Paired with Phase 1 artefacts in +`src/session_ir/`, examples in `examples/session_ir/`. Plan of record: +`ULTRAPLAN.md` at the repo root. + +This document fixes what the grade *means*, what memory *means*, and what the +model deliberately does **not** read. If a claim about the checker cannot be +reduced to this document plus the code, it is not a claim of this project. + +## 1. Machine configuration + +A closed program runs on a deterministic machine with four components: + +| Component | Contents | Discipline | +|-----------|----------|------------| +| Heap | linear buffers `Buf n` (n bytes) | explicit `drop` only; no GC, no implicit copy | +| Channels | pairs of endpoints created by `new S`, each side with a FIFO queue of events (`msg v`, `sel l`) | events drain in order; `close` requires the endpoint at `End` | +| Threads | one thread of control (a single term; `let` sequences everything) | binary sessions only — two endpoints of `new`, used by one program | +| Clock | communication steps: `send`, `recv`, `select`, `case` each count 1 | the only cost axis in v0 | + +The machine is deterministic: closed programs reduce along exactly one path. +A stepper (`src/session_ir/machine.py`) reduces a checked program, counts +communication steps, and records operational statistics (peak live bytes, +peak in-flight channel events). Machine-level faults (`R_*` codes) are +self-checks: they fire loudly if the checker and the machine ever disagree, +and are unreachable for accepted programs except the deliberate deadlock +detector (`R_DEADLOCK` when a `recv`/`case` runs with nothing in flight — +possible in principle for ill-ordered single-threaded code, never in the +shipped examples). + +## 2. Grade meaning — communication steps in max-plus + +The judgment is `Γ ⊢ e : A | r` where `r` is the **communication-step count**: +an upper bound on the number of `send`/`recv`/`select`/`case` actions any run +of `e` can perform. The grade carrier is ℕ (v0 has no recursion, so no ∞ is +needed; `∞` remains the designated value for unbounded protocols if recursion +is ever admitted — currently a rejection, per ULTRAPLAN D6). + +Grades form the max-plus semiring (ℕ, max, +, 0), exposed as a small +importable object (`session_ir.syntax.MaxPlus`): `op_add = max` (choice), +`op_mul = +` (sequence), `zero = one = 0`. The six typing-rule shapes are +expressed only in terms of it: + +| Term former | Grade rule | +|-------------|------------| +| `unit`, `alloc n`, `new S` | 0 | +| `drop e`, `close ep` | 0 + r(sub) | +| `pair e1 e2`, `letpair …`, `let … = e1 in e2` | r₁ + r₂ (sequence) | +| `send ep v`, `recv ep`, `select l ep` | 1 + r(subterms) | +| `case ep {li: xi. ei}` | 1 + maxᵢ r(eᵢ) (alternatives) | + +Soundness obligation (checked on every accepted example by the stepper): +**measured steps ≤ certified r**. A violation is a stop-and-ledger event +(ULTRAPLAN §6.2). The reported `certified/measured` ratio is the tightness +reading; it is 1.00 when the expensive path is taken and > 1 when the program +takes a cheaper branch than the worst case — worst-case-by-construction. + +### 2.1 Kill test: why choice is max and sequence is + + +The Phase 0 kill test: explain ⊕ = max, ⊗ = + in four sentences without the +word "tropical". This block is machine-audited by `scripts/check.sh` +(exactly four sentences; the banned word absent): + + +When a program may take any one of several branches, the number we can honestly promise is the number from the most expensive branch, because we cannot rule that branch out. +When one action must finish before the next begins, both costs definitely happen and they accumulate, so sequencing combines grades with addition. +Doing nothing costs 0, the identity for both combinators on the grade carrier ℕ, while ∞ would mark the unbounded and is absorbing for addition. +Because every term former maps to only these two combinators, a checker computes the worst-case grade compositionally from the syntax alone, without running the program or solving equations. + + +## 3. Memory meaning — linear uniqueness, not GC + +* `Buf n` has exactly one owner at every program point. Ownership moves + (delegation via `send`), it is never duplicated. Aliasing (`pair ep ep`, + double `let`-binding of one handle) is a type error (`E_ALIAS`). +* **Explicit drop for Buf, explicit close for endpoints; both consume** + (ULTRAPLAN D5). Dropping twice is `E_DOUBLE_FREE`; using a dropped buffer or + a closed endpoint is `E_USE_AFTER_DROP`; closing before `End` is + `E_CLOSE_NOT_END`; ending the program with any linear name alive is + `E_LEAK`. +* The invariant (ULTRAPLAN Phase 1): **each `Buf` and endpoint appears exactly + once in the linear context or is consumed.** Unrestricted `Unit` names may be + ignored or shadowed; linear names may not. +* Live memory is *counted*, not graded, in v0: the stepper reports peak live + bytes (high-water mark of allocated-minus-dropped buffers) and peak in-flight + channel events as operational readings. The occupancy/HWM grade algebra is + R2–R3, and is deliberately **not** a second semiring here (mission + constraint). + +### 3.1 Endpoint threading and `case` + +`send`/`recv`/`select` thread the endpoint name: the residual context carries +it forward at its continuation type. `case` is a destructor: it consumes its +endpoint name and binds the per-branch continuation `xi : Si` inside branch +`i`. Branches must agree on the result type (`E_CASE_TYPE`) and on the live +*linear* state after the merge (`E_CASE_LINEAR`); unrestricted names are +branch-local and do not escape. This is the one place the IR deviates from a +naive reading of the ULTRAPLAN grammar — the grammar's `case ep {ℓᵢ: x.eᵢ}` +binder is given its only useful reading (the continuation endpoint). +Revisitable; recorded in the decision log. + +### 3.2 Single-threaded correlated choice + +With one thread of control, the `select` determines which `case` branch runs; +the remaining branches are dead code but must still typecheck against the +post-select context. The grade still takes the max over all branches +(worst-case-by-construction). `examples/session_ir/accept_choice_max.sir` +(certificate 5, measured 4) and `accept_choice_expensive.sir` (6 = 6) pin both +sides of this. + +## 4. Determinism and what the model does not read + +* No GC, no implicit copy, no sharing of buffers or endpoints. +* The only annotation forms are types and constant grade bounds `@r` + (ULTRAPLAN §1.4 grade constancy: literals/statics only). A bound annotation + is *checked* (`computed ≤ claimed`, else `E_BOUND`), never trusted. + +Non-readings — this model is **not**: + +* **not echo** — no diagnostic indices, no trace annotation (R6+, maybe never); +* **not warrant** — no epistemic or evidence types; certificates are plain + bounds with an operational reading; +* **not residue** — no residual-evidence measure; `resource grade ≠ echo index + ≠ residue measure` (ULTRAPLAN §5). + +No imports from echo-types, epistemic-types, residual-evidence-types, +secret-types, tropical-resource-typing, or choreographic-types. Everything +used here is defined here. + +## 5. Running the artefact + +```sh +PYTHONPATH=src python3 -m session_ir check FILE # prints A|r or error +PYTHONPATH=src python3 -m session_ir run FILE --trace # steps, HWM, trace +PYTHONPATH=src python3 -m session_ir test examples/session_ir/manifest.json +``` + +Reproducible check for the whole rung: `scripts/check.sh` (also exposed as +`just check`). Python 3.11 stdlib only. + +## 6. Phase 1 kill-test verdict (pre-registered criteria) + +Pre-registered kill test (ULTRAPLAN Phase 1): *if errors are inscrutable, or +grade can be smaller than a real run, or you needed Echo/K-CUT to explain it, +Phase 1 fails.* + +| Criterion | Verdict | Receipt | +|-----------|---------|---------| +| Errors inscrutable | not fired | every reject example reports a specific coded error with position (`E_PROTOCOL`, `E_USE_AFTER_DROP`, `E_DOUBLE_FREE`, `E_CLOSE_NOT_END`, `E_LEAK`, `E_ALIAS`); see `examples/session_ir/manifest.json`, all 7 matched | +| Grade smaller than a real run | not fired | stepper asserts `steps ≤ r` on every accepted example; 7/7 holds (2=2, 4=4, 4≤5, 6=6, 2=2, 0=0, 2=2) | +| Needed Echo/K-CUT to explain | not fired | this document explains the whole instrument without either | + +Mission-level kill test (three-way): the rejects are real bug classes +(double-free, use-after-drop/close, protocol mismatch, close-before-End, +aliasing, leak) — not counting trivia; the stepper demonstrates `steps ≤ grade` +on every accept and strict inequality on `accept_choice_max.sir`. The eight +examples are therefore not "linear sessions plus counting sends" alone: they +pin a certified bound with a demonstrated operational reading and a memory +invariant. **Not fired.** diff --git a/docs/glossary.adoc b/docs/glossary.adoc new file mode 100644 index 0000000..5a89371 --- /dev/null +++ b/docs/glossary.adoc @@ -0,0 +1,107 @@ +// SPDX-License-Identifier: CC-BY-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) += occupancy-types Glossary +:toc: +:icons: font + +Vocabulary discipline (ULTRAPLAN §5): *cost grade ≠ occupancy grade ≠ echo +index ≠ residue measure ≠ warrant*. Each term below has exactly one meaning in +this project; cross-family borrowing of these words is a bug. + +The estate-wide shared glossary (Echo/Epistemic/Tropical/Residual/Choreographic +families) lives in +https://github.com/hyperpolymath/nextgen-typing/blob/main/docs/TYPE-CONNECTIONS.adoc[nextgen-typing +`docs/TYPE-CONNECTIONS.adoc`]. The two vocabularies must not drift: where a +term exists in both, that document is authoritative for cross-family reading +and this file is authoritative inside occupancy-types. Cost grade, occupancy +grade, echo index, residue measure and warrant are pairwise distinct in both. + +== Terms + +*Cost grade*:: + A bound on consumed work that composes with `+` in sequence and `max` across + alternatives (max-plus). In v0 the only cost grade is the *communication + step* count. Never used for memory. + +*Occupancy grade*:: + A bound on live state that composes by the high-water-mark (HWM) monoid + `(p₁,n₁)·(p₂,n₂) = (max(p₁, n₁+p₂), n₁+n₂)`, unit `(0,0)`, non-commutative. + Not instantiated in v0 (R2–R3). "Live memory counted in examples" is a + measurement, not an occupancy grade. + +*Communication step*:: + One `send`, `recv`, `select`, or `case` action. The unit of the v0 cost + grade. `close`, `drop`, `alloc`, `new`, `unit` cost 0 steps. + +*Max-plus semiring*:: + `(ℕ ∪ {∞}, max, +, 0)` — the grade algebra of cost. Exposed as the + importable `MaxPlus` interface (`src/session_ir/syntax.py`). + +*HWM monoid*:: + The sequential composition law of state resources (see *occupancy grade*). + Non-commutative: acquire-then-release composes differently from + release-then-acquire. Distinct from the max-plus semiring; neither reduces + to the other. + +*Linear uniqueness*:: + The memory discipline of the Session IR: every `Buf` and endpoint name has + exactly one owner per program point; ownership moves (delegation), never + duplicates. Violations are type errors (`E_ALIAS`, `E_DOUBLE_FREE`, + `E_USE_AFTER_DROP`, `E_LEAK`). + +*Explicit drop / close*:: + The only deallocation actions (ULTRAPLAN D5). `drop` frees a `Buf`; + `close` consumes an endpoint at `End`. Both are consuming. No GC, no + implicit free. + +*Session frontier (protocol frontier)*:: + The point where an endpoint reaches `End` and is closed. ULTRAPLAN §0.3 + designates it the reclamation point of the session epoch: buffers owned by + a dead session are dead. Not implemented in v0; R2 Phase 2. + +*Certificate*:: + A checked bound with an operational reading, produced compositionally at + check time (e.g. `Unit | 5`), verifiable without re-running the program. + Distinct from an analysis estimate and from a proof of optimality. + +*Tightness ratio*:: + `certified / measured` per unit, reported per run (ULTRAPLAN §6.3). `1.00` + is tight; `> 1` is slack (worst-case-by-construction). + +*Expected-rejection control*:: + A committed program (or proof) that must *fail* to check, with the error + class pinned. Guards against checker softening. (Session IR: + `examples/session_ir/reject_*.sir`; Idris spike: four controls.) + +*Kill criterion / kill test*:: + A pre-written falsifier for a rung. If fired: stop the rung, write a + `retraction-ledger.adoc` entry, do not silently redefine success. + +*Echo index*:: + R6+ concept only (post hoc, maybe never): a trace annotation. Not a + resource bound. Never appears in v0 code or certificates. + +*Residue measure*:: + Not used in this project. Named here only to keep the boundary sharp + (residual-evidence-types is a separate kernel; no imports). + +*Warrant*:: + Not used in this project. No epistemic reading of certificates; a + certificate is a number plus an operational argument, nothing more. + +== Where each term is realised + +[cols="1,2"] +|=== +| Term | Realisation + +| Cost grade | `MaxPlus`, `Γ ⊢ e : A \| r` in `src/session_ir/checker.py` +| Occupancy grade | R2–R3 (not in v0) +| Communication step | machine clock in `src/session_ir/machine.py` +| Linear uniqueness | checker context rules; `E_ALIAS`/`E_LEAK` family +| Explicit drop/close | `drop`/`close` rules; `E_DOUBLE_FREE`, `E_CLOSE_NOT_END` +| Certificate | `check` output `A\|r`; `@r` annotations (checked) +| Tightness ratio | `run` output `certified/measured` +| Expected-rejection control | `examples/session_ir/manifest.json` reject rows +| Kill criterion | `ULTRAPLAN.md` + kill tables in `docs/reports/` +|=== diff --git a/docs/reports/session-2026-09-27.adoc b/docs/reports/session-2026-09-27.adoc new file mode 100644 index 0000000..9ce5bbe --- /dev/null +++ b/docs/reports/session-2026-09-27.adoc @@ -0,0 +1,117 @@ +// SPDX-License-Identifier: CC-BY-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) += Session Report — 2026-09-27 — occupancy-types +:toc: +:icons: font + +Format: ULTRAPLAN §8. Branch `arena/01a0e2de-occupancy-types`. Work +environment: Python 3.11.2, gcc (host), make, git; *no* `just`, `idris2`, +`lean`/`lake`, `west`/QEMU/Zephyr. Toolchain downloads blocked by network +policy (github.com source + pypi reachable; elan/objects/releases hosts +blocked). Nothing in this report is measured data unless a command and its +output are shown. + +== Proved + +*Nothing is claimed as proved this session.* The one theorem shipped, +`StackcertCore.cert_sound` (`src/stackcert/StackcertCore.lean`), is written +to be proved (zero imports, no holes, no Classical.choice) but the work +environment could not run `lean`. Its `#print axioms` slot in +`docs/EXPLAINME.adoc` C5 is explicitly unfilled. Status: UNVERIFIED + +fixture request (ledger §Blocked). + +== Tested (commands run in this environment) + +Positive / expected-rejection — command: +`PYTHONPATH=src python3 -m session_ir test examples/session_ir/manifest.json` +→ *14/14 examples OK* (7 accept with exact judgments A\|r, 7 reject with +exact error codes; every accept also runs the stepper and asserts +`steps ≤ grade`, `steps`, and `peak_live` against the manifest). + +[cols="1,1,1,1,1"] +|=== +| example | certified r | measured steps | peak_live (bytes) | tightness r/steps + +| accept_send_recv | 2 | 2 | 0 | 1.00 +| accept_seq_add | 4 | 4 | 0 | 1.00 +| accept_choice_max | 5 | 4 | 0 | 1.25 (cheap branch taken) +| accept_choice_expensive | 6 | 6 | 0 | 1.00 +| accept_buf_delegation | 2 | 2 | 4 | 1.00 +| accept_pair_drop | 0 | 0 | 6 | n/a +| accept_annotated | 2 | 2 | 0 | 1.00 +|=== + +Rejects: `E_PROTOCOL`×2 (double-send, mismatch), `E_USE_AFTER_DROP`, +`E_CLOSE_NOT_END`, `E_DOUBLE_FREE`, `E_LEAK`, `E_ALIAS` — all with the +pre-registered codes. + +Phase 0 kill-test audit (4 sentences, banned word absent) and repo shape +gates: green (`bash scripts/check.sh --runnable-only`, full output run +2026-09-27). + +Fixtures provenance: `src/stackcert/fixtures/*.su` and `*.ci` generated live +with `gcc -O0 -fcallgraph-info=su -fstack-usage -c probe.c|cycle.c` (host +gcc); certificate arithmetic in `cert.toml` re-derives the rule by hand and +will be checked independently by the exe when `lake` runs. + +== Measured + +No real-target measurements this session (no QEMU/Zephyr). The session-IR +table above is machine output of the committed stepper, not hardware data. +No Zephyr painted-stack numbers exist; none are claimed. + +== Open / blocked + +* BLOCKED — `idris2` absent: Occ spike (Piece 2) written, unverified. + Commands + fixture request: `src/occ/README.adoc`; ledger entry present. +* BLOCKED — `lean`/`lake` absent (downloads blocked): stackcert (Piece 3) + written, unverified. Commands: `tests/run_stackcert.sh`. +* BLOCKED — Zephyr fixture request (samples/synchronization @ qemu_cortex_m3, + painted-stack HWM via `k_thread_stack_space_get`): exact command block in + `src/stackcert/README.adoc`. R1 time box has not started. +* OPEN — `verification/proofs/idris2/MANIFEST` registration for + `src/occ/Occ.idr` + `Demo.idr` (as `gated`) once `idris2` confirms they + compile. Deliberately not registered before that (a `gated` entry is a + "must compile" claim). +* OPEN — estate language-policy tension (Python deny-list vs ULTRAPLAN D2 + "Python or Rust"): checker is Python 3 stdlib. Decision logged in + ULTRAPLAN §9; revisit if a Rust port is wanted. + +== Kill dashboard + +[cols="1,1,3"] +|=== +| Rung / piece | Kill status | Evidence + +| R0-B Phase 0 | not fired | kill test passed AND machine-audited (stage 2 of `scripts/check.sh`) +| R0-B Phase 1 | not fired | rejects are real bug classes; stepper shows steps ≤ grade on every accept (strict inequality demonstrated); errors are coded + positioned +| R0-B Piece 2 (Occ) | open (pre-registered: not fired by the code as written) | kill question answered CONJECTURE-positive in `src/occ/README.adoc`; falsifier pre-registered there; verdict awaits `idris2` +| R1 (stackcert) | open | time box not started (fixture blocked) +|=== + +Kill criteria that would fire next: (a) Occ example needs data-dependent +grades to typecheck ⇒ ledger + stop; (b) `cert_sound` fails to compile +without adding side conditions the model can't justify ⇒ rethink rule; +(c) measured > certified on any Zephyr run ⇒ stop + ledger (ULTRAPLAN §6.2). + +== Retractions + +None. See `docs/retraction-ledger.adoc` (also holds the blocked/fixture table). + +== Next task ids + +1. **T-P2-1** — provision `idris2`; run `src/occ` accept + rejection + commands; paste outputs into the session report; register `Occ.idr` / + `Demo.idr` as `gated` in `verification/proofs/idris2/MANIFEST`. +2. **T-P3-1** — provision `lean`/`lake` (elan, toolchain `leanprover/lean4: + v4.15.0`); run `tests/run_stackcert.sh`; paste `#print axioms + StackcertCore.cert_sound` into `docs/EXPLAINME.adoc` C5. +3. **T-P3-2** — Zephyr fixture request (owner-side): build + `samples/synchronization` for `qemu_cortex_m3` with + `-fcallgraph-info=su -fstack-usage`; run under QEMU with painted stacks; + record toolchain versions + SHAs; compare measured HWM ≤ certified. +4. **T-P1-1** — optional: a second pair of eyes on `checker.py` case-merge + rule (E_CASE_LINEAR on linear part only) before any R2 work builds on it. +5. **T-DOC-1** — `just repo-init`-style placeholder cleanup of the root + `README.adoc` remains the template's mint procedure; project content lives + in `ULTRAPLAN.md` + `docs/` meanwhile. diff --git a/docs/retraction-ledger.adoc b/docs/retraction-ledger.adoc new file mode 100644 index 0000000..99ad764 --- /dev/null +++ b/docs/retraction-ledger.adoc @@ -0,0 +1,65 @@ +// SPDX-License-Identifier: CC-BY-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) += occupancy-types Retraction Ledger +:toc: +:icons: font + +Policy (ULTRAPLAN §3, §1.3): every rung ships a pre-written kill criterion. +When a kill criterion fires — or a claimed result turns out to be wrong — the +claim is *retracted here*, not quietly re-scoped. A retraction names the claim, +the evidence that killed it, and the rung affected. Kill-criterion firing stops +that rung; it does not start a redefinition. + +This ledger also records *blocked* rungs (environment missing, fixture +requested). Blocked ≠ retracted: no claim has been withdrawn. + +== Retractions + +[cols="1,2,2,1"] +|=== +| Date | Claim retracted | Evidence | Rung + +| _(none yet)_ | | | +|=== + +== Blocked / fixture requests + +[cols="1,2,2,1"] +|=== +| Date | What is blocked | Exact command(s) to unblock | Rung + +| 2026-09-27 +| Idris 2 spike unverified (no `idris2` on PATH in the work environment) +| `idris2 --check Occ.idr` from `src/occ/`; `./check-rejections.sh` for the + four expected-rejection controls (see `src/occ/README.adoc`) +| R0-B Piece 2 + +| 2026-09-27 +| stackcert core unverified (no `lean`/`lake` on PATH) +| `lake build && lake exe stackcert …` from `src/stackcert/`; + `lean StackcertCore.lean` then `#print axioms cert_sound` (see + `src/stackcert/README.adoc`) +| R1 Piece 3 + +| 2026-09-27 +| Zephyr ground-truth fixture absent (no `west`/QEMU/Zephyr SDK; fixture + request issued — see `src/stackcert/README.adoc` §Fixture request) +| `west build -b qemu_cortex_m3 zephyr/samples/synchronization` … + (full command block committed there; nothing measured until it runs) +| R1 Piece 3 +|=== + +== Kill dashboard summary + +Full tables live in the session report (`docs/reports/`); per-rung state: + +[cols="1,1,3"] +|=== +| Rung | Kill status | Note + +| R0-B Phase 0/1 (Session IR) | not fired | kill-test audited mechanically + (`scripts/check.sh`); 14/14 examples green; steps ≤ grade on every run +| R0-B Piece 2 (Idris spike) | open | kill question answered provisionally in + `src/occ/README.adoc`; verdict marked UNVERIFIED until `idris2` runs +| R1 (stackcert) | open | time box not started; fixture request pending +|=== diff --git a/examples/session_ir/accept_annotated.sir b/examples/session_ir/accept_annotated.sir new file mode 100644 index 0000000..96be55a --- /dev/null +++ b/examples/session_ir/accept_annotated.sir @@ -0,0 +1,14 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* accept_annotated.sir — optional @r annotations claim grade bounds on let + bindings. The checker accepts when computed <= claimed (a certificate is + an upper bound); slack is allowed. + + send computed 1 <= claimed 2 (slack) ; recv computed 1 = claimed 1 (exact) + close computed 0 = claimed 0. + Certified r = 2 (computed; annotations are checked, not trusted). *) +letpair ep1 ep2 = new (!Unit.End) in +let _ : Unit @ 2 = send ep1 unit in +let m : Unit @ 1 = recv ep2 in +let _ @ 0 = close ep1 in +let _ @ 0 = close ep2 in +unit diff --git a/examples/session_ir/accept_buf_delegation.sir b/examples/session_ir/accept_buf_delegation.sir new file mode 100644 index 0000000..fc568cd --- /dev/null +++ b/examples/session_ir/accept_buf_delegation.sir @@ -0,0 +1,15 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* accept_buf_delegation.sir — a linear Buf 4 is sent across the session + (delegation), received under a new owner, then explicitly dropped. + + Certified r = send 1 + recv 1 = 2. + Machine: steps = 2, peak_live = 4 bytes (the buffer is live across the + send; ownership moves to the receiver; drop is the only free). *) +letpair ep1 ep2 = new (!(Buf 4).End) in +let x = alloc 4 in +let _ = send ep1 x in +let b = recv ep2 in +let _ = drop b in +let _ = close ep1 in +let _ = close ep2 in +unit diff --git a/examples/session_ir/accept_choice_expensive.sir b/examples/session_ir/accept_choice_expensive.sir new file mode 100644 index 0000000..c9ceb10 --- /dev/null +++ b/examples/session_ir/accept_choice_expensive.sir @@ -0,0 +1,27 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* accept_choice_expensive.sir — same protocol as accept_choice_max.sir but the + program takes the EXPENSIVE branch, so the bound is tight. + + select b ep1 -> 1 + case ep2 -> 1 + max(branch a = 3, branch b = 4) = 5 + certified r = 6 + Machine (takes b): steps = 1 + 1 + 2 sends + 2 recvs = 6 <= 6 (tight). *) +letpair ep1 ep2 = new (+{a: !Unit.End, b: !Unit.!Unit.End}) in +let _ = select b ep1 in +case ep2 { + a: k. + let _ = send ep1 unit in + let _ = send ep1 unit in + let m = recv k in + let _ = close k in + let _ = close ep1 in + unit, + b: k. + let _ = send ep1 unit in + let _ = send ep1 unit in + let m = recv k in + let m2 = recv k in + let _ = close k in + let _ = close ep1 in + unit +} diff --git a/examples/session_ir/accept_choice_max.sir b/examples/session_ir/accept_choice_max.sir new file mode 100644 index 0000000..9749660 --- /dev/null +++ b/examples/session_ir/accept_choice_max.sir @@ -0,0 +1,33 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* accept_choice_max.sir — alternatives take max (the "choice max" expected + bound), and worst-case-by-construction is visible: the program selects the + CHEAP branch, so measured < certified. + + ep1 offers +{a: !Unit.End, b: !Unit.!Unit.End}; ep2 offers the dual &. + select a ep1 -> 1 + case ep2 -> 1 + max(branch a = 2, branch b = 3) = 4 + certified r = 5 + Machine (takes a): steps = select 1 + case 1 + send 1 + recv 1 = 4 <= 5. + + NOTE: in this single-threaded IR the select fixes which case branch runs; + the other branches are dead code but must still typecheck against ep1's + post-select type. Branch b's second recv would await a message that never + comes — it is never executed, and the certified bound counts it anyway. + That is exactly the point: the bound is worst-case by construction. *) +letpair ep1 ep2 = new (+{a: !Unit.End, b: !Unit.!Unit.End}) in +let _ = select a ep1 in +case ep2 { + a: k. + let _ = send ep1 unit in + let m = recv k in + let _ = close k in + let _ = close ep1 in + unit, + b: k. + let _ = send ep1 unit in + let m = recv k in + let m2 = recv k in + let _ = close k in + let _ = close ep1 in + unit +} diff --git a/examples/session_ir/accept_pair_drop.sir b/examples/session_ir/accept_pair_drop.sir new file mode 100644 index 0000000..d740881 --- /dev/null +++ b/examples/session_ir/accept_pair_drop.sir @@ -0,0 +1,10 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* accept_pair_drop.sir — memory-only program: pair of buffers, letpair, + explicit drop of each. No communication at all. + + Certified r = 0 (alloc/pair/letpair/drop cost 0 communication steps). + Machine: steps = 0, peak_live = 2 + 4 = 6 bytes. *) +letpair b1 b2 = pair (alloc 2) (alloc 4) in +let _ = drop b1 in +let _ = drop b2 in +unit diff --git a/examples/session_ir/accept_send_recv.sir b/examples/session_ir/accept_send_recv.sir new file mode 100644 index 0000000..4b25724 --- /dev/null +++ b/examples/session_ir/accept_send_recv.sir @@ -0,0 +1,14 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* accept_send_recv.sir — the smallest full session: send one unit, recv it, + close both endpoints. + + Grade derivation (max-plus): + send = 1, recv = 1, close/close/unit/new = 0, lets add + certified r = 2 + Machine: steps = 2 <= 2, peak_live = 0. *) +letpair ep1 ep2 = new (!Unit.End) in +let _ = send ep1 unit in +let m = recv ep2 in +let _ = close ep1 in +let _ = close ep2 in +unit diff --git a/examples/session_ir/accept_seq_add.sir b/examples/session_ir/accept_seq_add.sir new file mode 100644 index 0000000..094a1fc --- /dev/null +++ b/examples/session_ir/accept_seq_add.sir @@ -0,0 +1,13 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* accept_seq_add.sir — sequential composition adds: two sends then two recvs. + + Certified r = 1 + 1 + 1 + 1 = 4 (the "sequential add" expected bound). + Machine: steps = 4 <= 4. *) +letpair ep1 ep2 = new (!Unit.!Unit.End) in +let _ = send ep1 unit in +let _ = send ep1 unit in +let m1 = recv ep2 in +let m2 = recv ep2 in +let _ = close ep1 in +let _ = close ep2 in +unit diff --git a/examples/session_ir/manifest.json b/examples/session_ir/manifest.json new file mode 100644 index 0000000..e83d89b --- /dev/null +++ b/examples/session_ir/manifest.json @@ -0,0 +1,19 @@ +{ + "comment": "occupancy-types Session IR example manifest (ULTRAPLAN Phase 1). accept entries pin the expected judgment A|r, measured comm steps and peak live bytes; reject entries pin the expected error code. Runner: python3 -m session_ir test examples/session_ir/manifest.json", + "examples": [ + {"file": "accept_send_recv.sir", "expect": "accept", "type": "Unit", "grade": 2, "steps": 2, "peak_live": 0}, + {"file": "accept_seq_add.sir", "expect": "accept", "type": "Unit", "grade": 4, "steps": 4, "peak_live": 0}, + {"file": "accept_choice_max.sir", "expect": "accept", "type": "Unit", "grade": 5, "steps": 4, "peak_live": 0}, + {"file": "accept_choice_expensive.sir","expect": "accept", "type": "Unit", "grade": 6, "steps": 6, "peak_live": 0}, + {"file": "accept_buf_delegation.sir", "expect": "accept", "type": "Unit", "grade": 2, "steps": 2, "peak_live": 4}, + {"file": "accept_pair_drop.sir", "expect": "accept", "type": "Unit", "grade": 0, "steps": 0, "peak_live": 6}, + {"file": "accept_annotated.sir", "expect": "accept", "type": "Unit", "grade": 2, "steps": 2, "peak_live": 0}, + {"file": "reject_double_send.sir", "expect": "reject", "error": "E_PROTOCOL"}, + {"file": "reject_drop_then_send.sir", "expect": "reject", "error": "E_USE_AFTER_DROP"}, + {"file": "reject_protocol_mismatch.sir","expect": "reject", "error": "E_PROTOCOL"}, + {"file": "reject_close_before_end.sir","expect": "reject", "error": "E_CLOSE_NOT_END"}, + {"file": "reject_double_free.sir", "expect": "reject", "error": "E_DOUBLE_FREE"}, + {"file": "reject_leak.sir", "expect": "reject", "error": "E_LEAK"}, + {"file": "reject_alias.sir", "expect": "reject", "error": "E_ALIAS"} + ] +} diff --git a/examples/session_ir/reject_alias.sir b/examples/session_ir/reject_alias.sir new file mode 100644 index 0000000..d0ded43 --- /dev/null +++ b/examples/session_ir/reject_alias.sir @@ -0,0 +1,8 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* reject_alias.sir — BUG: the same linear endpoint name used twice (aliasing). + + pair ep1 ep1 would duplicate ownership of one endpoint. + Expected: E_ALIAS. *) +letpair ep1 ep2 = new (!Unit.End) in +let p = pair ep1 ep1 in +unit diff --git a/examples/session_ir/reject_close_before_end.sir b/examples/session_ir/reject_close_before_end.sir new file mode 100644 index 0000000..8c76021 --- /dev/null +++ b/examples/session_ir/reject_close_before_end.sir @@ -0,0 +1,8 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* reject_close_before_end.sir — BUG: close an endpoint that is not at End. + + ep2 : !Unit.End (dual of ?Unit.End) — a send is still owed before close. + Expected: E_CLOSE_NOT_END. *) +letpair ep1 ep2 = new (?Unit.End) in +let _ = close ep2 in +unit diff --git a/examples/session_ir/reject_double_free.sir b/examples/session_ir/reject_double_free.sir new file mode 100644 index 0000000..fdb46f0 --- /dev/null +++ b/examples/session_ir/reject_double_free.sir @@ -0,0 +1,8 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* reject_double_free.sir — BUG: drop the same buffer twice. + + Expected: E_DOUBLE_FREE. *) +let x = alloc 4 in +let _ = drop x in +let _ = drop x in +unit diff --git a/examples/session_ir/reject_double_send.sir b/examples/session_ir/reject_double_send.sir new file mode 100644 index 0000000..808ac63 --- /dev/null +++ b/examples/session_ir/reject_double_send.sir @@ -0,0 +1,9 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* reject_double_send.sir — BUG: second send on an endpoint already at End. + + After the first send ep1 : End; the second send is a protocol violation. + Expected: E_PROTOCOL. *) +letpair ep1 ep2 = new (!Unit.End) in +let _ = send ep1 unit in +let _ = send ep1 unit in +unit diff --git a/examples/session_ir/reject_drop_then_send.sir b/examples/session_ir/reject_drop_then_send.sir new file mode 100644 index 0000000..a535c30 --- /dev/null +++ b/examples/session_ir/reject_drop_then_send.sir @@ -0,0 +1,10 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* reject_drop_then_send.sir — BUG: use-after-drop. + + x is dropped, then sent as the message. Linear ownership is gone. + Expected: E_USE_AFTER_DROP. *) +letpair ep1 ep2 = new (!(Buf 4).End) in +let x = alloc 4 in +let _ = drop x in +let _ = send ep1 x in +unit diff --git a/examples/session_ir/reject_leak.sir b/examples/session_ir/reject_leak.sir new file mode 100644 index 0000000..1eef68e --- /dev/null +++ b/examples/session_ir/reject_leak.sir @@ -0,0 +1,8 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* reject_leak.sir — BUG: endpoints never closed (linear leak). + + ep1 and ep2 stay in the context at end of program. + Expected: E_LEAK. *) +letpair ep1 ep2 = new (!Unit.End) in +let _ = send ep1 unit in +unit diff --git a/examples/session_ir/reject_protocol_mismatch.sir b/examples/session_ir/reject_protocol_mismatch.sir new file mode 100644 index 0000000..3b2990b --- /dev/null +++ b/examples/session_ir/reject_protocol_mismatch.sir @@ -0,0 +1,8 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* reject_protocol_mismatch.sir — BUG: send on an endpoint that offers ?A.S. + + ep1 : ?Unit.End — it receives, it does not send. + Expected: E_PROTOCOL. *) +letpair ep1 ep2 = new (?Unit.End) in +let _ = send ep1 unit in +unit diff --git a/scripts/check-no-md-in-docs.sh b/scripts/check-no-md-in-docs.sh index 1658f93..0cb435b 100644 --- a/scripts/check-no-md-in-docs.sh +++ b/scripts/check-no-md-in-docs.sh @@ -23,7 +23,10 @@ REPO_ROOT="${1:-.}" DOCS_DIR="$REPO_ROOT/docs" # Justified exceptions, relative to repo root. Empty by default. -ALLOWED=() +# docs/OPERATIONAL-MODEL.md — ULTRAPLAN §4 Phase 0 names this exact path as the +# rung deliverable ("docs/OPERATIONAL-MODEL.md: machine config ..."), so the +# filename is fixed by the plan of record. Kept as .md for that reason. +ALLOWED=("docs/OPERATIONAL-MODEL.md") # docs/berrywiki/ and docs/wikis/ are wiki-SYNC source trees: their content is # mirrored to/from forge-hosted wikis (GitHub/GitLab), which are inherently # Markdown. Converting them to AsciiDoc would break the sync contract, so the diff --git a/scripts/check.sh b/scripts/check.sh new file mode 100755 index 0000000..cf04c21 --- /dev/null +++ b/scripts/check.sh @@ -0,0 +1,108 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# check.sh — the occupancy-types gate: ULTRAPLAN §5 +# just check = proofs + tests + expected-rejection controls + checker on fixtures +# +# A missing toolchain is a FAIL with a fixture request, never a silent skip +# (estate doctrine: a gate that cannot run must not report OK). The +# --runnable-only flag runs just the stages this environment can execute and +# reports the rest as BLOCKED; its scope is printed and its exit code reflects +# only the stages it ran. +# +# Stages: +# 1 session-ir examples (accept/reject/expected bounds) + steps <= grade +# 2 Phase 0 kill-test audit (four sentences; banned word absent) +# 3 repo shape gates (root allowlist; no stray .md under docs/) +# 4 Idris Occ spike: accepts compile + 4 expected-rejection controls +# 5 stackcert: core axiom footprint + fixture + 4 negative controls + +set -uo pipefail +cd "$(dirname "${BASH_SOURCE[0]}")/.." +ROOT="$PWD" +MODE="${1:-all}" +fail=0 +blocked=0 + +note() { printf '%s\n' "$*"; } +ok() { printf 'PASS: %s\n' "$*"; } +bad() { printf 'FAIL: %s\n' "$*" >&2; fail=1; } + +note "=== 1. Session IR checker on fixtures ===" +if PYTHONPATH=src python3 -m session_ir test examples/session_ir/manifest.json; then + ok "session-ir examples (accept + reject + expected bounds; steps <= grade)" +else + bad "session-ir examples" +fi + +note "" +note "=== 2. Phase 0 kill-test audit ===" +if python3 - <<'PY' +import re, sys +src = open('docs/OPERATIONAL-MODEL.md', encoding='utf-8').read() +m = re.search(r'\n(.*?)', src, re.S) +if not m: + sys.exit('KILL-TEST block missing from docs/OPERATIONAL-MODEL.md') +block = m.group(1).strip() +if 'tropical' in block.lower(): + sys.exit('banned word present in kill-test block') +lines = [l for l in block.splitlines() if l.strip()] +if not (len(lines) == 4 and all(l.rstrip().endswith('.') for l in lines)): + sys.exit(f'kill-test must be exactly 4 sentences, found {len(lines)}') +print('kill-test: 4 sentences, banned word absent') +PY +then ok "kill-test audit"; else bad "kill-test audit"; fi + +note "" +note "=== 3. Repo shape gates ===" +if bash scripts/check-root-shape.sh . >/dev/null && bash scripts/check-no-md-in-docs.sh . >/dev/null; then + ok "root allowlist + docs .md policy" +else + bad "repo shape gates (run scripts/check-root-shape.sh / check-no-md-in-docs.sh)" +fi + +note "" +note "=== 4. Idris Occ spike (accepts + expected-rejection controls) ===" +if command -v idris2 >/dev/null 2>&1; then + if bash src/occ/check-rejections.sh; then + ok "Occ spike" + else + bad "Occ spike" + fi +else + if [ "$MODE" = "--runnable-only" ]; then + note "BLOCKED: idris2 not on PATH (fixture request in src/occ/README.adoc)" + blocked=1 + else + bad "idris2 not on PATH — Occ spike cannot be checked (fixture request: src/occ/README.adoc)" + fi +fi + +note "" +note "=== 5. stackcert (core + fixture + negative controls) ===" +if command -v lean >/dev/null 2>&1 && command -v lake >/dev/null 2>&1; then + if bash tests/run_stackcert.sh; then + ok "stackcert" + else + bad "stackcert" + fi +else + if [ "$MODE" = "--runnable-only" ]; then + note "BLOCKED: lean/lake not on PATH (fixture request in src/stackcert/README.adoc)" + blocked=1 + else + bad "lean/lake not on PATH — stackcert cannot be checked (fixture request: src/stackcert/README.adoc)" + fi +fi + +note "" +if [ "$fail" -ne 0 ]; then + note "check: FAIL" + exit 1 +fi +if [ "$blocked" -ne 0 ]; then + note "check (--runnable-only): OK for the stages that ran; PROOFS BLOCKED (see above)" + exit 0 +fi +note "check: OK — proofs + tests + expected-rejection controls + fixtures" diff --git a/src/occ/Demo.idr b/src/occ/Demo.idr new file mode 100644 index 0000000..6844035 --- /dev/null +++ b/src/occ/Demo.idr @@ -0,0 +1,51 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +-- Demo — canonical examples for the Occ spike (ULTRAPLAN R0-B, Piece 2). +-- UNVERIFIED without idris2 on PATH; see README.adoc. %default total. + +module Demo + +import Occ +import Data.Nat + +%default total + +||| Fixed pool of capacity 4: allocate two cells, free them in any order, +||| peak 2. The capacity proof (LTE (S n) C) is a static argument to every +||| alloc; over-capacity has no term (see RejectOverCapacity.idr). +export +poolDemo : Occ 0 0 2 Unit +poolDemo = + WithAlloc 4 (LTESucc LTEZero) (\h0 => + WithAlloc 4 (LTESucc (LTESucc LTEZero)) (\h1 => + seqU (Free h0) (seqU (Free h1) (LPure ())))) + +||| Bounded buffer of capacity K = 2, producer/consumer sequence: +||| push 10 0 -> 1 peak 1 +||| push 20 1 -> 2 peak 2 (buffer FULL: K = 2) +||| pop 2 -> 1 peak 2 (consumer takes 10) +||| push (popped) 1 -> 2 peak 2 (producer refills) +||| Static peak = 2 = K: TIGHT, and constant — no data-dependent grade is +||| needed anywhere in the file. This is the kill-question evidence. +export +producerConsumer : Occ 0 2 2 (Queue 2 2) +producerConsumer = + LBind (NewQ {k = 2}) (\q0 => + LBind (QPush (LTESucc LTEZero) 10 q0) (\q1 => + LBind (QPush (LTESucc (LTESucc LTEZero)) 20 q1) (\q2 => + LBind (QPop q2) (\pr => + case pr of + (q3, got) => + LBind (QPush (LTESucc (LTESucc LTEZero)) got q3) (\q4 => + LPure q4))))) + +||| The same producer/consumer with the empty-first-starve check: popping an +||| empty buffer is not merely wrong at runtime — `QPop : Queue k (S n) -> ...` +||| has no instance at n = 0, so the program does not typecheck. (Compile +||| this comment's shape on demand; the accepted path is producerConsumer.) +export +neverPopEmpty : Occ 0 1 1 (Queue 2 1) +neverPopEmpty = + LBind (NewQ {k = 2}) (\q0 => + LBind (QPush (LTESucc LTEZero) 7 q0) (\q1 => + LPure q1)) diff --git a/src/occ/Occ.idr b/src/occ/Occ.idr new file mode 100644 index 0000000..510614e --- /dev/null +++ b/src/occ/Occ.idr @@ -0,0 +1,107 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +-- Occ — occupancy-indexed state monad spike (ULTRAPLAN R0-B, Piece 2). +-- +-- Occ : (pre, post, peak : Nat) -> Type -> Type +-- +-- pre/post : live cells before/after the action +-- peak : high-water mark of live cells during the action (absolute) +-- +-- Composition (LBind): peaks compose by max (absolute occupancy indices); +-- occupancy in sequence chains via pre/post. Four expected-rejection +-- controls live in Reject*.idr beside this file: double free, dropped handle +-- (leak), alloc over capacity, use-after-free — all fail to typecheck. +-- +-- UNVERIFIED in this work environment (no idris2 on PATH): see README.adoc +-- for exact check commands. %default total is on; no holes. + +module Occ + +import Data.Nat +import Data.Fin + +%default total + +-- ── Handles ──────────────────────────────────────────────────────────────── + +||| A handle to one live cell of a fixed pool. Multiplicity 1: handles are +||| linear values (see WithAlloc's continuation binder and Free/Peek). +public export +data Handle : Type where + MkH : (cellId : Nat) -> Handle + +-- ── Bounded buffer ───────────────────────────────────────────────────────── + +||| Bounded buffer of capacity k holding n messages (static n <= k). +||| FIFO: index 0 is the oldest message. Storage is a Fin-indexed cell +||| function; the occupancy indices are layout-independent (ring-buffer +||| layout is orthogonal to occupancy indexing and is deferred). +public export +data Queue : (k, n : Nat) -> Type where + MkQ : (get : Fin n -> Nat) -> Queue k n + +-- ── The monad ────────────────────────────────────────────────────────────── + +||| Indexed state monad for occupancy. Static indices only: every grade here +||| is a literal or a static parameter (ULTRAPLAN §1.4). Data-dependent +||| grades are a kill signal, not a feature. +public export +data Occ : (pre, post, peak : Nat) -> Type -> Type where + ||| Return a value; no occupancy change. The value is linear. + LPure : (1 x : a) -> Occ n n n a + + ||| Sequential composition. Peaks compose by max (absolute indices). + ||| The continuation receives its argument at multiplicity 1: values that + ||| flow out of an action (notably handles) must be consumed exactly once. + LBind : (1 act : Occ p q m a) + -> (1 k : (1 _ : a) -> Occ q r m' b) + -> Occ p r (max m m') b + + ||| Allocate one cell of a pool of capacity C: allowed exactly when + ||| S n <= C (static proof; over-capacity has no such term). + Alloc : (C : Nat) -> (0 ok : LTE (S n) C) -> Occ n (S n) (S n) Handle + + ||| Free consumes its handle linearly (multiplicity 1). + Free : (1 h : Handle) -> Occ (S n) n (S n) Unit + + ||| Read a cell id, consuming the handle (use-after-free is a second use of + ||| one handle, which quantity checking rejects). + Peek : (1 h : Handle) -> Occ n n n Nat + + ||| Bounded-buffer actions. Occupancy counts in-flight messages. + NewQ : Occ n n n (Queue k 0) + QPush : (0 ok : LTE (S n) k) -> (msg : Nat) -> (1 q : Queue k n) + -> Occ n (S n) (S n) (Queue k (S n)) + QPop : (1 q : Queue k (S n)) -> Occ (S n) n (S n) (Queue k n, Nat) + +-- ── Derived combinators ──────────────────────────────────────────────────── + +||| Allocate and hand the handle to a linear continuation: the binder h has +||| multiplicity 1, so dropping it (0 uses), duplicating it, or freeing twice +||| (2 uses) are all type errors. +public export +WithAlloc : (C : Nat) -> (0 ok : LTE (S n) C) + -> (1 k : (1 h : Handle) -> Occ (S n) post peak b) + -> Occ n post (max (S n) peak) b +WithAlloc C ok k = LBind (Alloc C ok) k + +||| Sequence a Unit-producing action with a continuation, consuming the unit. +public export +seqU : (1 act : Occ p q m Unit) -> (1 next : Occ q r m' b) -> Occ p r (max m m') b +seqU act next = LBind act (\u => case u of MkUnit => next) + +-- ── Push/pop on the bounded buffer as pure total functions ───────────────── +-- (The Occ-level QPush/QPop above are the graded actions; these helpers show +-- the underlying FIFO discipline total-function style.) + +||| FIFO push: message goes to the back (new index S n is the newest slot). +public export +qpush : (0 ok : LTE (S n) k) -> (msg : Nat) -> (1 q : Queue k n) -> Queue k (S n) +qpush ok msg (MkQ get) = MkQ (\i => case i of + FZ => msg + FS j => get j) + +||| FIFO pop: oldest message (slot 0) leaves; the rest shift down. +public export +qpop : (1 q : Queue k (S n)) -> (Queue k n, Nat) +qpop (MkQ get) = (MkQ (\j => get (FS j)), get FZ) diff --git a/src/occ/README.adoc b/src/occ/README.adoc new file mode 100644 index 0000000..8b9f876 --- /dev/null +++ b/src/occ/README.adoc @@ -0,0 +1,115 @@ +// SPDX-License-Identifier: CC-BY-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) += Occ — occupancy-indexed state monad spike (ULTRAPLAN R0-B, Piece 2) +:toc: +:icons: font + +Status: *UNVERIFIED in the work environment that authored it* (no `idris2` on +PATH there). Receipts below are of two kinds only: (a) what is claimed and +where the code is, (b) the exact commands that would verify it. Nothing here +is reported as proven until those commands run green. + +== The spike + +`Occ.idr` defines the indexed state monad of the mission: + +---- +Occ : (pre, post, peak : Nat) -> Type -> Type +---- + +* `pre` / `post` — live cells before/after the action (occupancy). +* `peak` — high-water mark during the action, composed by `max` in `LBind` + (absolute indices; this is the cost-vs-state separation: the state axis is + an occupancy counter, not a tropical cost). +* `Alloc C ok` — capacity `C` is a static parameter; `ok : LTE (S n) C` is a + compile-time proof. Over-capacity has *no term*. +* `Free` / `Peek` consume their handle at multiplicity 1; `WithAlloc`'s + continuation binder is `(1 h : Handle) -> …`, so QTT enforces one owner. +* `Queue k n` — bounded buffer of capacity `k` with `n` messages in flight, + FIFO, stored as a `Fin n -> Nat` cell function. `QPush` needs `LTE (S n) k`; + `QPop` needs `S n` (empty buffers have no pop term). + +`Demo.idr` programs the canonical examples: + +* `poolDemo : Occ 0 0 2 Unit` — fixed pool, two cells, peak 2. +* `producerConsumer : Occ 0 2 2 (Queue 2 2)` — capacity-K=2 buffer: + push, push (full), pop, push. Static peak = 2 = K. + +== Kill question (ULTRAPLAN R0-B): are constant grades tolerable and tight? + +*Provisional answer: yes on this example — labelled CONJECTURE until the +commands below run.* + +Evidence in the code (each checkable by the elaborator once `idris2` exists): + +1. *Tolerable* — `producerConsumer` is written entirely with literal indices + (`Occ 0 2 2 (Queue 2 2)`). No grade anywhere in `Occ.idr`/`Demo.idr` is + computed from runtime data; the only compile-time obligations are `LTE` + proofs about two fixed numerals (1 ≤ 2, 2 ≤ 2). A producer/consumer loop + of *known* shape (this is D6: finite unrolled protocols) needs nothing + more. +2. *Tight* — the derived peak equals the true high-water mark: the buffer + really holds 2 messages at the marked point, and the type says `2`, not + `3` and not `∞`. `poolDemo`'s peak 2 is likewise exact. +3. *Static capacity is real* — `RejectOverCapacity.idr` cannot produce + `LTE 5 4`; a third push in `producerConsumer` would need `LTE 3 2` and + fails the same way. + +What would falsify this answer (pre-registered): if making `producerConsumer` +typecheck required a grade depending on message values, on queue contents, or +on any runtime quantity — i.e. if the indices had to track anything finer than +a numeral counter. The mission's kill criterion ("non-trivial only with +data-dependent grades ⇒ stop, ledger") is therefore *not fired by the code as +written*; the residual risk is that the code as written does not compile, +which the commands below decide. If it fails in a way that can only be fixed +by data-dependent grades, the kill criterion fires and the ledger entry is +written — no re-scoping. + +== Expected-rejection controls + +[cols="1,2,2"] +|=== +| File | Bug | Why it fails + +| `RejectDoubleFree.idr` | `free h` twice | multiplicity 1 on `Free` (and state indices clash) +| `RejectLeak.idr` | alloc, never free | binder `h` used 0 times (the indices alone would NOT catch this) +| `RejectOverCapacity.idr` | alloc at `n = C` | needs `LTE 5 4`; no such proof +| `RejectUseAfterFree.idr` | `Peek h` after `Free h` | second use of one linear name (indices alone would NOT catch this) +|=== + +Controls 2 and 4 are the interesting pair: they isolate the QTT multiplicity +discipline from the occupancy indices — each is accepted by one guard and +rejected by the other. + +== Verification commands (the receipts that do not yet exist) + +[source,bash] +---- +# 1. accept modules must compile (%default total, no holes): +cd src/occ && idris2 --check Occ.idr && idris2 --check Demo.idr + +# 2. all four controls must be rejected: +bash src/occ/check-rejections.sh +---- + +Record the toolchain (`idris2 --version`) with any result, per ULTRAPLAN §6.1. + +== Deviations from the mission wording (logged, not hidden) + +* *"Bounded ring buffer"* — the buffer is a `Fin n -> Nat` FIFO. Ring-buffer + *layout* (circular cursors) is orthogonal to occupancy indexing: push/pop + sequences and their high-water marks are identical. Layout deferred; the + decision log carries this. +* No interpreter `run : Occ p q m a -> State p -> (a, State q)` is provided. + The spike's question is about static indices and linear handles; an + interpreter plus the absolute/relative bridge lemma is R0-A/R2 content + (ULTRAPLAN attributes the bridge lemma to the algebra rung). + +== Where this sits + +* Plan: `ULTRAPLAN.md` §4 R0-B. · Operational model: `docs/OPERATIONAL-MODEL.md`. +* Not registered in `verification/proofs/idris2/MANIFEST` yet: `gated` there + means "must compile", and this environment cannot run `idris2`. Registering + unverified code as gated would be an unbacked claim. Next task once the + toolchain exists: run the commands, register `Occ.idr` + `Demo.idr` as + `gated`. diff --git a/src/occ/RejectDoubleFree.idr b/src/occ/RejectDoubleFree.idr new file mode 100644 index 0000000..7d4e62b --- /dev/null +++ b/src/occ/RejectDoubleFree.idr @@ -0,0 +1,21 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +-- EXPECTED-REJECTION CONTROL — double free. +-- +-- bad = WithAlloc 4 ok (\h => seqU (Free h) (Free h)) +-- +-- h is used twice: Free consumes its handle at multiplicity 1, so the second +-- Free is a quantity error (and independently the state indices cannot line +-- up: the second Free wants pre = 1 while the first left pre = 0). +-- This file MUST FAIL to typecheck. Checked by ../check-rejections.sh. + +module RejectDoubleFree + +import Occ +import Data.Nat + +%default total + +export +bad : Occ 0 0 2 Unit +bad = WithAlloc 4 (LTESucc LTEZero) (\h => seqU (Free h) (Free h)) diff --git a/src/occ/RejectLeak.idr b/src/occ/RejectLeak.idr new file mode 100644 index 0000000..43cf8bf --- /dev/null +++ b/src/occ/RejectLeak.idr @@ -0,0 +1,22 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +-- EXPECTED-REJECTION CONTROL — dropped handle (leak). +-- +-- bad = WithAlloc 4 ok (\h => LPure ()) +-- +-- The continuation binder h has multiplicity 1 but is used 0 times: the cell +-- is allocated and never freed. Quantity checking rejects the leak. +-- (Note the occupancy indices alone would NOT catch this: LPure unifies at +-- post = 1. This control is exactly what the multiplicity is for.) +-- This file MUST FAIL to typecheck. Checked by ../check-rejections.sh. + +module RejectLeak + +import Occ +import Data.Nat + +%default total + +export +bad : Occ 0 1 1 Unit +bad = WithAlloc 4 (LTESucc LTEZero) (\h => LPure ()) diff --git a/src/occ/RejectOverCapacity.idr b/src/occ/RejectOverCapacity.idr new file mode 100644 index 0000000..dc9fd29 --- /dev/null +++ b/src/occ/RejectOverCapacity.idr @@ -0,0 +1,22 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +-- EXPECTED-REJECTION CONTROL — alloc over capacity. +-- +-- bad = Alloc 4 (witness that pretends 5 <= 4) +-- +-- Alloc at occupancy n = 4 of a pool of capacity C = 4 needs a proof of +-- LTE (S 4) 4, i.e. 5 <= 4. No such proof exists; the bogus witness +-- (LTESucc x4 LTEZero : LTE 4 _) mismatches LTE 5 4 and the file is +-- rejected. Capacity is a static parameter, never a runtime check. +-- This file MUST FAIL to typecheck. Checked by ../check-rejections.sh. + +module RejectOverCapacity + +import Occ +import Data.Nat + +%default total + +export +bad : Occ 4 5 5 Handle +bad = Alloc 4 (LTESucc (LTESucc (LTESucc (LTESucc LTEZero)))) diff --git a/src/occ/RejectUseAfterFree.idr b/src/occ/RejectUseAfterFree.idr new file mode 100644 index 0000000..067278d --- /dev/null +++ b/src/occ/RejectUseAfterFree.idr @@ -0,0 +1,22 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +-- EXPECTED-REJECTION CONTROL — use-after-free. +-- +-- bad = WithAlloc 4 ok (\h => seqU (Free h) (Peek h)) +-- +-- Free consumes h at multiplicity 1; Peek then uses the same handle again — +-- a second use of a linear name. Quantity checking rejects it. (The state +-- indices would accept this shape — pre = post = 0 throughout — so this +-- control isolates the multiplicity discipline.) +-- This file MUST FAIL to typecheck. Checked by ../check-rejections.sh. + +module RejectUseAfterFree + +import Occ +import Data.Nat + +%default total + +export +bad : Occ 0 0 1 Nat +bad = WithAlloc 4 (LTESucc LTEZero) (\h => seqU (Free h) (Peek h)) diff --git a/src/occ/check-rejections.sh b/src/occ/check-rejections.sh new file mode 100755 index 0000000..08ac050 --- /dev/null +++ b/src/occ/check-rejections.sh @@ -0,0 +1,52 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# check-rejections.sh — expected-rejection controls for the Occ spike. +# +# Each Reject*.idr beside this script MUST FAIL `idris2 --check`. A control +# that starts typechecking is a red flag (the discipline softened) and fails +# this script. Exit codes: +# 0 every control rejected (and Demo.idr / Occ.idr compile — the accepts) +# 1 a control was accepted, or an accept module failed to compile +# 2 idris2 not on PATH (fixture request; NEVER a silent skip) + +set -euo pipefail +cd "$(dirname "${BASH_SOURCE[0]}")" + +if ! command -v idris2 >/dev/null 2>&1; then + cat >&2 <<'EOF' +FAIL (fixture request): idris2 not on PATH — the Occ spike is UNVERIFIED here. +Unblock with: + install Idris 2 (>= 0.7.0), e.g. via pack, or build from + https://github.com/idris-lang/Idris2/releases +then re-run: bash src/occ/check-rejections.sh +EOF + exit 2 +fi + +echo "=== Occ spike: accept modules (must compile) ===" +fail=0 +for mod in Occ.idr Demo.idr; do + printf ' %-24s ' "$mod" + out="$(idris2 --check "$mod" 2>&1)" && ! grep -q '^Error:' <<<"$out" || { + echo "FAIL (does not compile)"; echo "$out" | head -20; fail=1; continue; } + echo "PASS" +done + +echo "=== Occ spike: expected-rejection controls (must NOT compile) ===" +for mod in Reject*.idr; do + printf ' %-24s ' "$mod" + if out="$(idris2 --check "$mod" 2>&1)" && ! grep -q '^Error:' <<<"$out"; then + echo "FAIL (control was ACCEPTED — the discipline softened)" + fail=1 + else + echo "PASS (rejected)" + fi +done + +if [ "$fail" -ne 0 ]; then + echo "check-rejections: FAIL" >&2 + exit 1 +fi +echo "check-rejections: OK — accepts compile, all controls rejected" diff --git a/src/session_ir/__init__.py b/src/session_ir/__init__.py new file mode 100644 index 0000000..36287a9 --- /dev/null +++ b/src/session_ir/__init__.py @@ -0,0 +1,10 @@ +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +"""occupancy-types Session IR: checker + stepper (ULTRAPLAN R0-B, Phase 1).""" + +from .checker import check_program +from .machine import run_program +from .parser import parse +from .syntax import SIRError, MaxPlus, pp_ty + +__all__ = ["parse", "check_program", "run_program", "SIRError", "MaxPlus", "pp_ty"] diff --git a/src/session_ir/__main__.py b/src/session_ir/__main__.py new file mode 100644 index 0000000..2ab752e --- /dev/null +++ b/src/session_ir/__main__.py @@ -0,0 +1,7 @@ +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +import sys + +from .cli import main + +sys.exit(main()) diff --git a/src/session_ir/__pycache__/__init__.cpython-311.pyc b/src/session_ir/__pycache__/__init__.cpython-311.pyc new file mode 100644 index 0000000..d699973 Binary files /dev/null and b/src/session_ir/__pycache__/__init__.cpython-311.pyc differ diff --git a/src/session_ir/__pycache__/__main__.cpython-311.pyc b/src/session_ir/__pycache__/__main__.cpython-311.pyc new file mode 100644 index 0000000..af10570 Binary files /dev/null and b/src/session_ir/__pycache__/__main__.cpython-311.pyc differ diff --git a/src/session_ir/__pycache__/checker.cpython-311.pyc b/src/session_ir/__pycache__/checker.cpython-311.pyc new file mode 100644 index 0000000..324d31b Binary files /dev/null and b/src/session_ir/__pycache__/checker.cpython-311.pyc differ diff --git a/src/session_ir/__pycache__/cli.cpython-311.pyc b/src/session_ir/__pycache__/cli.cpython-311.pyc new file mode 100644 index 0000000..243eca5 Binary files /dev/null and b/src/session_ir/__pycache__/cli.cpython-311.pyc differ diff --git a/src/session_ir/__pycache__/machine.cpython-311.pyc b/src/session_ir/__pycache__/machine.cpython-311.pyc new file mode 100644 index 0000000..355d5d8 Binary files /dev/null and b/src/session_ir/__pycache__/machine.cpython-311.pyc differ diff --git a/src/session_ir/__pycache__/parser.cpython-311.pyc b/src/session_ir/__pycache__/parser.cpython-311.pyc new file mode 100644 index 0000000..955afca Binary files /dev/null and b/src/session_ir/__pycache__/parser.cpython-311.pyc differ diff --git a/src/session_ir/__pycache__/syntax.cpython-311.pyc b/src/session_ir/__pycache__/syntax.cpython-311.pyc new file mode 100644 index 0000000..373b592 Binary files /dev/null and b/src/session_ir/__pycache__/syntax.cpython-311.pyc differ diff --git a/src/session_ir/checker.py b/src/session_ir/checker.py new file mode 100644 index 0000000..24716a3 --- /dev/null +++ b/src/session_ir/checker.py @@ -0,0 +1,323 @@ +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +"""Syntax-directed checker for the Session IR: judgment Gamma |- e : A | r. + +r is the communication-step count in the max-plus semiring (N, max, +, 0): +sequential composition adds; alternative branches take max. The only grade +in v0. Memory is enforced by linear uniqueness (no second grade): every Buf +and endpoint name appears exactly once in the context or is consumed. + +Rules (ULTRAPLAN Phase 1, in MaxPlus notation; op_seq = +, op_add = max): + + unit/alloc/new Gamma |- e : A | 0 + drop/close 0 + r(sub) (drop/close themselves cost 0) + pair/letpair/let r1 + r2 (sequence) + send/recv/select 1 + r(subterms) + case 1 + max_i r(branch i) + +Endpoint threading: send/recv/select update the endpoint's session type in the +residual context. `case` is a destructor: it consumes its endpoint and binds +the per-branch continuation xi : Si inside branch i. Branches must agree on +result type and on the residual linear state. +""" + +from __future__ import annotations + +from typing import Dict, List, Optional, Tuple + +from .syntax import ( + Alloc, BufT, Case, Close, Drop, E_ALIAS, E_BOUND, E_CASE_LINEAR, E_CASE_TYPE, + E_CLOSE_NOT_END, E_DOUBLE_FREE, E_DROP_TYPE, E_LEAK, E_LET_TYPE, E_PROTOCOL, + E_UNKNOWN, E_USE_AFTER_DROP, End, ExtChoice, IntChoice, Let, LetPair, MaxPlus, New, + Pair, PairT, Recv, RecvT, SIRError, Send, SendT, Select, SessT, Term, Ty, UNIT, + UnitLit, UnitT, Var, is_linear, pp_ty, dual, ty_eq, +) + +Ctx = Dict[str, Ty] + + +class CheckResult: + def __init__(self, ty: Ty, grade: int): + self.ty = ty + self.grade = grade + + +class Checker: + """Per-program checker. Keeps a graveyard of consumed names for errors.""" + + def __init__(self) -> None: + # name -> reason it left the context ("used" | "dropped" | "closed") + self.graveyard: Dict[str, str] = {} + + # -- name resolution with linear bookkeeping ---------------------------- + def _bind(self, ctx: Ctx, x: str, t: Ty, pos) -> Ctx: + if x in ctx and is_linear(ctx[x]): + raise SIRError(E_ALIAS, f"binder {x!r} shadows a live linear name", pos) + self.graveyard.pop(x, None) # fresh binding shadows a consumed name + out = dict(ctx) + out[x] = t + return out + + def _use(self, ctx: Ctx, x: str, pos) -> Tuple[Ty, Ctx]: + """Variable occurrence: consumes linear names (moves ownership).""" + if x in ctx: + t = ctx[x] + out = dict(ctx) + if is_linear(t): + del out[x] + self.graveyard[x] = "used" + return t, out + self._fail_consumed(x, pos, dropping=False) + raise AssertionError("unreachable") + + def _fail_consumed(self, x: str, pos, dropping: bool) -> None: + reason = self.graveyard.get(x) + if reason is None: + raise SIRError(E_UNKNOWN, f"unbound name {x!r}", pos) + if dropping and reason == "dropped": + raise SIRError(E_DOUBLE_FREE, + f"buffer {x!r} was already dropped", pos) + if reason == "dropped": + raise SIRError(E_USE_AFTER_DROP, + f"buffer {x!r} was dropped before this use", pos) + if reason == "closed": + raise SIRError(E_USE_AFTER_DROP, + f"endpoint {x!r} was closed before this use " + f"(use-after-close)", pos) + raise SIRError(E_ALIAS, + f"linear name {x!r} already consumed at an earlier " + f"occurrence (aliasing)", pos) + + def _use_ep(self, ctx: Ctx, x: str, pos) -> Tuple[SessT, Ctx]: + """Endpoint occurrence in channel position (send/recv/close/select/case).""" + if x in ctx: + t = ctx[x] + if not isinstance(t, SessT): + raise SIRError(E_PROTOCOL, + f"{x!r} : {pp_ty(t)} used where a session " + f"endpoint is required", pos) + return t, ctx + self._fail_consumed(x, pos, dropping=False) + raise AssertionError("unreachable") + + def _consume_ep(self, ctx: Ctx, x: str, reason: str, pos) -> Ctx: + out = dict(ctx) + del out[x] + self.graveyard[x] = reason + return out + + # -- the judgment ------------------------------------------------------- + def check(self, ctx: Ctx, e: Term) -> Tuple[Ty, int, Ctx]: + if isinstance(e, Var): + t, out = self._use(ctx, e.name, e.pos) + return t, MaxPlus.zero, out + + if isinstance(e, UnitLit): + return UNIT, MaxPlus.zero, ctx + + if isinstance(e, Alloc): + return BufT(e.n), MaxPlus.zero, ctx + + if isinstance(e, Drop): + if isinstance(e.e, Var): + x = e.e.name + if x not in ctx: + self._fail_consumed(x, e.e.pos, dropping=True) + t = ctx[x] + if isinstance(t, SessT): + raise SIRError( + E_DROP_TYPE, + f"drop {x!r} : endpoint — endpoints are consumed by " + f"close, not drop (D5)", e.pos) + if not isinstance(t, BufT): + raise SIRError( + E_DROP_TYPE, + f"drop {x!r} : {pp_ty(t)} — only Buf n can be dropped", + e.pos) + out = self._consume_ep(ctx, x, "dropped", e.pos) + return UNIT, MaxPlus.zero, out + t, r, out = self.check(ctx, e.e) + if isinstance(t, SessT): + raise SIRError(E_DROP_TYPE, + "drop of an endpoint — use close (D5)", e.pos) + if not isinstance(t, BufT): + raise SIRError(E_DROP_TYPE, + f"drop of {pp_ty(t)} — only Buf n can be dropped", + e.pos) + return UNIT, r, out + + if isinstance(e, Pair): + t1, r1, c1 = self.check(ctx, e.e1) + t2, r2, c2 = self.check(c1, e.e2) + return PairT(t1, t2), MaxPlus.op_mul(r1, r2), c2 + + if isinstance(e, LetPair): + t1, r1, c1 = self.check(ctx, e.e1) + if not isinstance(t1, PairT): + raise SIRError(E_PROTOCOL, + f"letpair on {pp_ty(t1)} — expected a pair", e.pos) + if e.x == e.y: + raise SIRError(E_ALIAS, + f"letpair binds both components as {e.x!r}", e.pos) + c1 = self._bind(c1, e.x, t1.a, e.pos) + c1 = self._bind(c1, e.y, t1.b, e.pos) + t2, r2, c2 = self.check(c1, e.e2) + return t2, MaxPlus.op_mul(r1, r2), c2 + + if isinstance(e, New): + return PairT(SessT(e.s), SessT(dual(e.s))), MaxPlus.zero, ctx + + if isinstance(e, SendT): + s_ep, c0 = self._use_ep(ctx, e.ep, e.pos) + if not isinstance(s_ep.s, Send): + raise SIRError( + E_PROTOCOL, + f"send on {e.ep!r} : {pp_ty(s_ep)} — endpoint does not " + f"offer !A.S", e.pos) + # The endpoint is in channel position: not visible inside the value. + c_pre = dict(c0) + del c_pre[e.ep] + tv, rv, c1 = self.check(c_pre, e.val) + if not ty_eq(tv, s_ep.s.msg): + raise SIRError( + E_PROTOCOL, + f"send on {e.ep!r}: message type {pp_ty(tv)} does not " + f"match declared {pp_ty(s_ep.s.msg)}", e.pos) + c1[e.ep] = SessT(s_ep.s.cont) + return UNIT, MaxPlus.op_mul(MaxPlus.one, rv), c1 + + if isinstance(e, RecvT): + s_ep, c0 = self._use_ep(ctx, e.ep, e.pos) + if not isinstance(s_ep.s, Recv): + raise SIRError( + E_PROTOCOL, + f"recv on {e.ep!r} : {pp_ty(s_ep)} — endpoint does not " + f"offer ?A.S", e.pos) + c0[e.ep] = SessT(s_ep.s.cont) + return s_ep.s.msg, MaxPlus.one, c0 + + if isinstance(e, Close): + s_ep, c0 = self._use_ep(ctx, e.ep, e.pos) + if not isinstance(s_ep.s, End): + raise SIRError( + E_CLOSE_NOT_END, + f"close {e.ep!r} : {pp_ty(s_ep)} — endpoint is not at End", + e.pos) + out = self._consume_ep(c0, e.ep, "closed", e.pos) + return UNIT, MaxPlus.zero, out + + if isinstance(e, Select): + s_ep, c0 = self._use_ep(ctx, e.ep, e.pos) + if not isinstance(s_ep.s, IntChoice): + raise SIRError( + E_PROTOCOL, + f"select on {e.ep!r} : {pp_ty(s_ep)} — endpoint does not " + f"offer +{{...}}", e.pos) + labels = dict(s_ep.s.branches) + if e.label not in labels: + raise SIRError( + E_PROTOCOL, + f"select {e.label!r} not offered by {e.ep!r} : " + f"{pp_ty(s_ep)}", e.pos) + c0[e.ep] = SessT(labels[e.label]) + return UNIT, MaxPlus.one, c0 + + if isinstance(e, Case): + s_ep, c0 = self._use_ep(ctx, e.ep, e.pos) + if not isinstance(s_ep.s, ExtChoice): + hint = (" — endpoint offers +{...}; use select" + if isinstance(s_ep.s, IntChoice) else "") + raise SIRError( + E_PROTOCOL, + f"case on {e.ep!r} : {pp_ty(s_ep)} — endpoint does not " + f"offer &{{...}}{hint}", e.pos) + offered = dict(s_ep.s.branches) + given = {lab for lab, _, _ in e.branches} + if given != set(offered): + missing = sorted(set(offered) - given) + extra = sorted(given - set(offered)) + raise SIRError( + E_PROTOCOL, + f"case on {e.ep!r} must cover exactly the offered labels; " + f"missing={missing} extra={extra}", e.pos) + # case is a destructor: the scrutinee name leaves the context and + # each branch binds its continuation as xi : Si. + base = dict(c0) + del base[e.ep] + self.graveyard[e.ep] = "used" + res_ty: Optional[Ty] = None + res_ctx: Optional[Ctx] = None # linear part only: unrestricted + grades: List[int] = [] # names may differ across branches + + def linear_part(c: Ctx) -> Ctx: + return {n: t for n, t in c.items() if is_linear(t)} + + for lab, x, body in e.branches: + bi = self._bind(base, x, SessT(offered[lab]), e.pos) + t, r, c = self.check(bi, body) + grades.append(r) + last_ctx = c + lin = linear_part(c) + if res_ty is None: + res_ty, res_ctx = t, lin + else: + if not ty_eq(t, res_ty): + raise SIRError( + E_CASE_TYPE, + f"branch {lab!r} returns {pp_ty(t)} but an " + f"earlier branch returns {pp_ty(res_ty)}", e.pos) + if lin != res_ctx: + raise SIRError( + E_CASE_LINEAR, + f"branch {lab!r} leaves a different live linear " + f"state than earlier branches " + f"({sorted(lin)} vs {sorted(res_ctx or {})}) " + f"— all branches must agree", e.pos) + assert res_ty is not None and res_ctx is not None + # Post-case context: the (branch-independent) linear part plus the + # unrestricted names that were live before the case. Branch-local + # binders do not escape their branch. + out_ctx: Ctx = dict(res_ctx) + for n, t in base.items(): + if not is_linear(t): + out_ctx[n] = t + return res_ty, MaxPlus.op_mul(MaxPlus.one, MaxPlus.op_sum(grades)), out_ctx + + if isinstance(e, Let): + t1, r1, c1 = self.check(ctx, e.e1) + if e.ann is not None and not ty_eq(t1, e.ann): + raise SIRError(E_LET_TYPE, + f"let {e.x!r}: annotation says {pp_ty(e.ann)} " + f"but e1 has type {pp_ty(t1)}", e.pos) + if e.bound is not None and r1 > e.bound: + raise SIRError(E_BOUND, + f"let {e.x!r}: computed grade {r1} exceeds " + f"claimed bound @{e.bound}", e.pos) + if e.x == "_": + if is_linear(t1): + raise SIRError(E_LEAK, + f"linear value of type {pp_ty(t1)} " + f"discarded to _", e.pos) + else: + c1 = self._bind(c1, e.x, t1, e.pos) + t2, r2, c2 = self.check(c1, e.e2) + return t2, MaxPlus.op_mul(r1, r2), c2 + + raise AssertionError(f"unreachable term {e!r}") + + +def check_program(e: Term) -> CheckResult: + """Top level: result must be Unit and every linear name must be consumed.""" + ck = Checker() + t, r, out = ck.check({}, e) + if is_linear(t): + raise SIRError(E_LEAK, + f"top-level result {pp_ty(t)} is linear and is not " + f"consumed", e.pos) + leaked = sorted(n for n, ty in out.items() if is_linear(ty)) + if leaked: + raise SIRError(E_LEAK, + f"linear resources never consumed: " + f"{', '.join(f'{n} : {pp_ty(out[n])}' for n in leaked)}", + e.pos) + return CheckResult(t, r) diff --git a/src/session_ir/cli.py b/src/session_ir/cli.py new file mode 100644 index 0000000..62811b9 --- /dev/null +++ b/src/session_ir/cli.py @@ -0,0 +1,145 @@ +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +"""CLI for the Session IR checker/stepper. + + python3 -m session_ir check FILE type-check; print A|r or error + python3 -m session_ir run FILE check, then step; assert steps <= r + python3 -m session_ir test MANIFEST run every example in a manifest + +Exit codes: 0 ok, 1 failure (type error, unsound bound, example mismatch), +2 usage error. +""" + +from __future__ import annotations + +import json +import sys +from typing import Any, Dict, List, Optional + +from .checker import check_program +from .machine import run_program +from .syntax import SIRError, pp_ty +from .parser import parse + + +def cmd_check(path: str) -> int: + try: + with open(path, encoding="utf-8") as f: + src = f.read() + e = parse(src) + res = check_program(e) + except SIRError as err: + print(f"ERR {err.code}: {err.msg}" + (f" (at {err.pos[0]}:{err.pos[1]})" if err.pos else "")) + return 1 + print(f"OK {pp_ty(res.ty)} | {res.grade}") + return 0 + + +def cmd_run(path: str, trace: bool = False) -> int: + try: + with open(path, encoding="utf-8") as f: + src = f.read() + e = parse(src) + res = check_program(e) + stats = run_program(e) + except SIRError as err: + print(f"ERR {err.code}: {err.msg}" + (f" (at {err.pos[0]}:{err.pos[1]})" if err.pos else "")) + return 1 + ok = stats.comm_steps <= res.grade + verdict = "steps <= grade OK" if ok else "R_UNSOUND: steps exceeded grade" + print(f"OK {pp_ty(res.ty)} | grade={res.grade} steps={stats.comm_steps} " + f"peak_live={stats.peak_live} peak_inflight={stats.peak_inflight} " + f"certified/measured={res.grade / stats.comm_steps if stats.comm_steps else 0:.2f} " + f"— {verdict}") + if trace: + for line in stats.trace: + print(f" | {line}") + return 0 if ok else 1 + + +def cmd_test(manifest_path: str) -> int: + with open(manifest_path, encoding="utf-8") as f: + manifest = json.load(f) + base = manifest_path.rsplit("/", 1)[0] if "/" in manifest_path else "." + rows: List[str] = [] + failures = 0 + for case in manifest["examples"]: + rel = case["file"] + path = f"{base}/{rel}" + expect = case["expect"] + got_label = "" + verdict = "" + try: + with open(path, encoding="utf-8") as f: + src = f.read() + e = parse(src) + res = check_program(e) + if expect == "reject": + got_label = f"accepted ({pp_ty(res.ty)} | {res.grade})" + verdict = "FAIL (expected reject)" + failures += 1 + else: + want_ty = case.get("type") + want_grade = case.get("grade") + problems = [] + if want_ty is not None and pp_ty(res.ty) != want_ty: + problems.append(f"type {pp_ty(res.ty)} != {want_ty}") + if want_grade is not None and res.grade != want_grade: + problems.append(f"grade {res.grade} != {want_grade}") + got_label = f"{pp_ty(res.ty)} | {res.grade}" + if problems: + verdict = "FAIL (" + "; ".join(problems) + ")" + failures += 1 + else: + stats = run_program(e) + if stats.comm_steps > res.grade: + verdict = f"FAIL (R_UNSOUND steps={stats.comm_steps} > {res.grade})" + failures += 1 + elif "steps" in case and stats.comm_steps != case["steps"]: + verdict = f"FAIL (steps {stats.comm_steps} != {case['steps']})" + failures += 1 + elif "peak_live" in case and stats.peak_live != case["peak_live"]: + verdict = f"FAIL (peak_live {stats.peak_live} != {case['peak_live']})" + failures += 1 + else: + verdict = (f"PASS steps={stats.comm_steps}<=r " + f"peak_live={stats.peak_live}") + except SIRError as err: + if expect == "reject": + want = case.get("error") + if want is not None and err.code != want: + got_label = err.code + verdict = f"FAIL (wrong error: {err.code}, want {want})" + failures += 1 + else: + got_label = err.code + verdict = "PASS (rejected)" + else: + got_label = err.code + verdict = f"FAIL (unexpected {err.code})" + failures += 1 + rows.append(f" {rel:<34} {expect:<7} -> {got_label:<28} {verdict}") + + print(f"{'file':<36} {'expect':<7} {'got':<28} verdict") + for r in rows: + print(r) + total = len(manifest["examples"]) + print(f"{total - failures}/{total} examples OK") + return 1 if failures else 0 + + +def main(argv: Optional[List[str]] = None) -> int: + args = argv if argv is not None else sys.argv[1:] + if len(args) == 2 and args[0] == "check": + return cmd_check(args[1]) + if len(args) in (2, 3) and args[0] == "run": + return cmd_run(args[1], trace=(len(args) == 3 and args[2] == "--trace")) + if len(args) == 2 and args[0] == "test": + return cmd_test(args[1]) + print("usage: python3 -m session_ir {check FILE | run FILE [--trace] | " + "test MANIFEST}", file=sys.stderr) + return 2 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/src/session_ir/machine.py b/src/session_ir/machine.py new file mode 100644 index 0000000..48d0e8c --- /dev/null +++ b/src/session_ir/machine.py @@ -0,0 +1,243 @@ +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +"""Deterministic stepper for closed Session IR programs. + +Machine configuration (docs/OPERATIONAL-MODEL.md): + * heap: linear buffers, explicit drop only (no GC, no implicit copy); + * channels: two queues between paired endpoints (created by `new`); + * one thread of control (single program term, lets sequence everything); + * clock: communication steps (send / recv / select / case each count 1). + +Statistics recorded (operational readings, NOT grades in v0): + * comm_steps — measured cost, asserted <= certified grade r; + * peak_live — high-water mark of live buffer bytes; + * peak_inflight — high-water mark of queued channel events. + +Machine-level errors (R_*) should be unreachable for well-typed programs; +they are machine self-checks, and fire loudly if the checker and the machine +ever disagree. +""" + +from __future__ import annotations + +from typing import Any, Dict, List, Optional, Tuple + +from .syntax import ( + Alloc, BufT, Case, Close, Drop, E_PROTOCOL, End, Let, LetPair, MaxPlus, New, + Pair, PairT, R_CLOSE_PENDING, R_DEADLOCK, R_INTERNAL, RecvT, SIRError, SendT, + Select, SessT, Term, UnitLit, Var, is_linear, pp_ty, +) + + +class BufVal: + __slots__ = ("bid", "size", "dropped") + + def __init__(self, bid: int, size: int): + self.bid = bid + self.size = size + self.dropped = False + + def __repr__(self) -> str: + return f"" + + +class EpVal: + __slots__ = ("chan", "side") + + def __init__(self, chan: "Chan", side: str): + self.chan = chan + self.side = side # "a" | "b" + + def __repr__(self) -> str: + return f"" + + +class Chan: + __slots__ = ("cid", "queues", "closed") + + def __init__(self, cid: int): + self.cid = cid + self.queues: Dict[str, List[Tuple[str, Any]]] = {"a": [], "b": []} + self.closed = {"a": False, "b": False} + + @staticmethod + def other(side: str) -> str: + return "b" if side == "a" else "a" + + +class PairVal: + __slots__ = ("v1", "v2") + + def __init__(self, v1: Any, v2: Any): + self.v1 = v1 + self.v2 = v2 + + +class RunStats: + def __init__(self) -> None: + self.comm_steps = 0 + self.peak_live = 0 + self.peak_inflight = 0 + self.live_bytes = 0 + self.trace: List[str] = [] + + def note(self, msg: str) -> None: + self.trace.append(msg) + + +class Machine: + def __init__(self) -> None: + self.stats = RunStats() + self.next_bid = 0 + self.next_cid = 0 + self.chans: List[Chan] = [] + + # -- helpers ------------------------------------------------------------ + def _inflight(self) -> int: + return sum(len(q) for c in self.chans for q in c.queues.values()) + + def _touch_inflight(self) -> None: + self.stats.peak_inflight = max(self.stats.peak_inflight, self._inflight()) + + def _ep(self, env: Dict[str, Any], name: str, pos) -> EpVal: + v = env.get(name) + if not isinstance(v, EpVal): + raise SIRError(R_INTERNAL, + f"{name!r} is not an endpoint at runtime", pos) + return v + + # -- evaluation --------------------------------------------------------- + def run(self, e: Term) -> Any: + v = self.eval(e, {}) + # Self-check: well-typed programs drain every channel queue. + pending = self._inflight() + if pending: + raise SIRError(R_CLOSE_PENDING, + f"{pending} channel event(s) still queued at end " + f"of program", e.pos) + return v + + def eval(self, e: Term, env: Dict[str, Any]) -> Any: + st = self.stats + + if isinstance(e, Var): + return env[e.name] + + if isinstance(e, UnitLit): + return None + + if isinstance(e, Alloc): + b = BufVal(self.next_bid, e.n) + self.next_bid += 1 + st.live_bytes += e.n + st.peak_live = max(st.peak_live, st.live_bytes) + st.note(f"alloc {e.n} -> {b!r} (live={st.live_bytes})") + return b + + if isinstance(e, Drop): + v = self.eval(e.e, env) + if not isinstance(v, BufVal): + raise SIRError(R_INTERNAL, "drop of a non-buffer at runtime", e.pos) + if v.dropped: + raise SIRError(R_INTERNAL, "double free at runtime", e.pos) + v.dropped = True + st.live_bytes -= v.size + st.note(f"drop {v!r} (live={st.live_bytes})") + return None + + if isinstance(e, Pair): + return PairVal(self.eval(e.e1, env), self.eval(e.e2, env)) + + if isinstance(e, LetPair): + v = self.eval(e.e1, env) + if not isinstance(v, PairVal): + raise SIRError(R_INTERNAL, "letpair of a non-pair", e.pos) + env2 = dict(env) + env2[e.x] = v.v1 + env2[e.y] = v.v2 + return self.eval(e.e2, env2) + + if isinstance(e, New): + c = Chan(self.next_cid) + self.next_cid += 1 + self.chans.append(c) + st.note(f"new channel {c.cid} ({pp_ty(SessT(e.s))} | dual)") + return PairVal(EpVal(c, "a"), EpVal(c, "b")) + + if isinstance(e, SendT): + ep = self._ep(env, e.ep, e.pos) + v = self.eval(e.val, env) + ep.chan.queues[Chan.other(ep.side)].append(("msg", v)) + st.comm_steps += 1 + self._touch_inflight() + st.note(f"send {ep!r} (step {st.comm_steps})") + return None + + if isinstance(e, RecvT): + ep = self._ep(env, e.ep, e.pos) + q = ep.chan.queues[ep.side] + if not q: + raise SIRError(R_DEADLOCK, + f"recv on {e.ep!r} with nothing in flight", e.pos) + kind, v = q.pop(0) + if kind != "msg": + raise SIRError(R_INTERNAL, "recv found a selection, not a message", + e.pos) + st.comm_steps += 1 + self._touch_inflight() + st.note(f"recv {ep!r} (step {st.comm_steps})") + return v + + if isinstance(e, Select): + ep = self._ep(env, e.ep, e.pos) + ep.chan.queues[Chan.other(ep.side)].append(("sel", e.label)) + st.comm_steps += 1 + self._touch_inflight() + st.note(f"select {e.label!r} on {ep!r} (step {st.comm_steps})") + return None + + if isinstance(e, Case): + ep = self._ep(env, e.ep, e.pos) + q = ep.chan.queues[ep.side] + if not q: + raise SIRError(R_DEADLOCK, + f"case on {e.ep!r} with nothing in flight", e.pos) + kind, lab = q.pop(0) + if kind != "sel": + raise SIRError(R_INTERNAL, "case found a message, not a selection", + e.pos) + st.comm_steps += 1 + self._touch_inflight() + st.note(f"case {ep!r} -> {lab!r} (step {st.comm_steps})") + for blab, x, body in e.branches: + if blab == lab: + env2 = dict(env) + env2[x] = ep # continuation is the same endpoint value + return self.eval(body, env2) + raise SIRError(R_INTERNAL, f"selected label {lab!r} has no branch", e.pos) + + if isinstance(e, Close): + ep = self._ep(env, e.ep, e.pos) + if ep.chan.closed[ep.side]: + raise SIRError(R_INTERNAL, "endpoint closed twice at runtime", e.pos) + if ep.chan.queues[ep.side]: + raise SIRError(R_CLOSE_PENDING, + f"close {e.ep!r} with unconsumed messages", e.pos) + ep.chan.closed[ep.side] = True + st.note(f"close {ep!r}") + return None + + if isinstance(e, Let): + v = self.eval(e.e1, env) + if e.x != "_": + env = dict(env) + env[e.x] = v + return self.eval(e.e2, env) + + raise AssertionError(f"unreachable term {e!r}") + + +def run_program(e: Term) -> RunStats: + m = Machine() + m.run(e) + return m.stats diff --git a/src/session_ir/parser.py b/src/session_ir/parser.py new file mode 100644 index 0000000..14dd01b --- /dev/null +++ b/src/session_ir/parser.py @@ -0,0 +1,326 @@ +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +"""Lexer + recursive-descent parser for the Session IR concrete syntax. + +Concrete syntax (comments are (* ... *), non-nested): + + e ::= unit | alloc INT | drop e | pair e e + | letpair x y = e in e + | new t | send x e | recv x | close x | select l x + | case x { l: y. e , ... } + | let x [: t] [@ INT] = e in e + | ( e ) | x + + t ::= Unit | Buf INT | t * t | s | ( t ) + s ::= End | ! t . s | ? t . s | + { l: t, ... } | & { l: t, ... } + +The channel operand of send/recv/close/select/case must be a name (the linear +typing of endpoints is name-based). +""" + +from __future__ import annotations + +from typing import List, Optional, Tuple + +from .syntax import ( + Alloc, BufT, Case, Close, Drop, End, ExtChoice, IntChoice, Let, LetPair, + New, Pair, PairT, Recv, RecvT, Sess, SessT, SIRError, Send, SendT, Select, + Term, Ty, UNIT, UnitLit, UnitT, Var, E_SYNTAX, +) + +KEYWORDS = { + "unit", "alloc", "drop", "pair", "letpair", "in", "new", "send", "recv", + "close", "select", "case", "let", +} + +# token kinds: NAME, INT, SYM, EOF +_TOK = Tuple[str, str, int, int] # (kind, text, line, col) + + +class Lexer: + def __init__(self, src: str): + self.src = src + self.i = 0 + self.line = 1 + self.col = 1 + + def _peek(self) -> str: + return self.src[self.i] if self.i < len(self.src) else "" + + def _bump(self) -> str: + ch = self.src[self.i] + self.i += 1 + if ch == "\n": + self.line += 1 + self.col = 1 + else: + self.col += 1 + return ch + + def tokens(self) -> List[_TOK]: + out: List[_TOK] = [] + while True: + self._skip_ws() + line, col = self.line, self.col + ch = self._peek() + if ch == "": + out.append(("EOF", "", line, col)) + return out + if ch == "(" and self.src[self.i:self.i + 2] == "(*": + self._comment(line, col) + continue + if ch.isdigit(): + n = "" + while self._peek().isdigit(): + n += self._bump() + out.append(("INT", n, line, col)) + continue + if ch.isalpha() or ch == "_": + n = "" + while True: + c = self._peek() + if c.isalnum() or c in "_'": + n += self._bump() + else: + break + out.append(("NAME", n, line, col)) + continue + if ch in "!?+&*.,{}()=:@[": + out.append(("SYM", self._bump(), line, col)) + continue + raise SIRError(E_SYNTAX, f"unexpected character {ch!r}", (line, col)) + + def _skip_ws(self) -> None: + while self._peek() and self._peek() in " \t\r\n": + self._bump() + + def _comment(self, line: int, col: int) -> None: + self._bump() # ( + self._bump() # * + while True: + if self._peek() == "": + raise SIRError(E_SYNTAX, "unterminated comment", (line, col)) + if self.src[self.i:self.i + 2] == "*)": + self._bump() + self._bump() + return + self._bump() + + +class Parser: + def __init__(self, src: str): + self.toks: List[_TOK] = Lexer(src).tokens() + self.p = 0 + + # -- token helpers ------------------------------------------------------ + def _tok(self) -> _TOK: + return self.toks[self.p] + + def _pos(self) -> Tuple[int, int]: + t = self._tok() + return (t[2], t[3]) + + def _at(self, kind: str, text: Optional[str] = None) -> bool: + t = self._tok() + return t[0] == kind and (text is None or t[1] == text) + + def _eat(self, kind: str, text: Optional[str] = None) -> _TOK: + if not self._at(kind, text): + t = self._tok() + want = text if text is not None else kind + got = t[1] if t[1] else t[0] + raise SIRError(E_SYNTAX, f"expected {want!r}, found {got!r}", (t[2], t[3])) + t = self._tok() + self.p += 1 + return t + + def _at_name(self, kw: str) -> bool: + return self._at("NAME", kw) + + # -- entry -------------------------------------------------------------- + def parse_program(self) -> Term: + e = self.parse_term() + self._eat("EOF") + return e + + # -- types & sessions --------------------------------------------------- + def parse_type(self) -> Ty: + t = self.parse_type_atom() + while self._at("SYM", "*"): + self._eat("SYM", "*") + t = PairT(t, self.parse_type_atom()) + return t + + def parse_type_atom(self) -> Ty: + tk = self._tok() + if self._at("NAME", "Unit"): + self._eat("NAME", "Unit") + return UNIT + if self._at("NAME", "Buf"): + self._eat("NAME", "Buf") + n = int(self._eat("INT")[1]) + return BufT(n) + if self._at("NAME", "End"): + return SessT(self.parse_session_atom()) + if self._at("SYM", "!") or self._at("SYM", "?") \ + or self._at("SYM", "+") or self._at("SYM", "&"): + return SessT(self.parse_session_atom()) + if self._at("SYM", "("): + self._eat("SYM", "(") + t = self.parse_type() + self._eat("SYM", ")") + return t + raise SIRError(E_SYNTAX, f"expected a type, found {tk[1] or tk[0]!r}", + (tk[2], tk[3])) + + def parse_session_atom(self) -> Sess: + tk = self._tok() + if self._at("NAME", "End"): + self._eat("NAME", "End") + return End() + if self._at("SYM", "!") or self._at("SYM", "?"): + is_send = self._eat("SYM")[1] == "!" + msg = self.parse_type() + self._eat("SYM", ".") + cont = self.parse_type() + if not isinstance(cont, SessT): + raise SIRError(E_SYNTAX, + "session continuation after '.' must be a session type", + self._pos()) + return Send(msg, cont.s) if is_send else Recv(msg, cont.s) + if self._at("SYM", "+") or self._at("SYM", "&"): + is_int = self._eat("SYM")[1] == "+" + self._eat("SYM", "{") + brs = [] + seen = set() + while not self._at("SYM", "}"): + lab = self._eat("NAME")[1] + if lab in seen: + raise SIRError(E_SYNTAX, f"duplicate branch label {lab!r}", self._pos()) + seen.add(lab) + self._eat("SYM", ":") + s = self.parse_type() + if not isinstance(s, SessT): + raise SIRError(E_SYNTAX, + f"branch {lab!r} continuation must be a session type", + self._pos()) + brs.append((lab, s.s)) + if self._at("SYM", ","): + self._eat("SYM", ",") + self._eat("SYM", "}") + if not brs: + raise SIRError(E_SYNTAX, "choice must have at least one branch", self._pos()) + return IntChoice(tuple(brs)) if is_int else ExtChoice(tuple(brs)) + raise SIRError(E_SYNTAX, f"expected a session type, found {tk[1] or tk[0]!r}", + (tk[2], tk[3])) + + # -- terms -------------------------------------------------------------- + def parse_term(self) -> Term: + tk = self._tok() + pos = (tk[2], tk[3]) + + if self._at("SYM", "("): + self._eat("SYM", "(") + e = self.parse_term() + self._eat("SYM", ")") + return e + + if self._at("NAME", "unit"): + self._eat("NAME", "unit") + return UnitLit(pos) + + if self._at("NAME", "alloc"): + self._eat("NAME", "alloc") + return Alloc(int(self._eat("INT")[1]), pos) + + if self._at("NAME", "drop"): + self._eat("NAME", "drop") + return Drop(self.parse_term(), pos) + + if self._at("NAME", "pair"): + self._eat("NAME", "pair") + return Pair(self.parse_term(), self.parse_term(), pos) + + if self._at("NAME", "letpair"): + self._eat("NAME", "letpair") + x = self._eat("NAME")[1] + y = self._eat("NAME")[1] + self._eat("SYM", "=") + e1 = self.parse_term() + self._eat("NAME", "in") + return LetPair(x, y, e1, self.parse_term(), pos) + + if self._at("NAME", "new"): + self._eat("NAME", "new") + t = self.parse_type() + if not isinstance(t, SessT): + raise SIRError(E_SYNTAX, "new expects a session type", self._pos()) + return New(t.s, pos) + + if self._at("NAME", "send"): + self._eat("NAME", "send") + ep = self._eat("NAME")[1] + return SendT(ep, self.parse_term(), pos) + + if self._at("NAME", "recv"): + self._eat("NAME", "recv") + return RecvT(self._eat("NAME")[1], pos) + + if self._at("NAME", "close"): + self._eat("NAME", "close") + return Close(self._eat("NAME")[1], pos) + + if self._at("NAME", "select"): + self._eat("NAME", "select") + lab = self._eat("NAME")[1] + return Select(lab, self._eat("NAME")[1], pos) + + if self._at("NAME", "case"): + self._eat("NAME", "case") + ep = self._eat("NAME")[1] + self._eat("SYM", "{") + brs = [] + seen = set() + while not self._at("SYM", "}"): + lab = self._eat("NAME")[1] + if lab in seen: + raise SIRError(E_SYNTAX, f"duplicate branch label {lab!r}", self._pos()) + seen.add(lab) + self._eat("SYM", ":") + x = self._eat("NAME")[1] + self._eat("SYM", ".") + brs.append((lab, x, self.parse_term())) + if self._at("SYM", ","): + self._eat("SYM", ",") + self._eat("SYM", "}") + if not brs: + raise SIRError(E_SYNTAX, "case must have at least one branch", self._pos()) + return Case(ep, tuple(brs), pos) + + if self._at("NAME", "let"): + self._eat("NAME", "let") + x = self._eat("NAME")[1] + ann: Optional[Ty] = None + bound: Optional[int] = None + if self._at("SYM", ":"): + self._eat("SYM", ":") + ann = self.parse_type() + if self._at("SYM", "@"): + self._eat("SYM", "@") + bound = int(self._eat("INT")[1]) + self._eat("SYM", "=") + e1 = self.parse_term() + self._eat("NAME", "in") + return Let(x, ann, bound, e1, self.parse_term(), pos) + + if self._at("NAME"): + name = self._eat("NAME")[1] + if name in KEYWORDS: + raise SIRError(E_SYNTAX, f"keyword {name!r} used as a variable", pos) + return Var(name, pos) + + raise SIRError(E_SYNTAX, f"expected a term, found {tk[1] or tk[0]!r}", pos) + + +def parse(src: str) -> Term: + return Parser(src).parse_program() diff --git a/src/session_ir/syntax.py b/src/session_ir/syntax.py new file mode 100644 index 0000000..b484581 --- /dev/null +++ b/src/session_ir/syntax.py @@ -0,0 +1,309 @@ +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +"""Abstract syntax for the occupancy-types Session IR (v0). + +Types: Unit | Buf n | A * B | S +Sessions: End | !A.S | ?A.S | +{li: Si} | &{li: Si} +Terms: unit | drop e | alloc n | pair e1 e2 | letpair x y = e1 in e2 + new S | send ep val | recv ep | close ep + select l ep | case ep {li: xi. ei} | let x [: A] [@ r] = e1 in e2 + +Judgment: Gamma |- e : A | r (r = communication-step count, max-plus) + +Design notes (see docs/OPERATIONAL-MODEL.md): + * Comm actions thread the endpoint name (send/recv/select update its session + type in the residual context); `case` is a destructor: it consumes its + endpoint and binds the per-branch continuation as `xi : Si`. + * All types except Unit are linear (Buf, session endpoints, pairs containing + them). Unit names are unrestricted. +""" + +from __future__ import annotations + +from dataclasses import dataclass, field +from typing import Dict, List, Optional, Tuple, Union + +# ── Grade semiring: max-plus (N, max, +, 0) ────────────────────────────────── +# +# The one grade of v0 is the communication-step count. Sequential composition +# adds (both actions happen); alternative branches take max (we cannot rule out +# the expensive branch). This tiny object is the importable constraint: six +# typing rules in checker.py are expressed solely in terms of it. + +GRADE_ZERO = 0 # cost of doing nothing; identity of max on N +GRADE_ONE = 1 # cost of one communication action + + +class MaxPlus: + """Semiring (N u {inf}, max, +, 0): op_add is choice, op_mul is sequence.""" + + zero = GRADE_ZERO + one = GRADE_ONE + + @staticmethod + def op_add(x: int, y: int) -> int: + """Choice: max. Worst-case guarantee is the most expensive branch.""" + return x if x >= y else y + + @staticmethod + def op_mul(x: int, y: int) -> int: + """Sequence: +. Both actions definitely happen.""" + return x + y + + @staticmethod + def op_sum(xs: List[int]) -> int: + out = GRADE_ZERO + for x in xs: + out = MaxPlus.op_add(out, x) + return out + + @staticmethod + def op_seq(xs: List[int]) -> int: + out = GRADE_ZERO + for x in xs: + out = MaxPlus.op_mul(out, x) + return out + + +# ── Errors ─────────────────────────────────────────────────────────────────── + +class SIRError(Exception): + """Structured checker/machine error with a stable code.""" + + def __init__(self, code: str, msg: str, pos: Optional[Tuple[int, int]] = None): + self.code = code + self.msg = msg + self.pos = pos + super().__init__(f"{code}: {msg}" + (f" (at {pos[0]}:{pos[1]})" if pos else "")) + + +E_UNKNOWN = "E_UNKNOWN" # unbound name +E_ALIAS = "E_ALIAS" # linear name used twice +E_USE_AFTER_DROP = "E_USE_AFTER_DROP" # use of dropped buf / closed endpoint +E_DOUBLE_FREE = "E_DOUBLE_FREE" # drop of already-consumed buffer +E_LEAK = "E_LEAK" # linear resource left unconsumed +E_PROTOCOL = "E_PROTOCOL" # session/message mismatch +E_CLOSE_NOT_END = "E_CLOSE_NOT_END" # close before End +E_DROP_TYPE = "E_DROP_TYPE" # drop of a non-Buf (e.g. endpoint) +E_BOUND = "E_BOUND" # annotated @r smaller than computed grade +E_CASE_LINEAR = "E_CASE_LINEAR" # branches leave different live linear state +E_CASE_TYPE = "E_CASE_TYPE" # branches return different types +E_LET_TYPE = "E_LET_TYPE" # let type-annotation mismatch +E_SYNTAX = "E_SYNTAX" # parse error +# Machine-level (should not fire on well-typed programs): +R_DEADLOCK = "R_DEADLOCK" # recv/select with nothing in flight +R_CLOSE_PENDING = "R_CLOSE_PENDING" # close with unconsumed messages +R_UNSOUND = "R_UNSOUND" # measured steps exceeded certified grade +R_INTERNAL = "R_INTERNAL" # machine/checker disagreement + + +# ── Types and sessions ─────────────────────────────────────────────────────── + +@dataclass(frozen=True) +class UnitT: + pass + + +@dataclass(frozen=True) +class BufT: + n: int + + +@dataclass(frozen=True) +class PairT: + a: "Ty" + b: "Ty" + + +@dataclass(frozen=True) +class End: + pass + + +@dataclass(frozen=True) +class Send: # !A.S + msg: "Ty" + cont: "Sess" + + +@dataclass(frozen=True) +class Recv: # ?A.S + msg: "Ty" + cont: "Sess" + + +@dataclass(frozen=True) +class IntChoice: # +{li: Si} internal choice (offer) + branches: Tuple[Tuple[str, "Sess"], ...] + + +@dataclass(frozen=True) +class ExtChoice: # &{li: Si} external choice (accept) + branches: Tuple[Tuple[str, "Sess"], ...] + + +@dataclass(frozen=True) +class SessT: + s: "Sess" + + +Sess = Union[End, Send, Recv, IntChoice, ExtChoice] +Ty = Union[UnitT, BufT, PairT, SessT] + +UNIT = UnitT() + + +def is_linear(t: Ty) -> bool: + """Unit is unrestricted; Buf, endpoints and pairs holding them are linear.""" + if isinstance(t, UnitT): + return False + if isinstance(t, BufT): + return True + if isinstance(t, SessT): + return True + if isinstance(t, PairT): + return is_linear(t.a) or is_linear(t.b) + raise AssertionError(f"unreachable type {t!r}") + + +def dual(s: Sess) -> Sess: + if isinstance(s, End): + return End() + if isinstance(s, Send): + return Recv(s.msg, dual(s.cont)) + if isinstance(s, Recv): + return Send(s.msg, dual(s.cont)) + if isinstance(s, IntChoice): + return ExtChoice(tuple((l, dual(c)) for l, c in s.branches)) + if isinstance(s, ExtChoice): + return IntChoice(tuple((l, dual(c)) for l, c in s.branches)) + raise AssertionError(f"unreachable session {s!r}") + + +# ── Pretty printing ────────────────────────────────────────────────────────── + +def pp_ty(t: Ty) -> str: + if isinstance(t, UnitT): + return "Unit" + if isinstance(t, BufT): + return f"Buf {t.n}" + if isinstance(t, PairT): + left = pp_ty(t.a) + if isinstance(t.a, PairT): + left = f"({left})" + return f"{left} * {pp_ty(t.b)}" + if isinstance(t, SessT): + return pp_sess(t.s) + raise AssertionError(f"unreachable type {t!r}") + + +def pp_sess(s: Sess) -> str: + if isinstance(s, End): + return "End" + if isinstance(s, Send): + return f"!{pp_ty(s.msg)}.{pp_sess(s.cont)}" + if isinstance(s, Recv): + return f"?{pp_ty(s.msg)}.{pp_sess(s.cont)}" + if isinstance(s, (IntChoice, ExtChoice)): + op = "+" if isinstance(s, IntChoice) else "&" + inner = ", ".join(f"{l}: {pp_sess(c)}" for l, c in s.branches) + return f"{op}{{{inner}}}" + raise AssertionError(f"unreachable session {s!r}") + + +def ty_eq(a: Ty, b: Ty) -> bool: + return a == b + + +# ── Terms ──────────────────────────────────────────────────────────────────── + +@dataclass(frozen=True) +class Var: + name: str + pos: Tuple[int, int] = field(default=(0, 0)) + + +@dataclass(frozen=True) +class UnitLit: + pos: Tuple[int, int] = (0, 0) + + +@dataclass(frozen=True) +class Alloc: + n: int + pos: Tuple[int, int] = (0, 0) + + +@dataclass(frozen=True) +class Drop: + e: "Term" + pos: Tuple[int, int] = (0, 0) + + +@dataclass(frozen=True) +class Pair: + e1: "Term" + e2: "Term" + pos: Tuple[int, int] = (0, 0) + + +@dataclass(frozen=True) +class LetPair: + x: str + y: str + e1: "Term" + e2: "Term" + pos: Tuple[int, int] = (0, 0) + + +@dataclass(frozen=True) +class New: + s: Sess + pos: Tuple[int, int] = (0, 0) + + +@dataclass(frozen=True) +class SendT: # send ep val + ep: str + val: "Term" + pos: Tuple[int, int] = (0, 0) + + +@dataclass(frozen=True) +class RecvT: # recv ep + ep: str + pos: Tuple[int, int] = (0, 0) + + +@dataclass(frozen=True) +class Close: + ep: str + pos: Tuple[int, int] = (0, 0) + + +@dataclass(frozen=True) +class Select: + label: str + ep: str + pos: Tuple[int, int] = (0, 0) + + +@dataclass(frozen=True) +class Case: + ep: str + branches: Tuple[Tuple[str, str, "Term"], ...] # (label, binder, body) + pos: Tuple[int, int] = (0, 0) + + +@dataclass(frozen=True) +class Let: + x: str + ann: Optional[Ty] # optional type annotation + bound: Optional[int] # optional claimed grade bound @r + e1: "Term" + e2: "Term" + pos: Tuple[int, int] = (0, 0) + + +Term = Union[Var, UnitLit, Alloc, Drop, Pair, LetPair, New, + SendT, RecvT, Close, Select, Case, Let] diff --git a/src/stackcert/Main.lean b/src/stackcert/Main.lean new file mode 100644 index 0000000..e7448f5 --- /dev/null +++ b/src/stackcert/Main.lean @@ -0,0 +1,178 @@ +/- +SPDX-License-Identifier: MPL-2.0 +SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) + +Main — lake exe stackcert --ci F.ci --su F.su --ann annotations.toml --cert cert.toml +→ exit 0 (certificate accepted) / 1 (rejected) / 2 (usage). + +Pipeline: parse inputs (UNVERIFIED layer) → build CallGraph → run +StackcertCore.check (verified layer) → report. CLI-level rejections before +the core runs: unresolved indirect calls, alloca/VLA-style dynamic frames +without a [dynamic] bound, call edges into longjmp-family functions, and +non-self cycles without annotation. See README.adoc for the fixture request +and ground-truth protocol; this exe's outputs are NOT yet a measurement. +-/ + +import StackcertCore +import Parsers + +open StackcertCore StackcertParsers + +def lookupNat (l : List (String × Nat)) (k : String) : Option Nat := + match l with + | [] => none + | (k', v) :: rest => if k == k' then some v else lookupNat rest k + +def lookupStrs (l : List (String × List String)) (k : String) : Option (List String) := + match l with + | [] => none + | (k', v) :: rest => if k == k' then some v else lookupStrs rest k + +def dedup (l : List String) : List String := + l.foldl (fun acc x => if acc.any (fun y => y == x) then acc else acc ++ [x]) [] + +def isForbiddenTarget (t : String) : Bool := + t == "alloca" || t == "__builtin_alloca" || t == "longjmp" + || t == "_longjmp" || t == "__longjmp" || t == "__longjmp_chk" + || t == "_setjmp" || t == "__sigsetjmp" + +/-- Non-self cycle detection (CLI-level; `partial` is fine outside the proof). -/ +partial def reaches (callees : List (String × List String)) (start fuel : Nat) + (cur tgt : String) : Bool := + if fuel = 0 then false + else + match lookupStrs callees cur with + | none => false + | some ds => + ds.any (fun d => + if d == tgt then true + else if d == cur then false + else reaches callees start (fuel - 1) d tgt) + +partial def hasNonSelfCycle (names : List String) + (callees : List (String × List String)) : Option (String × String) := + match names with + | [] => none + | v :: rest => + match lookupStrs callees v with + | none => hasNonSelfCycle rest callees + | some ds => + match ds.find? (fun u => u != v && reaches callees (names.length + 1) (names.length + 1) v u) with + | some u => some (v, u) + | none => hasNonSelfCycle rest callees + +def usage : String := + "usage: stackcert --ci FILE.ci --su FILE.su --ann annotations.toml --cert cert.toml" + +def getFlag (args : List String) (flag : String) : Option String := + match args with + | [] => none + | a :: rest => if a == flag then rest.headD "" else getFlag rest flag + +def main (args : List String) : IO UInt32 := do + let ciP := getFlag args "--ci" + let suP := getFlag args "--su" + let annP := getFlag args "--ann" + let certP := getFlag args "--cert" + match ciP, suP, annP, certP with + | some ciF, some suF, some annF, some certF => do + let ciText ← IO.FS.readFile ciF + let suText ← IO.FS.readFile suF + let annText ← IO.FS.readFile annF + let certText ← IO.FS.readFile certF + match parseCI ciText, parseSU suText, parseToml annText, parseToml certText with + | .error e, _, _, _ => IO.println s!"ERR E_PARSE: {e}"; return 1 + | _, .error e, _, _ => IO.println s!"ERR E_PARSE: {e}"; return 1 + | _, _, .error e, _ => IO.println s!"ERR E_PARSE: {e}"; return 1 + | _, _, _, .error e => IO.println s!"ERR E_PARSE: {e}"; return 1 + | .ok ciItems, .ok suEntries, .ok annRows, .ok certRows => do + match annOfToml annRows, certOfToml certRows with + | .error e, _ => IO.println s!"ERR E_PARSE: {e}"; return 1 + | _, .error e => IO.println s!"ERR E_PARSE: {e}"; return 1 + | .ok ann, .ok certList => do + let suNames := suEntries.map (·.name) + let nodeNames := ciItems.filterMap (fun i => + match i with + | CiItem.node t => + let n := normName t + if n == "__indirect_call" then none -- placeholder node, not a function + else some n + | _ => none) + let names := dedup (suNames ++ nodeNames) + -- frames from .su + let frames := suEntries.map (fun e => (e.name, e.bytes)) + -- callees from .ci edges (normalized); indirect handled below + let mut callees : List (String × List String) := names.map (fun n => (n, [])) + let mut indirectUsers : List String := [] + let mut badTarget : Option String := none + for item in ciItems do + match item with + | CiItem.edge s t => + let s' := normName s + let t' := normName t + if isForbiddenTarget t' then badTarget := some t' + else + callees := callees.map (fun (k, ds) => + if k == s' then (k, if ds.any (fun x => x == t') then ds else ds ++ [t']) + else (k, ds)) + | CiItem.indirectEdge s => indirectUsers := indirectUsers ++ [normName s] + | CiItem.node _ => pure () + match badTarget with + | some t => + IO.println s!"ERR E_FORBIDDEN: call to {t} (alloca/VLA/longjmp are rejected)" + return 1 + | none => pure () + -- resolve indirect calls via [indirect] + for f in indirectUsers do + match lookupStrs ann.indirect f with + | none => + IO.println s!"ERR E_INDIRECT: unresolved indirect call in {f}" + return 1 + | some ts => + for t in ts do + if !(names.any (fun n => n == t)) then + IO.println s!"ERR E_INDIRECT: target {t} of {f} is not a known function" + return 1 + callees := callees.map (fun (k, ds) => + if k == f then (k, if ds.any (fun x => x == t) then ds else ds ++ [t]) + else (k, ds)) + -- dynamic frames need a [dynamic] bound + for e in suEntries do + match e.qual with + | Qual.static => pure () + | _ => + match lookupNat ann.dynamic e.name with + | none => + IO.println s!"ERR E_DYNAMIC: {e.name} has a dynamic/bounded frame without [dynamic] annotation" + return 1 + | some _ => pure () + -- non-self cycles rejected + match hasNonSelfCycle names callees with + | some (v, u) => + IO.println s!"ERR E_CYCLE: undeclared cycle {v} -> ... -> {u}" + return 1 + | none => pure () + -- certificates must cover every function + for n in names do + if (lookupNat certList n).isNone then + IO.println s!"ERR E_CERT: no [cert] entry for {n}" + return 1 + -- build the core model and check + let g : CallGraph String := { + fns := names + frame := fun fn => (lookupNat frames fn).getD 0 + callees := fun fn => (lookupStrs callees fn).getD [] + } + let a : Annot String := { + selfDepth := fun fn => lookupNat ann.selfDepth fn + } + let cert := fun fn : String => (lookupNat certList fn).getD 0 + if check g a cert then + IO.println s!"OK certificate accepted for {names.length} function(s)" + return 0 + else + IO.println "ERR E_CERT: certificate rejected by rule (see StackcertCore.rule)" + return 1 + | _, _, _, _ => + IO.println usage + return 2 diff --git a/src/stackcert/Parsers.lean b/src/stackcert/Parsers.lean new file mode 100644 index 0000000..0156a37 --- /dev/null +++ b/src/stackcert/Parsers.lean @@ -0,0 +1,180 @@ +/- +SPDX-License-Identifier: MPL-2.0 +SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) + +Parsers — GCC `.su` / `.ci` (VCG from -fcallgraph-info=su) and the +annotations.toml subset. UNVERIFIED I/O layer: not covered by cert_sound; +inputs are treated as untrusted text and every failure mode is an Except. +Formats were captured from real GCC output (see fixtures/). +-/ + +namespace StackcertParsers + +/-- Frame quality from .su: `static`, `dynamic`, `dynamic,bounded`. -/ +inductive Qual where + | static + | dynamic + | dynamicBounded + deriving Repr, BEq + +structure SuEntry where + name : String + bytes : Nat + qual : Qual + deriving Repr + +structure Ann where + selfDepth : List (String × Nat) -- [recursion] fn = depth + indirect : List (String × List String) -- [indirect] fn = ["target", ...] + dynamic : List (String × Nat) -- [dynamic] fn = explicit bytes + isr : List (String × Nat) -- [isr] fn = level + threads : List (String × Nat) -- [threads] fn = stack bytes + deriving Repr + +/-- Text after `needle`, up to the next double quote. -/ +def extractAfter (needle : String) (line : String) : Option String := + match line.splitOn needle with + | _ :: rest :: _ => + match rest.splitOn "\"" with + | first :: _ => some first + | _ => none + | _ => none + +def nameOfLoc (loc : String) : String := + match (loc.splitOn ":").reverse with + | n :: _ => n + | _ => loc + +/-- Parse one .su line: `file:line:col:func\tbytes\tqualifiers`. -/ +def parseSuLine (line : String) : Option SuEntry := + let fields := line.splitOn "\t" + match fields with + | loc :: bytesS :: qualS :: _ => + match bytesS.toNat? with + | none => none + | some bytes => + let q := qualS.trim + let qual := + if q == "static" then some Qual.static + else if q == "dynamic" then some Qual.dynamic + else if q == "dynamic,bounded" then some Qual.dynamicBounded + else none + match qual with + | some qq => some { name := nameOfLoc loc, bytes := bytes, qual := qq } + | none => none + | _ => none + +/-- Parse a whole .su file (blank lines ignored). -/ +def parseSU (text : String) : Except String (List SuEntry) := + let lines := (text.splitOn "\n").filter (fun l => l.trim ≠ "") + let entries := lines.filterMap parseSuLine + if entries.length = lines.length then .ok entries + else .error "unparsed .su line(s)" + +/-- One .ci graph item. -/ +inductive CiItem where + | node (title : String) + | edge (src dst : String) + | indirectEdge (src : String) + deriving Repr + +def parseCiLine (line : String) : Option CiItem := + if line.trim.startsWith "node:" then + match extractAfter "title: \"" line with + | some t => some (CiItem.node t) + | none => none + else if line.trim.startsWith "edge:" then + match extractAfter "sourcename: \"" line, extractAfter "targetname: \"" line with + | some s, some "__indirect_call" => some (CiItem.indirectEdge s) + | some s, some t => some (CiItem.edge s t) + | _, _ => none + else none + +/-- Parse a whole .ci file. Titles are node identities; a node title of the +form `file.c:fn` is normalized to `fn` (GCC qualifies statics). -/ +def parseCI (text : String) : Except String (List CiItem) := + let lines := (text.splitOn "\n").filter (fun l => l.trim ≠ "") + let items := lines.filterMap parseCiLine + if items.length = 0 then .error "no graph items parsed from .ci" + else .ok items + +def normName (title : String) : String := nameOfLoc title + +/-! ## annotations.toml / cert.toml subset -------------------------------- + + [section] + key = 42 + key = ["a", "b"] +-/ + +def parseNatValue (v : String) : Option Nat := v.trim.toNat? + +def parseListValue (v : String) : Option (List String) := + let s := v.trim + if s.startsWith "[" && s.endsWith "]" then + let inner := (s.drop 1).dropRight 1 + some (((inner.splitOn ",").map String.trim).filter (fun x => x ≠ "")) + else none + +def parseToml (text : String) : + Except String (List (String × String × String)) := -- (section, key, value) + let lines := (text.splitOn "\n").map String.trim + let rec go (sec : String) (acc : List (String × String × String)) + (ls : List String) : Except String (List (String × String × String)) := + match ls with + | [] => .ok acc.reverse + | l :: rest => + if l = "" ∨ l.startsWith "#" then go sec acc rest + else if l.startsWith "[" && l.endsWith "]" then + let name := ((l.drop 1).dropRight 1).trim + go name acc rest + else + match l.splitOn "=" with + | k :: v :: _ => go sec ((sec, k.trim, (String.intercalate "=" v).trim) :: acc) rest + | _ => .error s!"bad toml line: {l}" + go "" [] lines + +def annOfToml (rows : List (String × String × String)) : Except String Ann := do + let mut sd : List (String × Nat) := [] + let mut ind : List (String × List String) := [] + let mut dyn : List (String × Nat) := [] + let mut isr : List (String × Nat) := [] + let mut thr : List (String × Nat) := [] + for (sec, k, v) in rows do + match sec with + | "recursion" => + match parseNatValue v with + | some n => sd := (k, n) :: sd + | none => return .error s!"recursion depth not a number: {k} = {v}" + | "indirect" => + match parseListValue v with + | some ls => ind := (k, ls) :: ind + | none => return .error s!"indirect targets not a list: {k} = {v}" + | "dynamic" => + match parseNatValue v with + | some n => dyn := (k, n) :: dyn + | none => return .error s!"dynamic bound not a number: {k} = {v}" + | "isr" => + match parseNatValue v with + | some n => isr := (k, n) :: isr + | none => return .error s!"isr level not a number: {k} = {v}" + | "threads" => + match parseNatValue v with + | some n => thr := (k, n) :: thr + | none => return .error s!"thread stack not a number: {k} = {v}" + | "" => return .error s!"top-level key outside a section: {k}" + | other => return .error s!"unknown section [{other}]" + return { selfDepth := sd.reverse, indirect := ind.reverse, + dynamic := dyn.reverse, isr := isr.reverse, threads := thr.reverse } + +def certOfToml (rows : List (String × String × String)) : + Except String (List (String × Nat)) := do + let mut c : List (String × Nat) := [] + for (sec, k, v) in rows do + if sec ≠ "cert" then return .error s!"cert file has unexpected section [{sec}]" + match parseNatValue v with + | some n => c := (k, n) :: c + | none => return .error s!"cert bound not a number: {k} = {v}" + return c.reverse + +end StackcertParsers diff --git a/src/stackcert/README.adoc b/src/stackcert/README.adoc new file mode 100644 index 0000000..0e95aca --- /dev/null +++ b/src/stackcert/README.adoc @@ -0,0 +1,128 @@ +// SPDX-License-Identifier: CC-BY-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) += stackcert — stack-depth certificate checker (ULTRAPLAN R1) +:toc: +:icons: font + +Status: *sources complete; UNVERIFIED in the authoring environment* (no +`lean`/`lake` on PATH there — toolchain downloads blocked; see +`docs/retraction-ledger.adoc` §Blocked). Every claim below is either +code-level ("the file says X") or an exact verification command. Nothing is +reported as proved until `bash tests/run_stackcert.sh` runs green and its +output is pasted into `docs/EXPLAINME.adoc`. + +== What it is + +A certificate checker for worst-case stack depth: + +* *Model* — `frame : Fn → ℕ`, `callees : Fn → Finset Fn` (lists-as-sets), + `cert : Fn → ℕ`. Rule per function `v`: + `cert v ≥ frame v + max_{u ∈ callees v} cert u`. +* *Self-recursion* — direct self-recursion is supported with an annotated + depth `d` (`[recursion]` in `annotations.toml`): the frame inflates to + `(d+1) * frame v` for path accounting. Any self-edge without an annotation + is rejected. All other cycles are rejected (CLI: `E_CYCLE`; semantically + the rule is unsatisfiable around a positive-frame cycle). +* *Rejects* — dynamic/dynamic-bounded frames without a `[dynamic]` bound, + unresolved indirect calls (edges to GCC's `__indirect_call` placeholder + must be listed in `[indirect]` and resolve), alloca/VLA/longjmp-family + calls, non-self cycles. +* *Verified core* — `StackcertCore.lean`: `check` and `cert_sound`, zero + imports, no holes, no Classical.choice. The theorem: if `check` accepts, + every call path's inflated-frame cost is ≤ the certificate of its start + function. Verify with `lean StackcertCore.lean`; the `#print axioms` + output is the receipt (expected clean — to be pasted into EXPLAINME after + the first verified run, not before). +* *Unverified I/O layer* — `Parsers.lean` + `Main.lean` (parse `.ci`/`.su`/ + TOML, CLI rejections). Explicitly outside the theorem. + +== Inputs + +[cols="1,2"] +|=== +| File | Format (real GCC output, committed fixtures) + +| `--ci` | VCG from `gcc -fcallgraph-info=su` (`node: { title: "f" label: ... }`, `edge: { sourcename: ... targetname: ... }`, indirect calls target `__indirect_call`) +| `--su` | `gcc -fstack-usage` (`file:line:col:func\tbytes\tqualifiers`) +| `--ann` | `annotations.toml` subset: `[recursion] fn = depth`, `[indirect] fn = ["t", ...]`, `[dynamic] fn = bytes`, `[isr]`, `[threads]` +| `--cert` | `cert.toml`: `[cert] fn = bytes` +|=== + +Fixtures in `fixtures/` are genuine GCC output for `probe.c`/`cycle.c` +(regenerate with `gcc -O0 -fcallgraph-info=su -fstack-usage -c .c`). + +== Verification commands (receipts that do not yet exist) + +[source,bash] +---- +# full harness: core + build + positive fixture + 4 negative controls +bash tests/run_stackcert.sh + +# or by hand: +cd src/stackcert +lean StackcertCore.lean # compiles; #print axioms cert_sound = [] +lake build +lake exe stackcert --ci fixtures/probe.ci --su fixtures/probe.su \ + --ann fixtures/annotations.toml --cert fixtures/cert.toml # exit 0 +lake exe stackcert --ci fixtures/probe.ci --su fixtures/probe.su \ + --ann fixtures/annotations.toml --cert fixtures/cert-decremented.toml # exit 1 +---- + +Negative controls (all must be rejected): decremented bound +(`cert-decremented.toml`), undeclared self-recursion +(`annotations-no-recursion.toml`), unresolved indirect call +(`annotations-no-indirect.toml`), undeclared cycle (`cycle.*`). + +== Fixture request — Zephyr ground truth (R1) + +The work environment has no `west`/QEMU/Zephyr SDK, so no real-target +measurement is claimed here. To unblock (ULTRAPLAN D3: Zephyr +`samples/synchronization` on `qemu_cortex_m3`): + +[source,bash] +---- +# 1. toolchain (one of): pipx install west; apt install qemu-system-arm +# plus the Zephyr SDK (arm-zephyr-eabi) and a west workspace +west init -m https://github.com/zephyrproject-rtos/zephyr --mr v3.7.0 ws +cd ws && west update && west zephyr-export + +# 2. build with callgraph + stack-usage info: +cd zephyr/samples/synchronization +west build -b qemu_cortex_m3 -- -DEXTRA_CONF_FILE=stackcert.conf \ + -DCONFIG_CALLGRAPH_INFO=y -DCONFIG_STACK_USAGE=y +# (flags: add -fcallgraph-info=su -fstack-usage via CFLAGS in stackcert.conf) + +# 3. run on QEMU and read painted-stack HWM via k_thread_stack_space_get() +# (the sample must paint stacks; measured HWM per thread is the ground truth) +west build -t run + +# 4. check: every thread's measured HWM <= certified thread budget +# (certified comes from stackcert on the build's .ci/.su dumps + +# [threads] entries in annotations.toml) +---- + +Ground-truth protocol (ULTRAPLAN §6), to be filled when the fixture runs: +record toolchain versions, flags, board/QEMU, workload duration, commit SHAs; +*measured ≤ certified on every run* (a violation stops the rung and writes a +ledger entry); report tightness `certified/measured` per thread; keep fixtures +reproducible with `just measure`. + +== R1 kill criterion (pre-registered) + +Fires if at the 3-week time box there is none of: a true positive (a real +program whose certificate is violated or whose budget can be safely reduced), +a justified budget reduction, or a consumer willing to adopt certificates. +Until the Zephyr fixture exists, the time box has not started; this is logged +in the ledger as *blocked*, not as success. + +== Layout + +---- +src/stackcert/ + StackcertCore.lean verified core (check + cert_sound) — zero imports + Parsers.lean .ci/.su/TOML parsing (UNVERIFIED layer) + Main.lean lake exe stackcert CLI (UNVERIFIED layer) + lakefile.toml lean-toolchain + fixtures/ real GCC outputs + certificates + negative controls +tests/run_stackcert.sh the harness (exit 2 = fixture request, never a skip) +---- diff --git a/src/stackcert/StackcertCore.lean b/src/stackcert/StackcertCore.lean new file mode 100644 index 0000000..0eb5ff3 --- /dev/null +++ b/src/stackcert/StackcertCore.lean @@ -0,0 +1,227 @@ +/- +SPDX-License-Identifier: MPL-2.0 +SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) + +StackcertCore — verified core of the stack-depth certificate checker +(ULTRAPLAN R1). Zero imports (no Mathlib), no admitted lemmas, no classical +axioms. Verify with: `lean StackcertCore.lean` and read the `#print axioms` +output at the bottom of this file. + +Model (mission statement, made precise): + + frame : Fn -> Nat -- stack bytes of the function's own frame + callees : Fn -> List Fn -- direct callees, treated as a set + cert : Fn -> Nat -- claimed bound per function + +Rule (per function v): + + cert v >= frame' v + max_{u in callees v, u != v} cert u + +where frame' v is the frame inflated by an annotated direct self-recursion +depth d (frame' v = (d+1) * frame v). A self-call edge without an annotation +is rejected (selfOk). Any other cycle makes the rule unsatisfiable for +finite certificates (summing inequalities around the cycle gives 0 > 0), so +"reject all other cycles" holds semantically; the CLI additionally reports +them explicitly. + +cert_sound: if `check` accepts, then for every call path starting at an +enrolled function, the sum of inflated frames along the path (its stack cost) +is <= the certificate of the start function. Real stack usage with self- +recursion bounded by the annotation is bounded by this inflated cost, since +each visit to v contributes at most (d+1) frames of size frame v. + +Nothing here is reported as verified until the toolchain command above has +run; see README.adoc for status. +-/ + +namespace StackcertCore + +/-! ## Boolean/list helpers (local, so the proof owns its plumbing) -/ + +def allb {α : Type} (p : α → Bool) : List α → Bool + | [] => true + | x :: xs => p x && allb p xs + +def memB [DecidableEq Fn] (x : Fn) (l : List Fn) : Bool := + l.any (fun y => decide (y = x)) + +theorem and_true : ∀ {a b : Bool}, a && b = true → a = true ∧ b = true := by + intro a b h + cases a with + | false => cases h + | true => + cases b with + | false => cases h + | true => exact ⟨rfl, rfl⟩ + +theorem allb_mem {α : Type} (p : α → Bool) : + ∀ (l : List α) (x : α), allb p l = true → x ∈ l → p x = true := by + intro l + induction l with + | nil => intro x hx hm; cases hm + | cons y ys ih => + intro x hx hm + have hp : p y = true ∧ allb p ys = true := and_true hx + cases hm with + | head _ => exact hp.1 + | tail _ _ hm' => exact ih x hp.2 hm' + +theorem memB_sound [DecidableEq Fn] : + ∀ (l : List Fn) (x : Fn), memB x l = true → x ∈ l := by + intro l + induction l with + | nil => intro x hx; simp [memB] at hx + | cons y ys ih => + intro x hx + have hy : (decide (y = x) || memB x ys) = true := by + simpa [memB] using hx + cases hyx : decide (y = x) with + | true => + have heq : y = x := of_decide_eq_true hyx + rw [← heq] + exact List.Mem.head ys + | false => + have hrest : memB x ys = true := by + simp [hyx] at hy + exact hy + exact List.Mem.tail y ys (ih x hrest) + +/-! ## Model -/ + +/-- Call graph over function names. `callees` is a Finset in the mission +statement; lists-as-sets suffice here (duplicates are harmless). -/ +structure CallGraph (Fn : Type) where + fns : List Fn + frame : Fn → Nat + callees : Fn → List Fn + +/-- Annotations. `selfDepth v = some d` declares direct self-recursion of +depth d at v. The rest of the annotation file (indirect targets, ISR levels, +threads) is CLI-level input and does not enter the theorem. -/ +structure Annot (Fn : Type) where + selfDepth : Fn → Option Nat + +variable {Fn : Type} [DecidableEq Fn] + +/-- Self-edges are legal only under an explicit depth annotation. -/ +def selfOk (g : CallGraph Fn) (a : Annot Fn) (v : Fn) : Bool := + if (g.callees v).any (fun u => decide (u = v)) then (a.selfDepth v).isSome + else true + +/-- Frame inflated by annotated self-recursion depth. -/ +def iframe (g : CallGraph Fn) (a : Annot Fn) (v : Fn) : Nat := + match a.selfDepth v with + | some d => (d + 1) * g.frame v + | none => g.frame v + +/-- max of `cert u` over callees of `v` other than `v` itself (0 if none). -/ +def maxExcept (cert : Fn → Nat) (v : Fn) : List Fn → Nat + | [] => 0 + | u :: us => if u = v then maxExcept cert v us + else max (cert u) (maxExcept cert v us) + +theorem cert_le_maxExcept (cert : Fn → Nat) (v : Fn) : + ∀ (l : List Fn) (u : Fn), u ≠ v → u ∈ l → cert u ≤ maxExcept cert v l := by + intro l + induction l with + | nil => intro u hne hm; cases hm + | cons y ys ih => + intro u hne hm + cases hm with + | head _ => + -- u is y, and y ≠ v, so the fold head is max (cert y) (...) + show cert y ≤ (if y = v then maxExcept cert v ys + else max (cert y) (maxExcept cert v ys)) + if hyv : y = v then + rw [if_pos hyv] + exact absurd hyv hne + else + rw [if_neg hyv] + exact Nat.le_max_left _ _ + | tail _ _ hm' => + show cert u ≤ (if y = v then maxExcept cert v ys + else max (cert y) (maxExcept cert v ys)) + if hyv : y = v then + rw [if_pos hyv] + exact ih u hne hm' + else + rw [if_neg hyv] + exact Nat.le_trans (ih u hne hm') (Nat.le_max_right _ _) + +/-- The certificate rule at v: inflated frame plus the worst certificate of a +non-self callee is covered by cert v. (Mission rule exactly when there is no +self-recursion and no annotation: iframe = frame, and max over all callees.) -/ +def rule (g : CallGraph Fn) (a : Annot Fn) (cert : Fn → Nat) (v : Fn) : Bool := + decide (iframe g a v + maxExcept cert v (g.callees v) ≤ cert v) + +/-- Every callee of an enrolled function is itself enrolled (resolution). -/ +def closed (g : CallGraph Fn) (v : Fn) : Bool := + allb (fun u => memB u g.fns) (g.callees v) + +/-- The checker. Accepts exactly when every enrolled function is +self-recursion-annotated where needed, satisfies the rule, and has resolved +callees. -/ +def check (g : CallGraph Fn) (a : Annot Fn) (cert : Fn → Nat) : Bool := + allb (selfOk g a) g.fns + && allb (rule g a cert) g.fns + && allb (closed g) g.fns + +/-! ## Paths and stack cost -/ + +/-- A call path is a nonempty chain of direct calls starting at `v`, never +traversing a self-edge (self-recursion is folded into `iframe`). -/ +inductive Path (g : CallGraph Fn) : Fn → Type where + | leaf (v : Fn) : Path g v + | step (v u : Fn) (hne : u ≠ v) (hu : u ∈ g.callees v) + (p : Path g u) : Path g v + +/-- Stack cost of a path: sum of inflated frames along the way. -/ +def cost (g : CallGraph Fn) (a : Annot Fn) : {v : Fn} → Path g v → Nat + | v, Path.leaf _ => iframe g a v + | v, Path.step _ u _ _ p => iframe g a v + cost g a p + +/-! ## Soundness -/ + +theorem cert_sound (g : CallGraph Fn) (a : Annot Fn) (cert : Fn → Nat) + (h : check g a cert = true) : + ∀ (v : Fn), v ∈ g.fns → ∀ (p : Path g v), cost g a v p ≤ cert v := by + have hsplit : + allb (selfOk g a) g.fns = true + ∧ allb (rule g a cert) g.fns = true + ∧ allb (closed g) g.fns = true := by + have h1 := and_true h + have h2 := and_true h1.1 + exact ⟨h2.1, h2.2, h1.2⟩ + have hrule : ∀ w ∈ g.fns, rule g a cert w = true := + fun w hw => allb_mem (rule g a cert) g.fns w hsplit.2.1 hw + have hcl : ∀ w ∈ g.fns, closed g w = true := + fun w hw => allb_mem (closed g) g.fns w hsplit.2.2 hw + intro v hv p + revert hv + induction p with + | leaf w => + intro hw + have hr : rule g a cert w = true := hrule w hw + have hle : iframe g a w + maxExcept cert w (g.callees w) ≤ cert w := + of_decide_eq_true hr + exact Nat.le_trans (Nat.le_add_right _ _) hle + | step w u hne hu p ih => + intro hw + have hr : rule g a cert w = true := hrule w hw + have hle : iframe g a w + maxExcept cert w (g.callees w) ≤ cert w := + of_decide_eq_true hr + have hall : allb (fun x => memB x g.fns) (g.callees w) = true := by + exact hcl w hw + have hmem : memB u g.fns = true := allb_mem _ (g.callees w) u hall hu + have hufn : u ∈ g.fns := memB_sound g.fns u hmem + have hcu : cert u ≤ maxExcept cert w (g.callees w) := + cert_le_maxExcept cert w (g.callees w) u hne hu + have hbody : cost g a p ≤ cert u := ih hufn + have hsum : iframe g a w + cost g a p + ≤ iframe g a w + maxExcept cert w (g.callees w) := + Nat.add_le_add (Nat.le_refl (iframe g a w)) (Nat.le_trans hbody hcu) + exact Nat.le_trans hsum hle + +end StackcertCore + +#print axioms StackcertCore.cert_sound diff --git a/src/stackcert/fixtures/annotations-no-indirect.toml b/src/stackcert/fixtures/annotations-no-indirect.toml new file mode 100644 index 0000000..64fdbd0 --- /dev/null +++ b/src/stackcert/fixtures/annotations-no-indirect.toml @@ -0,0 +1,6 @@ +# SPDX-License-Identifier: MPL-2.0 +# Negative control: indirect call in indirect() left unresolved. +# Expected: rejected (E_INDIRECT). + +[recursion] +recur = 1 diff --git a/src/stackcert/fixtures/annotations-no-recursion.toml b/src/stackcert/fixtures/annotations-no-recursion.toml new file mode 100644 index 0000000..e5e1b85 --- /dev/null +++ b/src/stackcert/fixtures/annotations-no-recursion.toml @@ -0,0 +1,6 @@ +# SPDX-License-Identifier: MPL-2.0 +# Negative control: self-recursion on recur() left undeclared. +# Expected: rejected (selfOk — a self-edge needs a [recursion] depth). + +[indirect] +indirect = ["top"] diff --git a/src/stackcert/fixtures/annotations.toml b/src/stackcert/fixtures/annotations.toml new file mode 100644 index 0000000..980bc7c --- /dev/null +++ b/src/stackcert/fixtures/annotations.toml @@ -0,0 +1,12 @@ +# SPDX-License-Identifier: MPL-2.0 +# annotations.toml — stackcert annotations for fixtures/probe.* +# [recursion] fn = annotated direct self-recursion depth +# [indirect] fn = ["possible targets", ...] (must resolve) +# [dynamic] fn = explicit byte bound for dynamic/bounded frames +# [isr] fn = ISR level [threads] fn = thread stack bytes + +[recursion] +recur = 1 + +[indirect] +indirect = ["top"] diff --git a/src/stackcert/fixtures/cert-decremented.toml b/src/stackcert/fixtures/cert-decremented.toml new file mode 100644 index 0000000..a2e8787 --- /dev/null +++ b/src/stackcert/fixtures/cert-decremented.toml @@ -0,0 +1,11 @@ +# SPDX-License-Identifier: MPL-2.0 +# Negative control: bound decremented by one (main = 111 < required 112). +# Expected: rejected. + +[cert] +helper = 16 +mid = 64 +top = 96 +main = 111 +recur = 64 +indirect = 112 diff --git a/src/stackcert/fixtures/cert.toml b/src/stackcert/fixtures/cert.toml new file mode 100644 index 0000000..1574795 --- /dev/null +++ b/src/stackcert/fixtures/cert.toml @@ -0,0 +1,15 @@ +# SPDX-License-Identifier: MPL-2.0 +# cert.toml — certificate for fixtures/probe.* (bytes) +# Derived from probe.su frames + probe.ci edges, rule +# cert v >= frame v + max_{u != v} cert u (recur: iframe = 2 * frame): +# helper 16; mid 48+16=64; top 32+64=96; main 16+96=112; +# recur (d=1) 2*32=64; indirect 16+96=112. +# Hand-computed; the checker re-derives independently. + +[cert] +helper = 16 +mid = 64 +top = 96 +main = 112 +recur = 64 +indirect = 112 diff --git a/src/stackcert/fixtures/cycle-annotations.toml b/src/stackcert/fixtures/cycle-annotations.toml new file mode 100644 index 0000000..1ba9da5 --- /dev/null +++ b/src/stackcert/fixtures/cycle-annotations.toml @@ -0,0 +1,6 @@ +# SPDX-License-Identifier: MPL-2.0 +# annotations/cert for the cycle.* negative-control fixture (no [recursion]): +# ping -> pong -> ping is a non-self cycle and must be rejected regardless of +# any certificate (E_CYCLE). + +[recursion] diff --git a/src/stackcert/fixtures/cycle-cert.toml b/src/stackcert/fixtures/cycle-cert.toml new file mode 100644 index 0000000..a66cd05 --- /dev/null +++ b/src/stackcert/fixtures/cycle-cert.toml @@ -0,0 +1,7 @@ +# SPDX-License-Identifier: MPL-2.0 +# A perfectly "good-looking" certificate for the cyclic fixture. Correctly +# rejected anyway: non-self cycles are not certificate-carrying. + +[cert] +ping = 128 +pong = 128 diff --git a/src/stackcert/fixtures/cycle.c b/src/stackcert/fixtures/cycle.c new file mode 100644 index 0000000..152ce48 --- /dev/null +++ b/src/stackcert/fixtures/cycle.c @@ -0,0 +1,5 @@ +/* SPDX-License-Identifier: MPL-2.0 */ +/* negative-control fixture: non-self cycle ping -> pong -> ping */ +void pong(int); +void ping(int x) { pong(x); } +void pong(int x) { ping(x); } diff --git a/src/stackcert/fixtures/cycle.ci b/src/stackcert/fixtures/cycle.ci new file mode 100644 index 0000000..9a68333 --- /dev/null +++ b/src/stackcert/fixtures/cycle.ci @@ -0,0 +1,6 @@ +graph: { title: "cycle.c" +node: { title: "ping" label: "ping\ncycle.c:4:6\n32 bytes (static)" } +edge: { sourcename: "ping" targetname: "pong" label: "cycle.c:4:20" } +node: { title: "pong" label: "pong\ncycle.c:5:6\n32 bytes (static)" } +edge: { sourcename: "pong" targetname: "ping" label: "cycle.c:5:20" } +} diff --git a/src/stackcert/fixtures/cycle.su b/src/stackcert/fixtures/cycle.su new file mode 100644 index 0000000..fb75d32 --- /dev/null +++ b/src/stackcert/fixtures/cycle.su @@ -0,0 +1,2 @@ +cycle.c:4:6:ping 32 static +cycle.c:5:6:pong 32 static diff --git a/src/stackcert/fixtures/probe.c b/src/stackcert/fixtures/probe.c new file mode 100644 index 0000000..17b6c17 --- /dev/null +++ b/src/stackcert/fixtures/probe.c @@ -0,0 +1,11 @@ +/* SPDX-License-Identifier: MPL-2.0 */ +/* stackcert fixture: generated with + gcc -O0 -fcallgraph-info=su -fstack-usage -c probe.c + Frames/callgraph below are real compiler output, committed as fixtures. */ +static int helper(int x) { char pad[24]; pad[0]=(char)x; return pad[0]+1; } +int mid(int x) { return helper(x) + helper(x+1); } +int top(int x) { return mid(x); } +int main(void) { return top(0); } +void recur(int d) { if (d) recur(d-1); } +void (*fp)(int); +void indirect(void) { if (fp) fp(1); } diff --git a/src/stackcert/fixtures/probe.ci b/src/stackcert/fixtures/probe.ci new file mode 100644 index 0000000..e0fe289 --- /dev/null +++ b/src/stackcert/fixtures/probe.ci @@ -0,0 +1,15 @@ +graph: { title: "probe.c" +node: { title: "probe.c:helper" label: "helper\nprobe.c:5:12\n16 bytes (static)" } +node: { title: "mid" label: "mid\nprobe.c:6:5\n48 bytes (static)" } +edge: { sourcename: "mid" targetname: "probe.c:helper" label: "probe.c:6:25" } +edge: { sourcename: "mid" targetname: "probe.c:helper" label: "probe.c:6:37" } +node: { title: "top" label: "top\nprobe.c:7:5\n32 bytes (static)" } +edge: { sourcename: "top" targetname: "mid" label: "probe.c:7:25" } +node: { title: "main" label: "main\nprobe.c:8:5\n16 bytes (static)" } +edge: { sourcename: "main" targetname: "top" label: "probe.c:8:25" } +node: { title: "recur" label: "recur\nprobe.c:9:6\n32 bytes (static)" } +edge: { sourcename: "recur" targetname: "recur" label: "probe.c:9:28" } +node: { title: "indirect" label: "indirect\nprobe.c:11:6\n16 bytes (static)" } +node: { title: "__indirect_call" label: "Indirect Call Placeholder" shape : ellipse } +edge: { sourcename: "indirect" targetname: "__indirect_call" label: "probe.c:11:31" } +} diff --git a/src/stackcert/fixtures/probe.su b/src/stackcert/fixtures/probe.su new file mode 100644 index 0000000..ce65ae0 --- /dev/null +++ b/src/stackcert/fixtures/probe.su @@ -0,0 +1,6 @@ +probe.c:5:12:helper 16 static +probe.c:6:5:mid 48 static +probe.c:7:5:top 32 static +probe.c:8:5:main 16 static +probe.c:9:6:recur 32 static +probe.c:11:6:indirect 16 static diff --git a/tests/run_stackcert.sh b/tests/run_stackcert.sh new file mode 100755 index 0000000..b7f3699 --- /dev/null +++ b/tests/run_stackcert.sh @@ -0,0 +1,73 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# run_stackcert.sh — stackcert verification harness. +# +# Stages (each must pass; nothing silently skips): +# 1. core: lean StackcertCore.lean — compiles, #print axioms clean +# (no Classical.choice, no sorryAx) +# 2. build: lake build +# 3. positive fixture: probe.* + annotations.toml + cert.toml -> exit 0 +# 4. negative controls (each must be rejected, exit 1): +# cert-decremented.toml decremented bound +# annotations-no-recursion undeclared self-recursion +# annotations-no-indirect unresolved indirect call +# cycle.* undeclared (non-self) cycle +# +# Exit: 0 all green; 1 failure; 2 toolchain absent (fixture request, never a +# silent skip). + +set -euo pipefail +cd "$(dirname "${BASH_SOURCE[0]}")/../src/stackcert" + +if ! command -v lean >/dev/null 2>&1 || ! command -v lake >/dev/null 2>&1; then + cat >&2 <<'EOF' +FAIL (fixture request): lean/lake not on PATH — stackcert is UNVERIFIED here. +Unblock with: + curl -sSfL https://elan.lean-lang.org/elan-init.sh | sh -s -- -y + elan default leanprover/lean4:v4.15.0 +then re-run: bash tests/run_stackcert.sh +EOF + exit 2 +fi + +echo "=== 1. core compile + axiom footprint ===" +lean_out="$(lean StackcertCore.lean 2>&1)" || { echo "FAIL: core does not compile"; echo "$lean_out"; exit 1; } +echo "$lean_out" | grep -q "cert_sound" || { echo "FAIL: no #print axioms output for cert_sound"; echo "$lean_out"; exit 1; } +if echo "$lean_out" | grep -E "Classical\.choice|sorryAx|propext" ; then + echo "FAIL: axiom footprint not clean (must be [] for cert_sound)"; exit 1 +fi +echo "PASS (axiom footprint clean)" +echo "$lean_out" | tail -3 + +echo "=== 2. lake build ===" +lake build >/dev/null || { echo "FAIL: lake build"; exit 1; } +echo "PASS" + +echo "=== 3. positive fixture (must be accepted) ===" +run() { lake exe stackcert --ci "$1" --su "$2" --ann "$3" --cert "$4"; } +if out="$(run fixtures/probe.ci fixtures/probe.su fixtures/annotations.toml fixtures/cert.toml)"; then + echo "PASS: $out" +else + echo "FAIL: positive fixture rejected: $out"; exit 1 +fi + +echo "=== 4. negative controls (must be rejected) ===" +fail=0 +neg() { # name, then the 4 paths; expects exit 1 + local name="$1"; shift + printf ' %-28s ' "$name" + if out="$(run "$@" 2>&1)"; then + echo "FAIL (accepted!)"; fail=1 + else + echo "PASS (rejected: $(echo "$out" | head -1))" + fi +} +neg "cert-decremented" fixtures/probe.ci fixtures/probe.su fixtures/annotations.toml fixtures/cert-decremented.toml +neg "undeclared-recursion" fixtures/probe.ci fixtures/probe.su fixtures/annotations-no-recursion.toml fixtures/cert.toml +neg "unresolved-indirect" fixtures/probe.ci fixtures/probe.su fixtures/annotations-no-indirect.toml fixtures/cert.toml +neg "undeclared-cycle" fixtures/cycle.ci fixtures/cycle.su fixtures/cycle-annotations.toml fixtures/cycle-cert.toml + +[ "$fail" -eq 0 ] || { echo "run_stackcert: FAIL" >&2; exit 1; } +echo "run_stackcert: OK — core verified, fixture accepted, all controls rejected"