Implement scope arrest anchor schema

.machine_read/LLM_SUPERINTENDENT.scm

@@ -0,0 +1,67 @@
+;; SPDX-License-Identifier: EUPL-1.2
+;; SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell
+;; LLM_SUPERINTENDENT.scm - Instructions for LLM assistants
+
+(define llm-superintendent
+  '((schema . "hyperpolymath.llm-superintendent/1")
+    (purpose
+      . "Guide LLM assistants working on the Ephapax codebase.")
+
+    (identity
+      . ((project . "Ephapax")
+         (pronunciation . "eff-AH-pax")
+         (etymology . "Greek ἐφάπαξ meaning 'once for all'")
+         (kind . "programming language")
+         (domain . "linear types + regions for safe memory management")
+         (primary-target . "WebAssembly (wasm32-unknown-unknown)")
+         (one-sentence
+           . "A language with a linear type system + regions that prevents UAF/leaks and targets WebAssembly.")))
+
+    (core-invariants
+      . ("Every linear value must be used exactly once."
+         "Borrows are second-class: cannot escape scope, cannot be stored."
+         "Regions scope allocations; exiting a region frees all its allocations."
+         "Copy is explicit: only unrestricted types can be copied, and copying requires `copy(e)`."
+         "The type system prevents: use-after-free, double-free, memory leaks, escaping regions."))
+
+    (implementation-stack
+      . ((rust . "Compiler implementation: lexer, parser, type checker, WASM codegen")
+         (coq . "Formal specification: typing rules, operational semantics, soundness proofs")))
+
+    (key-files
+      . (("spec/SPEC.md" . "Human-readable language specification")
+         ("formal/Syntax.v" . "Coq: AST and type definitions")
+         ("formal/Typing.v" . "Coq: Linear typing rules")
+         ("formal/Semantics.v" . "Coq: Operational semantics + soundness")
+         (".machine_read/SPEC.core.scm" . "Machine-readable core semantics")
+         (".machine_read/ROADMAP.f0.scm" . "First-pass roadmap and staged work")))
+
+    (do-not
+      . ("Do not change the core identity: linear types + regions for memory safety."
+         "Do not add implementation languages beyond Rust and Coq."
+         "Do not create Makefiles; use justfile recipes."
+         "Do not claim features exist that are not implemented."
+         "Do not weaken linearity guarantees or make copies implicit."))
+
+    (task-runner
+      . ((tool . "just")
+         (list-tasks . "just --list")
+         (run-tests . "just test")
+         (build . "just build")
+         (proofs . "just proofs")))
+
+    (semantic-authority
+      . ((executable-behavior . "Rust implementation is authoritative")
+         (formal-semantics . "Coq proofs are normative for soundness claims")
+         (human-spec . "spec/SPEC.md is the source of truth for language design")))
+
+    (conformance-testing
+      . ((location . "conformance/")
+         (structure . ((pass . "Programs that should type-check successfully")
+                       (fail . "Programs with deliberate type errors")))
+         (required-failure-cases
+           . ("double-use.eph"
+              "use-after-consume.eph"
+              "escaping-region.eph"
+              "illegal-copy.eph"
+              "borrow-escape.eph"))))))

.machine_read/ROADMAP.f0.scm

