From dafa491fef3163e93294e3621416e26da2cdf481 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 27 Sep 2026 16:58:06 +0000 Subject: [PATCH] docs: type-family map cross-links (nextgen-typing TYPE-CONNECTIONS) Coherence without code coupling: README gains the family-map section (question this repo asks + boundaries), glossary defers to the estate shared glossary for cross-family reading, ULTRAPLAN decision log records the registration and the naming errata (tropical-resource-typing = tropical-types; katagoria -> ideas-to-alphas is NOT kategoria). Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- .machine_readable/root-allow.txt | 1 + Justfile | 25 +- README.adoc | 50 ++- ULTRAPLAN.md | 211 ++++++++++++ docs/EXPLAINME.adoc | 82 +++++ docs/OPERATIONAL-MODEL.md | 164 +++++++++ docs/glossary.adoc | 107 ++++++ docs/reports/session-2026-09-27.adoc | 117 +++++++ docs/retraction-ledger.adoc | 65 ++++ examples/session_ir/accept_annotated.sir | 14 + examples/session_ir/accept_buf_delegation.sir | 15 + .../session_ir/accept_choice_expensive.sir | 27 ++ examples/session_ir/accept_choice_max.sir | 33 ++ examples/session_ir/accept_pair_drop.sir | 10 + examples/session_ir/accept_send_recv.sir | 14 + examples/session_ir/accept_seq_add.sir | 13 + examples/session_ir/manifest.json | 19 + examples/session_ir/reject_alias.sir | 8 + .../session_ir/reject_close_before_end.sir | 8 + examples/session_ir/reject_double_free.sir | 8 + examples/session_ir/reject_double_send.sir | 9 + examples/session_ir/reject_drop_then_send.sir | 10 + examples/session_ir/reject_leak.sir | 8 + .../session_ir/reject_protocol_mismatch.sir | 8 + scripts/check-no-md-in-docs.sh | 5 +- scripts/check.sh | 108 ++++++ src/occ/Demo.idr | 51 +++ src/occ/Occ.idr | 107 ++++++ src/occ/README.adoc | 115 ++++++ src/occ/RejectDoubleFree.idr | 21 ++ src/occ/RejectLeak.idr | 22 ++ src/occ/RejectOverCapacity.idr | 22 ++ src/occ/RejectUseAfterFree.idr | 22 ++ src/occ/check-rejections.sh | 52 +++ src/session_ir/__init__.py | 10 + src/session_ir/__main__.py | 7 + .../__pycache__/__init__.cpython-311.pyc | Bin 0 -> 587 bytes .../__pycache__/__main__.cpython-311.pyc | Bin 0 -> 315 bytes .../__pycache__/checker.cpython-311.pyc | Bin 0 -> 21083 bytes .../__pycache__/cli.cpython-311.pyc | Bin 0 -> 9327 bytes .../__pycache__/machine.cpython-311.pyc | Bin 0 -> 15530 bytes .../__pycache__/parser.cpython-311.pyc | Bin 0 -> 21476 bytes .../__pycache__/syntax.cpython-311.pyc | Bin 0 -> 16164 bytes src/session_ir/checker.py | 323 +++++++++++++++++ src/session_ir/cli.py | 145 ++++++++ src/session_ir/machine.py | 243 +++++++++++++ src/session_ir/parser.py | 326 ++++++++++++++++++ src/session_ir/syntax.py | 309 +++++++++++++++++ src/stackcert/Main.lean | 178 ++++++++++ src/stackcert/Parsers.lean | 180 ++++++++++ src/stackcert/README.adoc | 128 +++++++ src/stackcert/StackcertCore.lean | 227 ++++++++++++ .../fixtures/annotations-no-indirect.toml | 6 + .../fixtures/annotations-no-recursion.toml | 6 + src/stackcert/fixtures/annotations.toml | 12 + src/stackcert/fixtures/cert-decremented.toml | 11 + src/stackcert/fixtures/cert.toml | 15 + src/stackcert/fixtures/cycle-annotations.toml | 6 + src/stackcert/fixtures/cycle-cert.toml | 7 + src/stackcert/fixtures/cycle.c | 5 + src/stackcert/fixtures/cycle.ci | 6 + src/stackcert/fixtures/cycle.su | 2 + src/stackcert/fixtures/probe.c | 11 + src/stackcert/fixtures/probe.ci | 15 + src/stackcert/fixtures/probe.su | 6 + tests/run_stackcert.sh | 73 ++++ 66 files changed, 3791 insertions(+), 17 deletions(-) create mode 100644 ULTRAPLAN.md create mode 100644 docs/OPERATIONAL-MODEL.md create mode 100644 docs/glossary.adoc create mode 100644 docs/reports/session-2026-09-27.adoc create mode 100644 docs/retraction-ledger.adoc create mode 100644 examples/session_ir/accept_annotated.sir create mode 100644 examples/session_ir/accept_buf_delegation.sir create mode 100644 examples/session_ir/accept_choice_expensive.sir create mode 100644 examples/session_ir/accept_choice_max.sir create mode 100644 examples/session_ir/accept_pair_drop.sir create mode 100644 examples/session_ir/accept_send_recv.sir create mode 100644 examples/session_ir/accept_seq_add.sir create mode 100644 examples/session_ir/manifest.json create mode 100644 examples/session_ir/reject_alias.sir create mode 100644 examples/session_ir/reject_close_before_end.sir create mode 100644 examples/session_ir/reject_double_free.sir create mode 100644 examples/session_ir/reject_double_send.sir create mode 100644 examples/session_ir/reject_drop_then_send.sir create mode 100644 examples/session_ir/reject_leak.sir create mode 100644 examples/session_ir/reject_protocol_mismatch.sir create mode 100755 scripts/check.sh create mode 100644 src/occ/Demo.idr create mode 100644 src/occ/Occ.idr create mode 100644 src/occ/README.adoc create mode 100644 src/occ/RejectDoubleFree.idr create mode 100644 src/occ/RejectLeak.idr create mode 100644 src/occ/RejectOverCapacity.idr create mode 100644 src/occ/RejectUseAfterFree.idr create mode 100755 src/occ/check-rejections.sh create mode 100644 src/session_ir/__init__.py create mode 100644 src/session_ir/__main__.py create mode 100644 src/session_ir/__pycache__/__init__.cpython-311.pyc create mode 100644 src/session_ir/__pycache__/__main__.cpython-311.pyc create mode 100644 src/session_ir/__pycache__/checker.cpython-311.pyc create mode 100644 src/session_ir/__pycache__/cli.cpython-311.pyc create mode 100644 src/session_ir/__pycache__/machine.cpython-311.pyc create mode 100644 src/session_ir/__pycache__/parser.cpython-311.pyc create mode 100644 src/session_ir/__pycache__/syntax.cpython-311.pyc create mode 100644 src/session_ir/checker.py create mode 100644 src/session_ir/cli.py create mode 100644 src/session_ir/machine.py create mode 100644 src/session_ir/parser.py create mode 100644 src/session_ir/syntax.py create mode 100644 src/stackcert/Main.lean create mode 100644 src/stackcert/Parsers.lean create mode 100644 src/stackcert/README.adoc create mode 100644 src/stackcert/StackcertCore.lean create mode 100644 src/stackcert/fixtures/annotations-no-indirect.toml create mode 100644 src/stackcert/fixtures/annotations-no-recursion.toml create mode 100644 src/stackcert/fixtures/annotations.toml create mode 100644 src/stackcert/fixtures/cert-decremented.toml create mode 100644 src/stackcert/fixtures/cert.toml create mode 100644 src/stackcert/fixtures/cycle-annotations.toml create mode 100644 src/stackcert/fixtures/cycle-cert.toml create mode 100644 src/stackcert/fixtures/cycle.c create mode 100644 src/stackcert/fixtures/cycle.ci create mode 100644 src/stackcert/fixtures/cycle.su create mode 100644 src/stackcert/fixtures/probe.c create mode 100644 src/stackcert/fixtures/probe.ci create mode 100644 src/stackcert/fixtures/probe.su create mode 100755 tests/run_stackcert.sh 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 0000000000000000000000000000000000000000..d69997329c9bd9b767284e8f52b58f38c2b97aa6 GIT binary patch literal 587 zcmZ`#J!{-R5S=}pK795;aOZAG72yxrMVb%-HW+f|d^zr%M$ICm#V1=UZFVKFT)E3n zaPP+WC*)tKJhnP;mCoSKRd!_?at6;n9&eVJH^bca`#sR{d+_J%8Ufs!KbwkxrRJVBY#b~gd{~wh;mv026(aI=g#Y&6T5!&dV?7QJcH;>tBoe9%+>0gEo8@c;k- literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..af1057073fcbda113047b0d92e3ccc6f87ab1c64 GIT binary patch literal 315 zcmZ3^%ge<81nr(Xvt|S7#~=<2us|7~y?~7A3@HpLj5!QZ3@J=0%sGs?Oi@gX3``8E z3|Y)D4L}~#G9YI)On_k-BajEg5WomDA(%mv z=H#5rB9O(mSW+u8OI9*`2C4mJs-Kaco2p-0oLZ!xpPXD;keHWTsasN6kXo!?T$HR| zoLXF*nV%P*S)?By4>B)4Uaz3?7l%!5eoARhs$CH`&=in;#STE?12ZEd;|DedM(zeK o5PZNOdI1$ZVBlzAZsF(<=@97@>k+%iAaI32-~tR4aRLni0Oearga7~l literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..324d31b27b628bb3078925472c888ef4bf97cb31 GIT binary patch literal 21083 zcmeHveQX=owdV{!L`u{bMM>0`rIBRIqGU;yZCU=3W672hJGSgta?`NQsx)V8(-9?k zhO}drDxAJxpImr%={yBiTNz~^oId$Q#&ZD|aDnt8e-w*i(Lcz5ix2|{2=*bsKI|?a zBh8`+b{G3QcgP`!mSpEGip2suq7Lue?|aU<=bn4+x%|7bvJwu@U!VN#)&I7i6yQy|+Ht;B5#tdK-gH-lpI-@3vsGw>jA2Z3zlqA=v6|4YqmPg6-b+;CAo!;12JO zV28IOxYN5c*y-&Idc2-sm$xg}?d=Zk^6m=uczc4q-riuJw=cNcyF1wL?GNtp?g{So z?&UejBJGp9FPZAIW9PgBChk>EEP9_4ZND;c+{gIW9`AmZVn<4GLCT<5A(p*w@g5M% zCpb@~?|+#&ZsO)l$oFoK7?34@ND>AA70LgOBny{jWg&D$5+)=?3Czw2C(j=eu7<_S zL1`u=yy^=EeL}QHkc30Run-mG-jWho2q>(Ge>NBl&jkFw5DNAvA!$zV&xTPfFvHS= zXm4&htO$w}49J0*%R=Y)E&;K-gzjC!ZqK0-MYk*G_(V}TEcm8F zl01XTuS>#3**Ak8qg~%S5>?SF2$Sgb?9B8{;j-)#r4lrHeK(@dNWoe8CiPL8!QlKD z>&2VGbYMpE$pX4dEn=)f=gcfR=AWGrwF*3k1nIhjk|W_uB|gMTGveHA0K=K_1tq~Z zH-`#P>AOCE2#wCp_@(SXQAtR8HzWX+XcliuI4Frg)%ox=`rLWp^yK;BbEk*Lg>zSY ziX`;!qLOEP@17&<%*=)u1`i9fb5p>GFhuA<7-&Ekg9WBa1nPUJ&o@0i>+hS9ZU~0w zIYRA50a2cv>+?^~qQ&Q)-9on@cPinFp8TZFydq$Vpdw9Q#{m4ZN(l5qm2^fZ^*+=LKFrU{N>h(O^`Jtz{e-Jc9?A{OOa(9s zjX8vXr=(;wOS8}wS@MbCxkJx48lDq6x>0Wr+DlTjG# z^#khF4~Wh_L6nq`9QKE10@H@-*L$2{cm=#A^_KiI z$qWy#I(#!(c2hhS)p8=>52=>Z0VSl`&(6{0^G&PP$?)8?^v{sCoTpp04in3%7EFst z)p8u8SFOj1sZbgWrrJiQhEJayo}j?U*$d+*)Uwg3Rakj}D(#9huk3x6X~K z6?i#)7K!6$C#OcW%qPxX7&$#UHFkbH$E6#pg~eG3Vz}qQtE!dYq-viyd45!uXJyqg0qUw&f|F{|1Y>1-RTLDN z1pBI{$(yR>!uZKa)ph~X_H-bmS}8E8n!n?d)#89Mr4dNA&dp7QkeS#_wT5m^N!R?E zfY)F~-t%A8;{6^cab6xPph>ieR!DfWSOf`gR~^SmoS$brp_)QBsI`Phb)rP=5F3Lx_DLpZ2!W+?^Jt8;3J>E^Z61Rz!c(;koVimsaVvAUf?_yC9>+oG7)`RY?s*NE` zk|U$%AXw()Sx`KfUE3i%UYDdfl2nMkF5UFWkQ0}(a!O zBLJ7@=~cf%%Ex-D+z=ub&O9MYHpD@@jGBIK5>5BbQOmE8=VLwJk1=bm>TmJ9GP%-G zlgJr$GoA}M^3r)@Kjy7bbJQ9&5gSIWps;y7Vxz?aidv*mP_FpI*&9U9X;O+ZBA(dT zQzR1-=j>)jCD(M#^+r z(JOJb@(uu|qN6lsUO2FD;C^wuJ??wZk*xEi>O2bv)~Xur4<@#culN8mpK}w*s>xK< zWTJF3Z7;o3{<*#3Gke2Q|B{%rx2Npw348lmc~xxh?ZBPDf;sK1S}-pR-!4j5R4tS+ zHu$ETtx4aTytzvNFTCx~M>jD72*H2#?-9_6KWHTQyv4{2g^15*0Fc_q9%V$7Az}vZ zYDOS~KpL4WQR^ks1g1k=X9jdbf53`n(X?tdG7s3GSkHp3im|;P^B!wt2n$8PcX1l4 zJtV0tOHeouW#_JvPkd;Y!CBJNW^c?$vT`Lb=jl}~5W?cvLteF$PB#ZlNOgo~pcMJ9 zP^BKLd=4GZxQ6jc`P3y}V0tR6y{hHI3dA_61Z>fJo`K$=^29~*d4T5_$TEc|tE!DDcRh=qh2v`#bxY3M(K}HH+OqC+wR?$=jitAD z#Vm{EOV^T>t!Y8uK-^X2)1J64BeF5{9W9)Ng{aQV z1GeFRZn|%Znv6^U31XIos6{lr!<`}U2>8~R+D*XLqZrevcs9>;j3EIe}&yG3mk5>y*wQ%Qup3tzfK@~&FA z;e)K3CPn@x+sw=%xrxPQG7A?aZ1G5yhdvGlQ;XPkM~oEf>UX4v70}`f^9!9Q)Z@E^ zEk_T_;fa*yNmU^-ptql$7lIE;_>6$P;B)}J%*{=q(>ERPDVS&;k1Zp9FH0d!B-a5i zvWoz1?U{te3}h0S31c>w7LV zSzULcuA6cXr5lgN-$*nb)jpq^pP6~rDE}vp;5x^bjq+bOoUyk)b2KL$%_#978@tnu zV^m~J`}~0wIm3#aVMWfcBH#VYu`S`)rWIK?@lCtq*HB^8?i@(>?|Wu7x%U5w10XT5 z|LY>I!u{b5WUt#D_aSE;WzPUDdj(~$pzOu_wPnMpEgMWV-(cmSDaKZg|B8UVa-7<7 z<*uGUSN>rbO`hGQV(*`8fwA!xAl6Cm^7k<8w`k2b=d-fzs< zxJJ5Y_KCucD-vd-Pv1-Hvk=o$hOGz2Cvi-E6Wx;E0`S<>k^p85HmO+LWDmvfAmAp@ zPk{Jd{vJSfy5tlXef=qzE2@oFo+)WAQlZZmErRM%J_Ois{c&wu@_kg3bnQ&JcCK^g zvZ1xw=KGO!TRYfH7-Znlj>r7N&ehIb3=5?X90s$xhroUAA#k5_XuXK5uK5=&Q5VrY zgKA4!1>;fLpxooO)?ze01xh4$RbRMr>ZGQko3xdm7X9ZJb!uK_nB8zucVzVgLa$3l zZ$>yG@-oURM8jKLzD8GC5#txe(oJoo+{dmZ?e#g`PUR)J3njjB<#askSToa=hM#?C zbz!LZ?~tMes4#6lE#VVwBiqAgmnGLNyX z7%$&5Frn$HE^4-*!9Sr_dcGXavE#8~ug1%5piv&ivTf5o$WT(JkjSqV=t4Zv)0(rL z&zlYXG>4jVwHn7Hw}e`AX`!}U7@Ctct9fn49Y5v^+Mz9S<}tRT^u3@RYl!Af=D}is zNu1lIVu>iaPuS3LVB}KTk;X~Mc)bX)i4>m_H=19ilXd!QOxrW$G(&=j) z_4hGnF?)&%wqRS)qj6I_*$tyW&G|d>m!`w6P3tdyAqAj=Z%%=HJVuK)lnW&5GLI2Y zvbZI7$pFY6V=0DR+q`|gc+=9w=rJv+o0Tq^cg&ZDXuZumQCqac*h;?D;;KHyqV}l6 zm@itof!x}ct+!BNf-I@qwAUn?UpQt1#cd%nf@B_JzZ4_I$(WgW#1aF=ZO_d)2kl@s zr#RA@vUMT6EgR14soD*kMuwftBbMfu)b@v4w8F((vL*AsqeRHWl&u{Qi}3 zwiBmpUYkCGsO_pQ6<<)>#xmih_%2%Vf5clSvg0k}EqOejqeFS)#aP<2rHs_h&lMs~ zGxKa-!dTwObKhdMJ(X>#a1@v!Z-QDKx%6C!$y~Bgv&TRogIr|VOWAz6VXlf*nvOU0xUv4ZtUlFayZ*7Q-Z5wkO z<aV$(uR?a);i$k;l$vn}@XdWi6?#jj+%PMDH8V?l)X;Nt%3Gh&9NZ+{af>r;1 z(dM*;?vc;g`StbaV=>gnB!*5o5=i-L*2Z(uz{$PYdZSJwmZHTQ$o_wo&0WaZ^6Fol zuYa&v+gtFpGoRC5g0HJyz}MfFI_3H86LmJ`&rK*&z5xYjOP6_!^paQp;uH|GEf-S1 zfC86t`9xPf23~>!)mu{lW87FLHegz;G0ZXJdim1Yu|dL`LRWI5GGZQ5-TD{D{ngD{ zFTj1iRImM(xOZ=jdxKQZmrZ(`M)^2jh4u%t{f<^)UwC*^$y=A77kpCx?fU*Lq^hA; zy7J2z`yMs$({pmQBs(gOyPA`r8_n0bT+RZnG09*5#kq!#XEKkmb!F1P-FeguZOUn~ zNo<(m#m0Hprc`YDc2pC$MO{DVUO>BiT_UfaS2yFjYO(o!9OvcIPjJ5i4nEEzf}5|2 z)`Y_PD;KRc(*7OjTdk&8{ZH3X1*q%N4X%s1P^Y!>|xXjHriUZ<~_bu~8d7UCBxETL-1=G>C z&0FW2!RL7^XQonop;fCv15Km3hQ*HPHb}gk23_)b zYf+~mz24ZD7g0aj7H!Dz^{}BIKYFeo9s}pL6}BUG8PXf(_&@>ggCD!^8|_nu9n6pU z7=OnZt$)uHZMbDR#X;-MpW_Y27U$ceb@5}lUgko^S$%?gyPoZhw!>2RSGin;b~lA6 z)*jtXe0--NTK{cyWJBJOY#Y%=V~>q=kG5~1#r^AS*+NYUx`cmIZhk2n3g)4{i+=BI z15Xl7^fY5HmDdbh@snKt#9b)Wlzj)E_89muzedB(1YFQ-$oZTtW^1{RR>!ifzIPC| zsl4}hpwU4>_Zs^AZ?m}}p9=fj7qz25yYuUK;f%=}wb-Ar{~R%JR>6p5qg5)F*PlIG zV?x}!wN+|{?CBdz&;pAQM#ykOZEs*F+E_~dWh^^?lQ;f-bYyzpWSl2(jM+av$qo=B zR`LN5!gMNz6G;7}@ju;K)L-B|fa6I0;Q8Yxm+`c0-^K7fJc^4MVQV81S-s2 z%HixP;3yOa{THRI>w!E)`8oht%W$M4KY;8ZDiy^kqt*heH^Mw`$l)&H$hb_Cmu{Fa z%36}%ozr~reax>q(wfc1+=YdUv!N^KJlx`E;3JQ*C_=(Abc);m*FEpe$A13LC+TSh5T3G!|b01mPFJ|j@d6)_bXJl=4&B@ z8=vb5PJ5{z@RS&x5#=8sJpxyM=I~7jXn(GN-Y2c=-9PN@?VXRI9eGVg+FsnP|3T$7rbx3ctT_L{{rB#N z^{e%0H0eH`LTu%6jVWxIs|Jx`xL=TCFGNU-a4~FfVanvuGYkpS61;`U%~TAKD50A` z`3|S-P62$b^4y@bI#8xFViB&x7mE%NJZy&I#!Bw`PVNpv!~$t2M5+!!ie|4Q2#W6} zdgx?5l==l+mdS`MCwV>w=fZSzi8-|kkvg!iUy?*zPnq@waNh<3libOU$=A?!q$cCX zb=@}|rb&>gr~+eB{BVRu{?M#26>;V{MGAEFM1V6n5h*tvSjclqzC^Ko1ilZTTFCKM z^Oc~5R<%SVI8l?;RVFjCTucDlJWi%vp-hLP@>K%Nr-iskb9SNiKy!8pAf#HEIFL!c zt0t)*|9j*%dMUz{pkR1fCgN)zGOtrKe^Yb#onS9MmA@zpEU3tP@GX<5lrK|^Nt%;s z`C|Sbsu`G(_fot$s9aVpSSCYo1%?OdcFIGNQYMEBnZ%wu8S_)YiE#(Tz zN1hFu3($@{A7+NhGn90mfQAYgcOQT;8UKF#hxQ6-d`Z+-CAk`f<&Ft#$hI-0E6ld9Qsdu(BNL4hajhnE+p z zcMmQeynlIldIdH0B})6WjMYg;bIQ^DjB6+s)+*|kT9@1JE6IxXR0X`MD$DxP)isO9 z7hj9<=*QCW*pb+gbamb5)jL0{-nqiB^snw+9eg^OsNR{Z9!XV?B&tW4Gw|YAj9)Xl zYgwEJ)*9N@>e}HSSid_?&W82mAD98@{yk4>p4rTe2mZtXz`d*Hz}I%Jt}WjB(PYxy zm2!8ja~5ZdR!6$-T%1qTox|smb;bA4zG~Or0Mm8#%T}tXg=zu{%r!0RcFx`Sd2PpM zwHKbY@5v^ux$2gxmd@WDS{(Xl=Y!tI zRgcdn+YY4K4m@p3xX{oM1CKr99L0OGwQbN4k@@0BJCd%>lnZWmrm_nRCy{i^=|>kH z?|Jyv>RXAH)7s|`zCTKYqzep57Z{Q*@LyC^-ce${MgLDC3lYN4jdaVYPy2trH_>tm zpFa%$ag+*8utF28&;`yuS7e?S@yG3FKX&YcB z?W+0k#^R6S7gySn?w*vpXGKo9`V*!78b(WoJ(%1vklHbjbnQ>M_W#cIN$IElgzIFY^rTitW@0|$oFJdO@m}-$sn{YG|~ zT>j3oH%nwo*$5Fi)0acpz8s=P5B)}ZI`ZqllK^{RV6CHj<;3dP>ZxSMV5(zq-Hco; zA$|DBC#-)Xpsm?G0@|9LBRtLfZA;YR_mXZ;%I#SgS-5s5bo(_;)HOe{tvbN7^#@Y* z1w5;ZJ$rHA{~hdZ*7dZ@y|{nz(ES_BKU^6}xOx+%y#|I@=j_GZFV$s#($$r6ku)r8 zWJG9BSD#yYV;NHT96peT;zP%(Lwf@x2|h|p&`3DO)i|@W5%SRG{=BN~v#PfEp7^x~ zp_T7GzV;-XtQtyH4dHsnMoUU<(jlZA!ZWVC*z-~y4J2K=Q!dDOOIdG@TRP&-2h~J< zh&X^pqmQ>ge0}xxTnr1PcXmDqQ>S~W)4kN`Ua&=N!_xNUj^(~&O;@U>3;wDQ9XFOP zB`UV#lWSwgl5hDk)w6?vr_N7Ui`v_oyJ>0i?hhA#NPMV8r8{;$kf^mDYORM_>(Q9- zJ6MumU7pgUfsqXx;};XI&O~XaMn`=iJzV@<{@dZFsBGVtjXUDvgG-MB$;JaIEPrOc zei#efFh1#{$JWi9v*t^E!tKgVxLq{7UHOw=i%IYB(BLvJJ-w?JXmI;zaQkR*`!G0n zr{b+rro)@1cSs(JwOp`!Y}dFj=kmM)imrs23j_{bH1 z^OsEznjTw|tpmx1{i%liG22>Q^HTUDWo7V}(Ff6F%id(&zEs`5m^DX}!EC3=QM+a^ z-O@o_%)IpN%X>L+@Dp0U-LFu8U!nfK@^vXKgr>U(77r|(NLNRtxA0{rXt5}SMOMKU$wGRV z_XBU-68Al-S-J68S&b$=M^c_6PkoZ0t@ol8CPv=hvD$)|z%g#%~+r<9_rX-x`Eq9sc!|Cs*?0*7hHMI`-?} zlOXV?XH38P+V5%dw2YHj1q2T30U?_jmo9(squ7sFBc64WdD~%X178e$DL_5?rQ?BP z-Kt0R4?eX$E&Fs&vVSbqKbA|-N)>TKM?V>T=CHOLM_UBfIcq%-Yv$@Y*2}r-hJd!#n{lVpDcqZ96o@yLVoO?6jdNWb_reV2$##L>pz>o|H zCn^MxTz=gDWFYA|nDQJ%1bFv;1cVTd;`Ss_LO9C6@4}zH@%szEjebI%%fzki8GLH` zwdV=VyG&I2m1CbUg>DR(F}aC~CMRGKSLwWSBT>;7m!a#w`nS<|lv<*DGs59)OP~kd zo?c{M43L8CrrNcn^pPRp9qJz|rp7u{tt6EORQW`-ccfJ}A=nYNXh4U-Ig+E()fg$VTEUs(mXrT?WZ zXA_pQ>lTw03xN@o6j@#CoDo!(P(CB5tF+>>mJw_>W??1jEL5Knl%FtLv5(sdGJ>=2 zYjzhMQ3fNVeh2IyVU_!9tMOWi(SkXTi=1(?-97ivb$H|P7&8!?=FLB`=HCg!^-Yw| zx%A@z$d;=tM19FTBA6@ zzpEf$M?D$qwq{Nw&k3V_yZFdu{Ib!zb25$=m{kaNF7|s6d6w*Kjv;WNLJt4`8GkTl zyN==W(;Z8#OXq*%!3L}6Ne?1o!&*W<)C|k589V^Rvtj(k5)OO_tNK|Rt^}HP2?mr9 zpEHz@Jo}K>k)8rCXXv zdyJSD<7b%ga~N6woIz0gnMC`UPo42=iS0-5f$d>0wlw=6zPY?U$Rd(royc$lr-Yvr{cUdMu7*ZyeWvGd`9RY+UB~zh89gp;hW1zLj$K=7O*)!Vj;4gA zDYN8T3go|r--Gfa!YF>$uVU?%})r1wyWt#{oN+C_lYaG6{WwKELHjEn{MP#mUaM%6e)p#cJn zbBT)z^n!2fN3`G4IV%4asbDcq`FD`RAP^57(ZyTVIRafA-=5&w@;_g2y@?ln)-6T6 z3HrnT2mjCFppvsW7NEW_489+{WnM2b^JE!%4m_hcOyF!n>8OQ=nAsRUWAT5=Pd#TZ N=W)of31GATe*+pl;nn~E literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..243eca50ce1800bea22b092449a6d55f1f254db5 GIT binary patch literal 9327 zcmd5iTWlN0cDvkNa!HD!BvO*~Udgg8+M;B|j_o*-5m}Pok)6noSdPOo+||S8L)l%$ z7PItKZc~&g43th)n7MIq*}_egMnMJCA8wlu=kZ}&^kXRyEwO+KqeVUf^g}^z0YhIs zGt0*=ZRa}Z&s`1Ao-=di%wuQHoO4Eh?{YZ^c>etOKVP952;#pHQG93}A%FUJKyDK} zF-hVW2 zMO>3EjI-hDhANf4(C??v5Utj zH#o%ooIF{OWbW1B@#9CvCeGrnp%#R91#y8Bt_LG?VS$^CazQQA=%F#H4hZcxL8 z=Q1!S#-_z!1c`uQlt_!lP8@%I3{9=Z%*_Sl1>j)jf}$j7^juJ$(I`n4HLEDd^I}w^ z;CqBh3j!Lj!;c~e@~1rH-Ud=Olq#^;S1g~wV*3IwIN&8-Bod@TW(-^?SAWclFJa+f z^YDbZK1oEKTZsWeqOV!5Qx}PABuQK(NcfYPq8x%yEas(~pk$k&l&UDDqkpoMkl8Xv zHz7_W7};6Q;VFf=VlC325IhZZN#-ZSr-&{|5IcCrNb}aFVpRg_+Dv7vsm%T<6D4^^ z9Qe(>MC0U%1apJoS=fdcyGC9k^jR?V)hT;Q%@GQH1uH9*W0nX#se;ndDA6d)9I)lB z6NJw-zRAqXQ~m>=lNu{TVTI2|r#I=b*I(y0EeE+xhU*E+oQOX1CV5aq)38bUG-8uF zeUjUxIEC|7X>@E(h-$Pb1bNW~93omfB5E8K9NOp_jkbZd;xp6#1k(CncIAHe%W>;*aKdq_uMi7pZw78_H$?y607XBt(PFYEHhZeMvq4yx+A>&YU265t)Wp&o@Pd@_+-=k`_3VY**-L6)NbNhb z8oD=qKX~s7ppYKy`ELKif$t9LQ~?G<*=jz^3OQC#St0MPNxoD3gML2VV4zue|F4x` z9IC_r*Gww3Gi1I1Re;>1 z57_Qgfcz_Y!1h%qAYZpT4!=x&-80M{-ba12j{)L{#>iqY1d8bGSS%bWsSuD>13#>G zRLFf!wPR5%&!u*#|A*RnLa~_CPQ~T|1%tLg;ZZ6}tyn3Qwk|2bhN(r#CQc|pC)dMQ8q-c=wKoAL5VMPn? z1a()Hu$#u^lFK@gfSRQ-o7EF2uxg`Rpxwqcfvy1>X$|}UT?@3^K-U@hMYmC!u_O+C zhkjal&nGnRRqQag)#kpCghGm~PzS9|{EQNpy$OeDT=j|rYE~RhByqDI&x93P0M+hm z7#ETL7QG07c}a+k2p~fZ>sS#@4%V__Gs0Q`#A}g-gN+)jEVJ) z2&|~tsab*Vj|f2t%o~0vPW8PoHIL3a`2S8&a zFr6fEC&DeUtC|grIUd_i;n}Dlq4lYsAsC9g5T6a54PY{f`+-72rB2W}=wx93m`;ZE z8aO6yRWDU1nI!W^a7b)e35PppZ%R+xxwvNEzIZslZHHPtu2y%VxEw%oxJ<-&Yp>(Z|_D5#3_^7{vK`%jeVN3V?KUOA(37c$gc`|?<> zcQDHhs*uiKP#te=FvWV%!@8yoTao;cpqSR*BLGqXumtNuXKZKQ+q85N9nzf`BuCfb zaQ3IYDSyhJt>SW3oQhMvrY?CXIglJklPcX*JoNmCPIH<4p z53?f-^)15yp}C6gL;#uJCSx0|Pkic)g5i1lxlC;t_>0e#(g~`NX5IBmO>H=Lh<6Fl zc0|S?zt|1|J|a(>&32wCD|Dns6Vx=3pm`?2C>GvUE*m9Mmdk4it77F1Cs4wsP@ucv zv;*x)!MS1O?d3WNJMTz1;ODGxKiFrw9|a%1++&1&2EQ*#S&6D&Xa}ILQ+SlBiurXJ zPXWbMQCh9od1t{V_wiM7>3jl5rn-Edn`^;*xS+Ijx&vMPDFgH1PB;~Yr{kb*6HJPX zeyCV81}mc2NBBxLW{C+nJDTftcaU$0hizd!bTeO267@j4OxN^Qn4PlmqKJ)a~P zrAKii%f{RzIDKp0-({Q+rKZp(_sllEMt&^0=4q0jyJr>O16Ha-sTDiWCGEga*BuHscLHt~%{4jAVaBUfSF7}iX5j&D+| zu)lX1>%pFDD(|_%+&1&gMjkweCcdXgALd(1(n~8Hq_;dpdMijT@f4&R_?{xYj&G~z zQM*~jr*y&@eGlAyt~jIEvW_M^hFy5{nLDAwyzUZS#rytt#dD>$C{6Je=BCA%3;U8Y z($Mox#ru^0cN)2%Ru}ZPu_AA)k;XD8<9fki0?!Rkl!YJxybbm^{fyn$t=RZ&VA*bm zIoJX39>u}?FztjL!J5ZRf{wnKlaXmwczBlIiMV;a_Ab5`*YW#IP z`bw^wbuzNt3Xl1OF!LrFOp+QDCJwp|=7drj0QNmaPcYzf&~OGZU}^UoEbUFQU$?2z zF}X?hL8L>E@<|#!H5(Q*t8jfz2+7#oMiH?qK*SxvP)L}Q!KCgH+n^%0$m0!1hL4}( zdh`lVrZf9A8bu+nQ5$D)JP^#}&LJ*t)ou2;Rj(Jfyv!A4lx+B-ZBB8AIAqC!wI8q2 z`E}D@9Dw%YHF{RbQ0C&!Gs6=T#oE<_L!!aB*BBgDjeGQ3*Th(KS`ShlRo z%N5M-cvUg-DS^A<^I~5?qpwIYh!cflK^|sVnhVd$mHtD?A;41!QUzJF1|irS<)M0P zHY#EdV>kL9Xi{`v1G^a zD??~EEFovl;D#7c-6dg>OM=4F;zeK`grC#`j@KfwZg(XknQ7JDm$moh?0sOcGTdtC zx~FmJrSxmJ2A2ktECi|;4i{hmfhvZBK$S7CTw2ETK-CjmkNO5yFROirAti_Y!`ZRs z?8s1=*RswXIp>aLGUwc>I(IDw|9TL8Fg7LVm?wxpYLHQgJ;e&$v3M+}p6zPc{8 z?`Akj`OF2i)}O8Q=W6}X zQ&-1oZN8!L_S8pHw`P`RQWOl;)qx8zfT6lNV5r8ta%maUhx!E9_cisY&@IQ3BRRZY z*O4K!bzQl-uH;DGU7y~v=I&J8o%z6EAM{Zw$i4y9))y&&sQ($7{HW0-~2+# zhGt;+mMg{HVjnfP|F-8hJ(+#k=AF6bolw@+`P(;s^G0Sm+t!zB>q|NEEo~__?`c*& z+rNBq)pM`m^P!cY`$yMyji|du^4`|lr$0Kab|3q4Y<26s?VrE8@+uIJ?qAd2S?}?j z_qggkp7*q=9^Z0kW%mBTwZ1X6Z>(H-d1B>aq1uUxYU>@{nTfmSKTh09sI7yLpbJep z2BYzS3szG*Lgw4IFMI#7=^vU_4`h9VIp1Kmeek}NZ9kkk3aw4)eQTyyu3cSIS7+9zXux-MB%x?CoV>TsDm@x37P6J!8u@_T(CSQgq(asCu@7 z6U?rTuJs&Hdk*Bet#{ef@qGKK)scJ0)b>-59-P(R08P{UsL0!&I+{BAsI}wHF|_br zf^R>gHov4N!zzUJu0I?@(Gz7qOihmL01Q#tmO z%ANw`d)l5nuR4bGlAkSURA&eF#)B%|A)Npv z`BD8I>YwQSwtpe_+rDwup6IZA(^`Lci1}uq3gJWa2xxL2D7XkF{>)M~f)k|aMytYQ=Pd-yE6wTC)-(OKcd>2A*JQa@SSVR+txbz)sFskcSA}}4=-K&J860E z-z?l+SRMY`8|sen``!27`D(|5i)#nRRri^!`%KP#MrF^Gr5PJPzt+40e$3=!ZoFc3s6{E>@%~_y5U(_5w7#~FLcSw-lW+A0X`NA1T;q=Ff|Vs z@j@UVqV*(>A@DW;%?j=WT*`{b=NG{kBt)cqM6_xlgsuNa2EK9CY>{AS2EyIgMuxAx z5S4@1bqg8U)tVLG{)>9JzG9)EkB_Dx8jL_6G+Kavc=((Ur%+S70Bo{@kr+Q877mFb zkVv;lF9C!}CCLpdOVS$z0$zgLsuEqs^oVdS;=erMSj2yMqF4Px>5*9o2+R|lYEF3q z+ImXL6HTf)ZCD*71bxk**+VvO5KjTUqa+EI^b>I0Vir)A*G$k=$@m)8q*6_Jx@vLc fgJa3F$+I7xzj;1Odvml`Ev5~MpqqgUPwoE!kWz%s literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..355d5d82b039584770fdd201d72484dfae3c0d6d GIT binary patch literal 15530 zcmeHOTWlLwdY&OUylEs+qOO)LjV`uDUnJiWTk<6If2#N)EANGL^2!t5GMbKh_-8UI_U;Nbn zKSK^V)Fr!Zf_>@H@Sij1oH>{O|Nj4+^Uu*gS5`V12tOG4<%}pW%zxoSAy~8s`{GTO zVeT^`<7GrvG=$F371V%khYfV*MS9cbC|3 ziSabW_n8@HNKzyc4n~5q5)25kBE@175hkNV2!x`tBnp=#Sq?@c!pOJ~Bhe}156eAH z=Xrl%IvA0JKr}KLoQe~_f@QkJXh7~AyD&UHFflSVI&g09`LUtlb3I|v)9)07UBa~F zkM#>7c+*dWtMSQ6iO72d=~gTh3O<2BpA@xf!u`FW$1~}D-bDg18%Yuk^%}u0)81P0zSf9@rWYq_W)lnDex+a zLdNn@B0{gbqaYGmqdx?xei51lu8odO2p|p-Mjng^H}>UOj9u_)Eerp7dr=5WemRc( z2t;LNkKmVOi6AeI9Tx%+3r+^%fz~4sjkz(&f6W&P-jD==)-WBMn%;X87)XS$pIk#; z(OgY_z*I$&OWq7dCPVOsveCO#TF@O$gvd&eQ4vymLy!^@BtoJDm^bd*gz04l2GWPEZ$wG09VRBjM84c-Ry ztIlEHh4Hb8vB9x(s(Cmfs^)W&qS}C509dQG^Zr{GLUCC&k4iUH3r*vYPN>!6zQJ>2 zm*D;3(V>yiQ>t^^H#9sjbZ%_$EXGGhCx*vCCsl47kT{{*FO7^3BbQa~5+HO!wO*po z#79|%&P@RDRomrAP&pS=RPz--Q5``Ukb&B(a=l~1Et5#sc6@TclSv6k`imF8pCM4B{W&k8gc0x6(8B~~b zLo5K+N)Ol+JhLzMLF7J@WRr|f&rF)&3HeQfhQL`=G%WSTL0fvGfj~Uwj|65Z(&S#51bSu7Ec$|^H;7!gK2qnC$g^8*gXY8g#%$3Rs(U$OnK*b^R8aj=hBvIpLl@g;%m z1&RY8Qj8b|pe10VavKmBKy}Z8vUn?9-2>N3*F%pMLu&6Ky-;Su_5{V(U*b$evhV&=B3GDhNLx!zS~1ESTAbq3(4ht1(_T?gLWa17CHQY~oh z5Z5wB`buHBKS_5>>QI zIxJCGavczmY95c;E#*i#G(Moj*2m!i$SKF60fC4}UGqv2X*njvgjZ}2IRsTew~;5R zIS>>zhP(!kC8(rAFZNu+<3TLb4g~RdU_o3AE{4<92jE%}9|pA;Qu_fNk=P0uM542u z9LC2ZNRA^xerVi!17k?2ir}lIxDpUoCa!svF%mn=9YkEMOSIatP6Mt$r!lZEG=7$u zO$*{m;xxng5tRFwmPX>W=FO-D!SvWnPD7$<)s{o5Ra?N(M5=uOT@+9Z8-*YH;uu8A zAvVQKfq7Xrno*MomYk;P^-yDK9`%@1)~~Wx-y~Jn#QmY&)Y&S3hMxpaMB*rIEpT>EnhWkSqj{{ws0*a zr{onmZQqrLnW@NdFoMQzQcd^RNFTO}V<$(Epa>{;R9?m^wC$6q+AOojrACE_HBO%k-R<(@6M#o^mbqzU3tD`F< zh-ra7p&HOowtB*~6zG-~ra-rRC|DZM7(6zO6096n#LnVIM0My}3bm3(3ws3Bi8~1& z-9o6GLj15LDL4Lf+NvoGNf#zUU&ciRn2s$iAk6Aq^A@;O<+in^ELr=OLaNXKsm>Jq zQRb@Vuso$rxp`F6-s7O)$G$+dM58f7laZ|G%+Qk{l4L)E^pEvC@H7AeC_=#kqV!a& zAC|EZv0xBINGmmnss(lsQle5H8a_^7A(S!<%g)a`zqB`hVQ*gQ%-CDA_SSUa($HF1 zPrU`@!PsB}bY$8pi>9tYE?q@UVaYPf@_kH0f}oJmCKZvpYT~%gRmMoFSgsB2$+|=X zGFFGI(1UJBPC!x#kllG8*X50gn*y2>>qQ=bZ510t7u;>&z^H+{U91J5H{ouGZt#lZ zT_5IXG43;pE-QvHPNbV`7rqAYvJa7N~$CT4QzT=tcGp zB3v&$RK^b@vVqm6Q3GQ+s2bK^?28aY&N3`jn74c9*d+UPYGY*l5c9Ts&ZJ;{`H(aj z8^6NbXIW;xZhl`;z03q5s#~+Ib@XB#)N&u={W|QaeqiY(W960L)CN}@q6a?Ab@o32wY44r`JEZ^^13Z{%+>*>FnXtTI$pG ze>k{s{qF0FuWQd`l&S!%jm&a9OrlV2x%gEF>=rd=Nup*=-`>HFv;zSYRM%>CuN->V z53x+`NET@INVa+;Z6Bcxtq~BFJ%RU)$S;+9adDnxR-pXaU=)|ppIBOxaf7W{K?|5# z|1E+TA;?uSi=@oFtJOXw8V^htInk(d!kB?}B)?XC*12Ovd6>xVeB<-FU$_2yYi8hL zcHm;Bb3EHQj#`nm3u$^$&ZuT7a^qDMI%mEQd+I#`_-ft;;|p6)&05kGIjTz`ARa0E z<{^TMgF&LK688rniBWDo&m|&2=T}ihwqy-uw%|O6h?ZNmQ zl6Qfq=2%o#*&8yB8=N2c1-okYNwGwQE)FR+3HkCU5SX0!>K~r^;MBs<`{(D+r`TuJ z%}ebME@!Gcv(+$Bm>g%>XSG`%^ygYT(k(;U^?BgAnRTCKUouEx=BPZ&epT&C*)=J# z5@~~~>4M9!RnevKA!Os!yaM;NA;|_ABbVo31GE0*ZG`olIcX-XrB+C>7VA%%Vdshx zVP|xCu91yNlg&P(TeDjR-=z`^g)|qnh+;x#FnCb&-b#>`MFKmf=>`>1BQ#C^76{Df zR8D`733q^~He61i_ZK@-A}0`iQBLp>fovIPCX|!wha(@1EclmdGyK*pzcs~vRoigC z=Uz{ywj*2Hk+S6~YGJ3~*pKphBiFhe1hdssB)MI?pKO25ncVwdGC)AKmHSt%jH@Ou zH^X|~32g#o*%v2kG*K0&gE_N7IoOSrgH(b8kDbw>kC@fMC8n&762&o!9=3Y08Y?S} zy~~HP((fykg&bJfF*CYyLO=92jPJ}@lFTi(SW;vYP)ESzE52)nd`F?)(wg!m^*p7% zPzqW%&r}qiAg-4&ww^TmN=mKpg*Qs?;1De7J-T0#7BDWB(pn*vdtft8xh#XGri^#E z@yiEePskHcvZ_K}=^a|HE)t0_&i6 zSD`gny&8B)PAa(1%!f^+ftH1aa%pVxPSZy382hjWFX+q42V+U{qfJ`du!n2#f|haJ z`ZvLgb2C{hxG>3wH50ov$<3f~rXh*A+gf@0+_f6Hw1%I! zh|dRON%AksKp}_PE?rxUn3}Uud!^^<_DW9yyQgc{N@uaoVl27VQf!3uill9(tMDdR z8D2r(U_L0gdCv#n<<3If*kj`p)KU3hjh>VuU%6PQ2l!wUtBiaq%PsqAZY;Zo`{;?w z2V+U{Yd~{}W)@08577FeYmph1~#)MX$PBG z3$vD9C!Mv{U|}7bi3`?zD3jZNd;@Y@R|2K{Epl|uk#xvihM8=-&@-6H+@)B7(bhdM zZ;Tk&3OH6utW`-p^+t)l1@pw56R_eGUDxP(YLl6;Vbd1BZ7DbYu~JULM@_@pfmK39 z4wOmxm*19@zg0bJ0!bV$jOovyam}Ue0~)t%Ae%L_!8#fkD~zLj)v~~n6W^9}{#QEK z0;AUL^*64A6`+GnU#o*#|ExN=jmp`atXS9Hu8}tMwXYyuaO53%3oOhWKUXw4-eW!6M+t5!6IMT-8WR#0VebhcVH3LXv)S=itS8Z?otc~z{NNLe?1h6q zaHg`v9hhhkqj7p#4vw#tq)#L``evdYPBzBin=Lw}v^wx9!NWO8-IoqY^UWW;qW6k z#`5PP;m8~w`UK}D99)#)(4CavXfg1jOQD1f2%eq4^`$H2ZyRJQB!(e5f73Io;Ngy_ zcaTgWL8Oxu66zSlZ7Fr@QlBC5;A1xu^eNFV(W*&;5Ao6gg1!>fB7z^Be&kl!Tl9;( z%FYsWWzb^k?T`J{o`WcBbWMw&iH*_e%|8J#C!$h`WBJG;URlDYAG5=g4fAI5* zzq*`hIGb%an|7VeHEm4|%#ReubS1-g=0~Y@|H#rny6y;Ek4#T0wHVM0-l5;IOBdZ z>wYuMzgZ?Bo5NEach`zJqUOtCqEzf)o`ZaOt#@n+I8lc zyK%{Uw{Nj8H3Z*kmo2HGg_=e8`y<8&cjNuOdwn3EiIqbdE7N?p))O5`oTKlVt8QUp z@$CZd*8;*df96Ym+ZQ~@1R#;+g)}ed@;|k*|KV%tIzYmypAG-p_D|W*%>TOUlU(MiyYj(;?B6XXI8RhN_qB_*#VXLOn_1UR=(xKMzk7^p0?)OL zJZgW^m2Ml+uHWqc?Q8I5t8pB^Yykyq)Qq!VH8kFr?nz4ncc&Mp-#-N?XwOx<7vdkx zrRMUu8PBx|%W-^l2fn!jU)=FkLC3#=QR_BB|9{0R~| zv*cf%O4pr%>(RJ&|Fq*XFh!UGSB5{E<XL_Kt^JRv8O?WJ7Yda=`-M z?&^RmO9$^AT{!xzrESIh!t=km{@Zw_;c~X&a@ut{S5~l~K<}agu}>^tr$9S)!DI&ZV(Gy0VVD~7%DynR zG`=vlFqYxFvV2#X?20q+tpNg8rs{CE>TueAn0~h&CDX7XfHPj`Ri&qJ zJXY<~`d?!LeqS#+ll2CcwP-6h`n8+BWx-TyNh+>s2z|ep?#B20o)7(PIsL_Q&vu`EO&{fmr*On)!+%SQsT1X zqmk6bS?ET?@MB+Gfr#;p%SVv%G5oZE$CB1R29RWo{!;Kl zv&Azph0}aytt*tZ=xPL6@E@CujmoR45?NMie-N~8C$6c!y3u^-C z|34|?L6w7r1LSMTb4+_#%xJQ+@V^dg$#YD5SE;!7eWQq5}wn(XqCAUP= zS?^#rp#>$TwdytPaj!X@eyFE6XeHPMoM01pgGu591Ek6*pp^oQG!pE`070Ne5Avap zB(;G%?|IyF&pr2CeOXy)r{MZWXaD5~5Bn(UzvDypGAjxC zhyM+U2NX*MD3)dolXTb+FwmGbP8!3efGKPan8TKU1@cU+d9osG4OqjrfGunf*u##1 zBkT+~!-oI-q>|-{A@Mr`nf64%esdte@*Z$ z_~=|{HpDSo7%nt6!$l`An~IEa zAwI-J=OTP?cAMRPQk%o{j7^2ZP)U>tav`Rtm)W*$8`JCWV&-5x?g_1px@{@+5 zr0@XrKF+j3?lvY0siV2n7KU_?&vXvnb!l_#_7ULO*!5r}5}IVDrbAp1Dw`T7BWAzIJ0e?#iA2bzkq{S_4I^{1>C({I z5xD}nc5Z@~&6pUGjqe0G**Y*fe0gZ(_`63c0TbCU5s{4`8L|N2oy)(FGd z2*cV8cN5$#a5u9xtQGDS*2CK2Ucq|VD!5x&7YzGa*-XZ~Y>aYa0C;XJr#ql_OdBaG z+f zf2omqB8QA{w3G`V|$m zZF)|&j*dB}@y})#@6!SysKZaI>v?yqKAQpC6zU zC0jtV&2W*i9GZ}6f$%e7(8PUp;?AlCtI!7{m*a^j>BLIM8mDLOHCfTKNsj?+uShYG6 zmIX_)?XCmwtB%T~cm6=)z^c=oIJm|*KA_&GZqqgpq%>r2ypS1R=dx)OxEw3;MeDZl zHjK@5jy$uS~Hwrk!C~^%aI~W z+>&us{{=)~3U6GB$mj`3DGm+5jG}y2q7EL`a2q}*7SHWx; zy)iL8`cahI4|Q?}5DZ{bmf-X>SRiCJQ6?AbXvS2RD<-1s#QPIGcNR;+Q*d(ndQeG3 zX2Kj|$+ZLUS15|rI5orPHE;$$qa!js7R4cqhB{n|&b9DUH$stU%&E*%$`hH({wF9f z(7KJy3FDff#deVf)p~Dme(>)3h4YE?tM$!~ZRy>g?Mt>NPOVngK4@HQyx+XkoHzlh zHF{ zOdek|Qguy5%YT>a{*E-ed{SuIF1mL}?j3@A$A8f^Z>wxbap~blbE!GfjWvV0dJ|CS ziT#oNq4Tjbc^u}U2Xl*a_iruTTBD4$o6^DM-RX(+#A)l@-`1HUp4}ErM#k&#}nhuKYLz4TD z;64OjysT;bWS`J^^65nY@cWE?e)8EBvF3tQb3t%kAoC%}^;9IJnF&$+VSLa({5MFT z$&rTp#!IVFxOd7c$I_q!PC?n+e3@UfwoaT^)A_G+X>B>KvAlBF_R0|!EaLn>F!5q0 z##U(uI|auk8Ft($Nafjg+%P=nOxnz#eh-*&0&(lh~u! z!}#O)@|@7R4}Nhty*dBp-E#})66Zh^U7jELK>3W+rUS|w!ag$WWg{#DiEK$;>M;?@R>dgYZNoNG1ryBf|{=_Ax`R-)~VQj>uk4 zx2rP)tUgdds|r4fOwMX_?h;m$U2A2gkRaqme*pjl)9SoupSRz2E;tiT&BL0Z!q%_~ zVwh2@Dei@nin^lkcNR`4Hv*74l6E07;Ujr(!xbocO-4s$`{-zRik+Fnv~zUy! zl%a*|Iu2JP1oS{6`Z0hzxt}$I$y~ceX@QeApP*sD>Y>GIu34kBz}srR2xT|G6STqH zutsTt)sA^ZfYM{^>=^vzu8caMf53Hep1-0o12ZxgSj%3Y0f z1N#Mk^bdcZ^o!3^BXL^0v?*tz(6~R)HIl)bB8naqJaK>cO$s-W+p-BvpQubva|hum ze_2XoBj!@NpYvW!VW}!Kn1|aolAKi`y>}5 zSQ*l{br*5|U4eYfXf6Gm~x?;L46uGD2@TtdcVc`!G{vT zTgEv+^Z85wgr=vWDnjt^5fqNL0RV(xDm^=Y_U>B?ZzbqecXhID$&?JH=p{B07pzSL z!6DgnV**`#d}x+mugp31Ltr@JjW{j=%Ii_5O=y!Fq&HM}s>q63AfO3B#~B?l?zl zSN_qfFdOC#U8pB>eF1mXKXTg`H~cZIz9JwY;OEfLjI(N=BNbYj-8Pr78emn&n&M_y z+hMI{RodXmqCOR}EXwRRy3&vriFXh zp{6I=do_lC@s2!ty)IG;R}op&nL8~UY&e$l;M za&J!@Uo+!sbYnGZ7Rp_n8LJwO=VlB6`2Kt0c*`qs95rL+A}h3la}vfBX!*Az%>| zud`CyKGX?T2JcaM$)gs@Tx=EC*?E@FbOk)SRNII6y=m61=D_=E^=YGRelJDb^7Q!y=9&5;s!~EKUSBseu50DuABvg^vg4Y9Et@* zY$2i-Tk-uU0vu&rJpj2zQKQ*yW}->w@h$dVaeynvvuxmRZ~@HRXghN_t;c*Dlqylo zkKkSO-+(lOX05EgcX|Hu-75=MV7JlXy0>qBU-ES7wCHG;9AG>dZ1q{KI-VLAot=`i zQ*d^^^wcHZQi~6Wj?Iz-l(5m(q!tf}&JM}hAvil;x;@EL56&*0O@%~nhve-@Uy!`r zik~}i94brE_xCRCO$-&NlD6%B>8VEzzWqhRcClfn)UZ?Z?2)IHd@xDWjFyF^d70N2M)CN$%giN`od_Z5HSJi3d$i*P=^ww@L0cFglgRn`Umpz5g>Wt9&2N3T=Z= zcRmgN^`56ko}GC1;jafE1AbTQ8&f+To5Abe_IM`w5570juI}Ga0MIkqt(azYz|6w4 z)G5%2zn596qv$C95xYcdeU#AlM%JX&1|{?)tbnv-xqn}@e@5+mlfPQZ?je(%YZDN4 z!=>$g30-DnE3`c#`mvlkO`6%!#5>haXlso2@GkWo?^e^S6|m2nv(-1+{_FPx;|8vl zuT@LOjd9Zlxw%@~dc>Q*=UA#_NgnIxP27DiJjWXKv4lyQ`#-P6Wt-xwAiLs)XE!6O zn|Eo9im>oaDs8lsyj@YE-@2JHNk{!f`>k69csvy{*s5Fqwi)H8F31@gd$FB`9M zQH)ot?@nR zU+foa+NGNI#K~-%8aos0+M|m{MNfz1=}4S<>1j!^pAU$hUdhu726<&4+1OldeP^|` z{mI;;xretN-}>HcsO$S31prLr>OOFI__qt5(;x3n86isL9i=Y8)A3g$PurjJe|=Nj zb6VPST5z5&fS1oUv;nX0Da>81ZFq2b@p5WLtnHL)JJUg_wrBa|i`xFg>4J#Vc){nI zq2MVb%Js$TshRYc=^n1UF8?TUBBG_ z>Hc3H{Oll5xM@33xM@33xOO{GI1}V@GF| zuV3=|1+Rat3FCM+(qyfff<+u`4C&SuK3F7F{yjRguYF#)aOv9%ffpA7;)Scyg{z|P zJ<0c;;C^qlZ>QiH{CNK-m(sf)1|A1QPmkp35j;Kr+V<}{pBw+C_t(ARzCmfO+xaZ`>pjnoJU{XL!{5MKaQ&6~ zrZeBTw@UO)R~Gt)Ticnd%)XV20pO{IhnA$S&QZtx^AZ^7%93$ZSQ2z*V!kB6=4mn0 zxztw};#;^aBU@;xQU<4QTZ-0cVO?5-AGnq0yo|$!Z5+QYqZN=R*j)M=H<-v(k{fPq zt6aQ94|Qb;H_%YpaOt#K1&>~)%oVTT(NCGVw5`L^B5#?@H)l&hL`pUED{o|}Z?tXc z-4glBig?8bIr)F3F;}DQB{x!nM!K@EDY4f4WeqId%jJ9dqtK(n>1YX@bY(#@yH)xZ z|4yrc^GD<>QQ!LtJ=K+kp8EfQJ+0OC^h$Bsu)4CZDJM35OCEl<;_a2>MfpHE~4gFQ$j>SUwv4OoH8fh>k8rh}|E!fj}dOyG4 zFt?SZ-^O+Bchc)(+-%miU($W1D_gSO4N~$=aVgm#Q&6+L#2km)_pc!l{H{D|TKPSB zPj>CN2fbVVSl^_jAdL0?;^TqUm401`VyW9s_^X7Lig8vayBr3r7t;^AvZPn#SS)y` zs#yE2TDovYO0=&l3-b{=yE0eN?{p(Mf9BNklhCOc?td5?b#E3MI5267JL8qFV5M5X zN`*h=DrKc=u`UtVR7zV_#jE&z+14luG<0K84b8->U^}1c3wo<|XFPO}|bbi&<}k=02L@SSIFS;EX)W1hE%4gWN>$+GI!@ z3IWl28Yi-UliqdwbL<0y0R2HqC!{-RlIsq4UBqE!yVa%&+!jl$JoC8$nbDjqp(bb2#;s1Jo>}U)) zulGE|*}=AjndG%p^-?GiNf^J&L}=v2JN!R}A7pFP#C$MW|ExCVqcOGX{-LEqg0ofq z>L;S3LvnOrhy^+8g?`BK)cc~dOLBGz&Mt`E_{0N;|1LkeoSqR|wn{BqmxEFZ1aj<< z8g@X0hG(zj*(*5rs#WF%pKLGOk-C)WiR+OIP7+G>{$;46U-I+|&i;aRoFqp&m40a= zSTvRF{^sbfj*43jNm~v*9TPn#B+m)Kc|xu5tmx>H99?Tvh3&A~sR_~9BRP8nC!EzJ z5yq)5CEz0sQ6C);^-(ytP%H=>E^S?G6{|N()tljXX>NCc6`k#pvt4kuzw|&fNGh1F zNsoLv`st|H`G(Z_##5u{IV5?2DTma~=JqMfwl=jUb)N#el^2_Wdj`SJYcpXn;58n} zdW{F3@&94&-_HHbtzX{~eZ!J(Sa1)6i$3|`QZ#k){^6y=f|F63%`whs+oLwC(i{)a zHY_%z-cYbi?~tlH6DKgbrv@Zs^wFr;vQ28)wgM>amOQ%!=k5Y^W6(~HIBMM_M(9by zqlWYwVneUg(7O!swRJg~3l&nU$`jeVsx%@CM`+8c>Wt{=oZYy8<6rbcJQdl&NgtPLx^R=DA=M5?C1E#a*(bJcms+>4R7>09)q2+LLcrZMC6zCO{r5) z&OSPu4vEcuQgh$(1*y4TtluuxZ%>*Fic>in3seP&`b_%Ta>qCQzv>rz4@$iUpMsnp zmpsP>=kXkoL`Re4Xu{JPn~|CO7x$+!`;ZVT=;?-Y8ZHmS$&vpVlikurYgbIpJ4c|YqbOZvx|F%SY-SeneH7r#P3)W#Jm@WttF&r&81~=|TUU~{M z!kA&S!A2X^9I>;9j2?eYgm2^ z0gHf~=8Ry9?5*Fz)E^=E8G?U^fY?rVG4-bih_w~M)KLV75xk!TSW~nD7EO0@KWheq z*#lF%2H0tH8y@t`2Nr|58O!AZtHFE}^ELph)m)87LN@>}Z3aU^3#>*grv*+k=4nBd z*9=jSTF}>xd0H?+U#HC@aQgH|ZwieFd2oH6$1-G-W-k-gNkCzCi164*fuZpEG_7P|-EdJ$kKh+?**l;_#_h>v2_ z6H^|EP7dL4t(amEv>`y-orFbmNI`{7qnN_+rW}1GOhiI)TH#-}9#T$9AL0HLyag&! z(Ix{$tr=;WUbDDq(;9`KgQD97YIFYYcT|s1{CCY{q79(T{y!*#22P_BXq5$btneQ} ztd)u3WP1{fOrf$>s$lMz)+{G!8V-UNhToI?-{rqOXBaWkIM9pVzE|G;PFo~mp=k`T JE)2*x`oCMFDYpOs literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..373b59233bf6d23de99abe8b6797d549ba477129 GIT binary patch literal 16164 zcmcgSZEPDycDv;ATNL$aOO|7={3X$rC@Zp@L{Xf`66I5@P_`)NgNeb=+?CCQAM)%n zkretsUsHs+^ABB+z|JKuoP(XSkrZ{VS0GmeX#4L_^aoi8EwQKpqeaoX9|dH{KMMWo zd$asnlG?N4+%0z>XJ_7f^WMyxH*aS4S5Bv$f$M{*-@diHmtp=3Uy4_wnqb%Oni=LQ zBQOC*UbQ?_AUzvji+LYrq<_1#B^Uz#el199R};5KIB5 zfjPkl=Jy%F@}+@czJf=+0*$o93MDqt^`#NY;3Q)mtB5ZVG=LVIARur2U}usyI#=m_i=E~h`^1CuTt$8#)VHU~YWjs&g`xMkfJb;uI12v*LO^&L{tpYU3(vs+pzww; z3ja^)$od?}dQ4Z=Asy=Hf%*kq>LWVTV?cdemwH%-dK{=Hbg7T(PSuJQPXhI{F7=2G^-DnQ)1`h^hk6F6Pw7&R>QJ8s>RDat=X9w3 zKs~2ReN2b?3{bzUOZ_~Iydm+3I4m9&pAw%IpAkpIXT?$RIq{hI{JgVbEWRMT;%D4v zLvENt#?DDH358`|T8hh|MSea(c=>|JC&J<6LMR?y>X(-mM2Yu{k`zhA`KejH_npIT zkKI0p`6E1DXW|i=Pw~f-^L!ls$M}Q%arpP!3si{ajSG;~J?8Pl-}CCOdi&Si= znqTB!AK}N&@~^+Zle3iq*k4Qv=VM}A2K`TjVzCgP>IXdl87l|LdI_M16R{X58VV{=n8zOm{4 zmu4os)1H{%9sw;5^5ejkhn@wd5_BmMLjvttXn}=9BrfyuP)tNtabW-(VxXXJazO~m zA|H_@Xf4|5v{BFuuwBtO2nZu2p$Wr@xGXNp?q~To!_Yo&@)3y-@q!38l?=-XG6HN6 zNlL~*Y+y-Ql_Us3XPk?~1(Z+Z7evy3j)2WwpnN0oByABsB=K)9MxfRFkvBb5wXtZF zSItsf42ui0YJedk^3h0K3=zH;OtG&hK3}X)>f_N&B+5P%iAUn+Rn;ztF}J5+#@H&L z1n^46K~I@P!m=oM?0>*H&dn;0P#ijeN+!7tiVYeo6pn@@Nioew#HiplDcl6mDBN^J zk`?RB0`@>Cs+i`I3sF%q!C*&x(Rl@XZ$3jw780z;$71x%tj zU=gi?6M{poY8tiCd`nHf9r7CmdriKB<~wTg8-xaM3oga-QfToMSl#lZUyMZvv=ZOz zvJ0w`-$1H z32!jqot+^lB*7-VVXFeFyO4CwrS?S8#^+_d~@p> z!`j>wWXA5bbYAs*>ZN}$?PKt|4gM?l(924aW34!(@p$c_l zh5Hatn?+%1AF4WIhwq0+`XzvL>6hnDWw}%L9qs9fyuCF&e&5u*W-yrctT9FKz{r?e z-hV^QwL%(G?O3jYit_d~wVX47H55Uq95WgyeX)olY067fw5_S+VUV|UacYWPKLCjj zs@%C?6YLpgo)xU`I|E#XS!4qy81fFq>YtkR5|SXxNBndGO%hQ6&nkxB2JaLLg)hMD z#*2u-zZ*e+z(X6Ki;6Iz38KfRaQLqnVbW5JG3mTwTu4Y8oy8gGbvgmzuf11k@XIE?Hze}} zW!qp!h=cyS6~=8M1CSn4}~`9BA(7OM^k2xFH0Zug0?lgLHlm1|@WW;Bxr1 zYOo{ly4+msG*6My6l6;a0RAt{i_SCvi&b-`%m2Uf7|>UOu+qZ_#eB!n^)5XIQMd{^Oc(EldXpgl;2dy}5j0QIgP<1yDx^3I`i8}56k3HP=vXA|`WIBSJ&1~65)1qQ zK+)na&mGHh$JRK`^csuf=KDfb7pz6Gd4p$sCw()o_!NsbI5s^s=2w~^&krw?bKcqD z#O%x|#pw-B%$zws?F~-OdcBI-8=UrzomA}J;HlY}xtZ~qX~pFYj!(}3nQvw;==Dt~ z4xj9-eh{{KfuBGxs@bdO~ep#L(0Z4gfE99p~C|?Pp-P ziblbJmLM2G5>DYD!k(j3io(WycepBn6jv}<5h%kXN;-1@TagOW{TMX8NcY7V3}DW+2p|Icl3J#$Mv3L8?`b3XD4kXK6=z&r#v zj3t~@wbD7#C(Nk zOs5@;&<-4J2b^il3g?G45qTY%qC?y;_uxvs2PcrYT)#;|h>YMpc-Cv1#F?H-PhFnM zb4}^#^z>zT($lKMNc8v;&%zS5EHOEU;vm=h(xTlH1eY-(AfSN;X4RMFk6OHKDlV&Q zkd0mHOsYbdZTon&{m%CB9*^g&VpW$MqEuhF3n&hP58zqHcu#9xeOV6g9EFfjMMr|~ zE4p{FAUcTv7xET>`l7|K7{L`x;Mi0v$E@#Jxd}~cj&_*BZqgzNtO&u+;i=;d3dV&d zrpkl33M(syxg{FBD%`n5BB}}4IY2R@FFVN6)e6Akm0~JaDcZFNfhD(}k+s;!t8mp| z8)~r4MO+9~AP^~^;sEbjZ0n}jy)uR`g)7CpRpP4+fEHS-@JivB77yfXE^T zTsLTOe!{xBE_Fi9kFNMd=8+AM7LLw^QE&;5)VaKVo3*(ub+h|4> z5V+DPm2M%qZHhf2MdA>-!sY;-r06_AyPx`8#TJo*>P8NE0|X{#0Vs`Q60Fg2FNKE4 z5SLtpY#NuSYe4cY;v)DQ3w{OwR(+P{mF`c@Avshz3}lQ;3YWmX z4|_0g(F0%1ny6aMXorgStw!&rBG($d56Kvi6)sKvhR3QOC%D43`QY|x3=cbC2z}%+ zNStI?FuoLXwgb)Z5_`#zVl_roIkvnVF+HQOqaTV&$2_HiZ$K8hY4dyL_b`OByT;-EhP%t&9lXKb zI&z!+;;EZYT}!F?m5`3HKdF8s1+tMJ1JGziegZk0>hrfq^A`xPhc?cLJ&qk0|%Un6_bpc$#fzoi;w~CkcO)0ISTHOk|DSQj|6=SZK*mq zf6mgmYU!lz@SdyX!{im%{i|__?t8A*m9dY#*N@y_Z<;?H{d_d%>Rom9X05$j$9*kl z*}ZDnja7PC@SfM()sFj?{mu@l+^+FefSu#3o#Q#z#Hwo|Yn@PQ`CgRhgNN_30N~Eq zkFMH}X1SxP4?YadQDY?3``(5&+Jg7pTA*NuT@L20lD~$%kFA6PFFl$szN8(n6(NJX zd6;1aZ-F~9+;t;t<6_EGRof;31@7N$!SA(I`npO#TjNP9J(+ovFvSAfT^Oe<<4Tm@ zV0+0^(6P%#IQb$;NEJuaX-KO9#><$(^_gN?SP05X<=}$G9*PBWaXiwIq>d^B4Kfri zD$dK58|&n!$P2-5;gS9YKyh$YL=W5YuJ+73HG^em-qp1d`Z%0PWl~vdms(yT<4nEx zTx~0-KlXpPd}TSq-E*`f^7Y}IqkGlS4I{|5JKwr%MP7Lpf0>DV%eJhm2kz^`H=1v@ zeme5`i29zj_Ehm^O*`+owyj+JSo$z^h1RVTtZ2pv&f;{8?ATg_vb8bNCm1%1MYJ{o zHfpT0(NdgIjd>lG{+elwkvESG`ULLJB0)uTAh$r<7OwfKgAwAblDvYhDylIExIb#X z1bd`6N)b$vFaE=JGe$S1C53);gOfkBvJH1>1v_oS@&+vlSxwqhOzG7lGQg@^n5(|nc5|4{S8+lMZ2!4n1 zTQ`~I>o0naI|gAKBD4{dVxX5lH1aCszSB zO|CXgW=#2(wydig?rSFXAEC9IuDCXv?Mn;D`UkJ-E-O89rpv5C97{Ljz@|#nmChf6 zuce@Pk^BN${NJ$E9ROgf-_fwb{`6@2B{d9%ywX*e_1X1N$g00pNk9EDe$8pUSHL8g zVC&9|bbPT;i@|9p=Ta=C|I>|{3;UT zGJqmfZ$f^K1ql8F9_bkX>5AWduDI#f#a|n~y)D~yIM;P}wd-(tJj)$c?_4pV24Bbv zt-f@Xng+MQv`rI$9cTC^wQ~Q~f;0YfL?(X)*yIKRJk#*O=}whi^r(X>hYLKl@^(!9 zvIzbY64G7(8kM@bQTT54&J`0XJ(AWJz86Zg!k4$p1DwFYn`snq1T*xZMKQq#EQzps zAWNf?Ds}GEs6#cOI#sE26Sxut{{xTI2SB4vaUVUerx%j{AbN2V@SzrLCgT@eu)i)= zcN4hA3FOuu;f#XMI`=yeS8sjt=~l>BkEN@j-!Sa2essukXB)Ew<# zjt<2#Ey`3|bSvdgWT^7wYs~v=1XV^_w=@3+5fN;_Bb@-CRljholP}q2sU1oQy#_(f z^&4c1Bhcs*-z7`HO%3)RMYV4b8-Wof+4b6yRy-5ZlOM_J%dcan6^A#_d1mN53++5B zbe>It?e(}Yr_KllaY40MBYfZZNd5I2R0@F&l&WK{MWr}b`egd#<&(O81o_n0Zi~HR z!owa_C-QeF;iL4=w}^nbgdFFd0kB=4k;9IqeSSvx$j6eba zxeJ)4Zk*;~sumY#wOU-7YgQwC$`?5H9e}a=M`4IyA;E244;3R@+1TP`*AvlfT41xfHAc7DA?ZQ(%f1_=Q%>kQh zzNtC&OpWd&)1~XrknR@6@6s0E~t`bn>UuB%M~M_oe=iIu|;|sPQNqj?}7H zaKk#PesFk<{4+2F`(mU|p&i$ZEX%H$n^0c`0{E!W&{0CQ*5lwn4%GlTIFN&*l7j=jtE`d1z&5}~ zm^I)5<~>AE=73m#5-kjDGs;j6P=;odp}A6q=6W*J5>tj-;J~u|*pk%%Te2TpvcD_? zV%2HMT4Ks@OB@=Jq#7WHMwFqkQiev5!RpNTSN2`wu0?KlW}Q#2T87eG-ek`VL#F9k zGV9p4YTBPR+_yBOlb7Fp|J^jVX123O))+0=;b5OyW3+&8Ks+tjrA46>J6W~`g{}k* z^~`J#d!!m*2MuBu50+I!th#0fUlX%zHNeK%gN?JN%mK0LbdUjwYXQmt8~~I#AXXh2 zYKbYsEpRZR47K0^<~>AEmI1Nqw4@0+)Pe_?_Ygsu17bDR>x;*2hgt=wQd`jC@muoo zIXu1=kI%u3y;%z$VBSLn<=#ZB7Inz?TpPZz?>2Y){9P&UY+3Qb>w(+*?iyhtZae~m N!8)Ag@JClz{|~C#A$R}) literal 0 HcmV?d00001 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"