@@ -0,0 +1,105 @@
+;; SPDX-License-Identifier: EUPL-1.2
+;; SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell
+;; ROADMAP.f0.scm - First-pass (f0) roadmap and staged work
+
+(define roadmap-f0
+  '((schema . "hyperpolymath.roadmap/1")
+    (phase . "f0")
+    (phase-name . "Foundation")
+    (target-tier . "silver-now")
+
+    ;; ========================================
+    ;; F0 OBJECTIVES
+    ;; ========================================
+    (objectives
+      . ("Freeze core language semantics: linear types + regions."
+         "Establish single runnable golden path for tests and proofs."
+         "Create conformance corpus exercising all type safety properties."
+         "Resolve identity drift between README and repo description."
+         "Ensure parser exists (even if minimal) to validate syntax claims."))
+
+    ;; ========================================
+    ;; COMPLETION STATUS
+    ;; ========================================
+    (status
+      . ((core-type-system . ((status . "complete")
+                              (notes . "Linearity, regions, borrows fully designed")))
+         (formal-semantics . ((status . "complete")
+                              (notes . "Coq proofs in formal/: Syntax.v, Typing.v, Semantics.v")))
+         (lexer . ((status . "complete")
+                   (notes . "logos-based tokenizer in ephapax-lexer")))
+         (parser . ((status . "complete")
+                    (notes . "chumsky-based parser in ephapax-parser")))
+         (type-checker . ((status . "in-progress")
+                          (notes . "Core logic in ephapax-typing, needs test coverage")))
+         (wasm-codegen . ((status . "in-progress")
+                          (notes . "Basic structure in ephapax-wasm")))
+         (interpreter . ((status . "complete")
+                         (notes . "Tree-walking interpreter in ephapax-interp")))
+         (repl . ((status . "complete")
+                  (notes . "Interactive shell in ephapax-repl")))
+         (cli . ((status . "complete")
+                 (notes . "Command-line interface in ephapax-cli")))
+         (conformance-corpus . ((status . "complete")
+                                (notes . "Located in conformance/")))
+         (coq-proofs-ci . ((status . "staged")
+                           (notes . "Proofs build locally; CI integration deferred to f1")))))
+
+    ;; ========================================
+    ;; GOLDEN PATH
+    ;; ========================================
+    (golden-path
+      . ((smoke-test
+           . ((commands . ("just test" "just build"))
+              (expected . "All tests pass, release build succeeds")))
+         (proof-check
+           . ((command . "just proofs")
+              (expected . "Coq proofs compile successfully")
+              (staged-note . "Coq is optional for basic usage; proofs are normative for formal claims")))
+         (conformance
+           . ((command . "just conformance")
+              (expected . "All pass/ programs type-check; all fail/ programs are rejected")))))
+
+    ;; ========================================
+    ;; CONFORMANCE REQUIREMENTS
+    ;; ========================================
+    (conformance-requirements
+      . ((minimum-pass . 5)
+         (minimum-fail . 5)
+         (required-pass-cases
+           . ("region-basic.eph"
+              "borrow-read.eph"
+              "linear-consume.eph"
+              "pair-destruct.eph"
+              "sum-match.eph"))
+         (required-fail-cases
+           . ("double-use.eph"
+              "use-after-consume.eph"
+              "escaping-region.eph"
+              "illegal-copy.eph"
+              "borrow-escape.eph"))
+         (comprehensive-example
+           . ((file . "region-full-cycle.eph")
+              (exercises . ("region allocation" "borrow" "consume"))))))
+
+    ;; ========================================
+    ;; STAGED WORK (DEFERRED TO F1)
+    ;; ========================================
+    (staged-f1
+      . ((coq-ci . "Integrate Coq proof checks into CI pipeline")
+         (property-testing . "Add property-based tests for type checker")
+         (wasm-artifacts . "Generate and test actual WASM output")
+         (documentation-generation . "Auto-generate docs from Coq and Rust")
+         (benchmark-suite . "Performance benchmarks for compilation")))
+
+    ;; ========================================
+    ;; UPGRADE PATH
+    ;; ========================================
+    (upgrade-path
+      . ((current . "silver-now")
+         (next . "gold-after-f1")
+         (gold-requirements
+           . ("Coq proofs in CI"
+              "Property testing coverage > 80%"
+              "WASM artifacts tested in browser/wasmtime"
+              "Full conformance corpus with >20 test cases"))))))

.machine_read/SPEC.core.scm

@@ -0,0 +1,198 @@
+;; SPDX-License-Identifier: EUPL-1.2
+;; SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell
+;; SPEC.core.scm - Machine-readable core language semantics
+
+(define spec-core
+  '((schema . "hyperpolymath.spec-core/1")
+    (version . "0.1.0")
+    (status . "draft")
+
+    ;; ========================================
+    ;; LINEARITY
+    ;; ========================================
+    (linearity
+      . ((definition
+           . "A value is linear if it must be used exactly once during program execution.")
+         (annotations
+           . ((linear . "Value must be consumed exactly once")
+              (unrestricted . "Value may be used zero or more times")))
+         (linear-types
+           . ("String@r" "Functions consuming linear args" "Products with linear components"
+              "Sums with linear variants" "Region-scoped allocations"))
+         (unrestricted-types
+           . ("()" "Bool" "I32" "I64" "F32" "F64" "&T"))
+         (consumption
+           . ((variable-use . "Using a linear variable consumes it")
+              (function-application . "Passing to a function consumes the argument")
+              (pattern-match . "Matching destructures and consumes the value")
+              (explicit-drop . "drop(e) explicitly consumes the value")))
+         (invariants
+           . ("Linear values cannot be used after consumption."
+              "Linear values cannot be duplicated without explicit copy."
+              "All linear bindings must be consumed by scope exit."))))
+
+    ;; ========================================
+    ;; REGION SCOPES
+    ;; ========================================
+    (regions
+      . ((definition
+           . "A region is a lexically scoped memory arena. Allocations within a region are bulk-freed on region exit.")
+         (syntax . "region r { e }")
+         (semantics
+           . ((entry . "Push current bump pointer to region stack; introduce region name r")
+              (allocation . "String.new@r(...) allocates in region r using bump allocation")
+              (exit . "Pop bump pointer from stack, restoring previous allocation point; all allocations freed")))
+         (type-rule
+           . "region r { e } : T requires that T does not mention r (no escaping references)")
+         (invariants
+           . ("Allocations in region r cannot outlive the region scope."
+              "Type checker rejects any attempt to return a region-scoped value."
+              "Regions cannot be first-class values; they are purely lexical."))))
+
+    ;; ========================================
+    ;; SECOND-CLASS BORROWS
+    ;; ========================================
+    (borrows
+      . ((definition
+           . "A borrow &e provides temporary read-only access to a value without transferring ownership.")
+         (syntax . "&e")
+         (type . "&T")
+         (second-class-restrictions
+           . ("Cannot be stored in data structures (pairs, sums)."
+              "Cannot be returned from functions."
+              "Cannot escape the lexical scope where created."
+              "Cannot be assigned to let bindings that outlive the borrowed expression."))
+         (typing
+           . "R; Γ ⊢ &x : &T ⊣ Γ  (borrow does not consume x)")
+         (use-cases
+           . ("String.len(&s) -- read length without consuming string"
+              "Comparison functions -- compare without consuming"
+              "Inspection operations -- examine without ownership transfer"))
+         (invariants
+           . ("Original value remains linear and must still be consumed elsewhere."
+              "Borrow lifetime is strictly nested within original value's lifetime."))))
+
+    ;; ========================================
+    ;; EXPLICIT COPY RULES
+    ;; ========================================
+    (explicit-copy
+      . ((definition
+           . "Duplication of values requires explicit syntax; there is no implicit copying.")
+         (syntax . "copy(e)")
+         (applicability
+           . "Only unrestricted types may be copied: (), Bool, I32, I64, F32, F64")
+         (linear-types
+           . "Linear types cannot be copied. Attempting copy(linear_val) is a type error.")
+         (semantics
+           . "copy(e) evaluates e and produces a fresh copy of the value, leaving original unconsumed.")
+         (rationale
+           . ("Prevents accidental duplication of resources."
+              "Makes resource flow explicit in source code."
+              "Aligns with linear logic where contraction (copying) is controlled."))
+         (invariants
+           . ("copy(e) where e : T requires unrestricted(T)."
+              "The original value and the copy are independent."))))
+
+    ;; ========================================
+    ;; TYPING JUDGEMENT
+    ;; ========================================
+    (typing-judgement
+      . ((form . "R; Γ ⊢ e : T ⊣ Γ'")
+         (components
+           . ((R . "Set of active region names")
+              (Γ . "Input typing context: list of (x : T, used) triples")
+              (e . "Expression being typed")
+              (T . "Resulting type")
+              (Γ' . "Output context with updated usage information")))
+         (context-operations
+           . ((lookup . "Γ(x) = T retrieves binding for x")
+              (mark-used . "Γ[x ↦ used] marks x as consumed")
+              (extend . "Γ, x : T adds fresh binding")
+              (all-used . "∀(x : T, used) ∈ Γ. used = true (all linear vars consumed)")))))
+
+    ;; ========================================
+    ;; KEY TYPING RULES
+    ;; ========================================
+    (typing-rules
+      . ((T-Var-Lin
+           . ((premises . ("Γ(x) = T" "linear(T)" "¬used(Γ, x)"))
+              (conclusion . "R; Γ ⊢ x : T ⊣ Γ[x ↦ used]")
+              (description . "Using a linear variable consumes it")))
+
+         (T-Var-Un
+           . ((premises . ("Γ(x) = T" "unrestricted(T)"))
+              (conclusion . "R; Γ ⊢ x : T ⊣ Γ")
+              (description . "Unrestricted variables can be used without consumption")))
+
+         (T-StringNew
+           . ((premises . ("r ∈ R"))
+              (conclusion . "R; Γ ⊢ String.new@r(s) : String@r ⊣ Γ")
+              (description . "Allocate string in active region")))
+
+         (T-StringConcat
+           . ((premises . ("R; Γ ⊢ e1 : String@r ⊣ Γ'"
+                           "R; Γ' ⊢ e2 : String@r ⊣ Γ''"))
+              (conclusion . "R; Γ ⊢ String.concat(e1, e2) : String@r ⊣ Γ''")
+              (description . "Concatenation consumes both input strings")))
+
+         (T-Region
+           . ((premises . ("r ∉ R"
+                           "R ∪ {r}; Γ ⊢ e : T ⊣ Γ'"
+                           "T does not mention r"))
+              (conclusion . "R; Γ ⊢ region r { e } : T ⊣ Γ'")
+              (description . "Region introduces fresh scope; result cannot reference region")))
+
+         (T-Borrow
+           . ((premises . ("Γ(x) = T"))
+              (conclusion . "R; Γ ⊢ &x : &T ⊣ Γ")
+              (description . "Borrow does not consume the value")))
+
+         (T-Drop
+           . ((premises . ("R; Γ ⊢ e : T ⊣ Γ'" "linear(T)"))
+              (conclusion . "R; Γ ⊢ drop(e) : () ⊣ Γ'")
+              (description . "Explicit drop consumes linear value")))
+
+         (T-Copy
+           . ((premises . ("R; Γ ⊢ e : T ⊣ Γ'" "unrestricted(T)"))
+              (conclusion . "R; Γ ⊢ copy(e) : T ⊣ Γ'")
+              (description . "Copy produces duplicate of unrestricted value")))))
+
+    ;; ========================================
+    ;; MEMORY SAFETY THEOREMS
+    ;; ========================================
+    (safety-theorems
+      . ((progress
+           . "If R; Γ ⊢ e : T ⊣ Γ' and e is not a value, then e can step.")
+         (preservation
+           . "If R; Γ ⊢ e : T ⊣ Γ' and e → e', then R; Γ'' ⊢ e' : T ⊣ Γ' for some Γ''.")
+         (linearity-soundness
+           . "If R; Γ ⊢ e : T ⊣ Γ' and e →* v, all linear bindings in Γ are consumed.")
+         (no-use-after-free
+           . "Linear types ensure resources cannot be accessed after consumption.")
+         (no-double-free
+           . "Linear types ensure resources are consumed at most once.")
+         (no-leaks
+           . "Linear types ensure resources are consumed at least once.")
+         (no-region-escape
+           . "Region-scoped types cannot outlive their region.")))
+
+    ;; ========================================
+    ;; WASM TARGET
+    ;; ========================================
+    (wasm-compilation
+      . ((target . "wasm32-unknown-unknown")
+         (memory-model
+           . ((bump-pointer . "0x0000 (4 bytes)")
+              (region-stack-pointer . "0x0004 (4 bytes)")
+              (region-stack . "0x0008 (256 bytes, 64 levels max)")
+              (heap-start . "0x0108")))
+         (type-mapping
+           . (("()" . "no value")
+              ("Bool" . "i32 (0 or 1)")
+              ("I32" . "i32")
+              ("I64" . "i64")
+              ("F32" . "f32")
+              ("F64" . "f64")
+              ("String@r" . "i32 (pointer)")
+              ("(T1, T2)" . "i32 (pointer to struct)")
+              ("T1 + T2" . "i32 (pointer to tagged union)")))))))