Merge branch 'main' into phase-0/wiki-and-machine-docs

Author: hyperpolymath

.github/copilot-instructions.md

@@ -33,7 +33,7 @@
 
 ## Banned Languages
 
-- No TypeScript (use ReScript)
+- No TypeScript (use AffineScript)
 - No Node.js / npm / bun (use Deno)
 - No Go (use Rust)
 - No Python (use Julia or Rust)

.github/workflows/dogfood-gate.yml

@@ -143,7 +143,7 @@ jobs:
             -not -path '*/.deno/*' -not -path '*/target/*' \
             -not -path '*/_build/*' -not -path '*/deps/*' \
             -not -path '*/external_corpora/*' -not -path '*/.lake/*' \
-            -type f \( -name '*.rs' -o -name '*.ex' -o -name '*.exs' -o -name '*.res' \
+            -type f \( -name '*.rs' -o -name '*.ex' -o -name '*.exs' -o -name '*.affine' \
               -o -name '*.js' -o -name '*.ts' -o -name '*.json' -o -name '*.toml' \
               -o -name '*.yml' -o -name '*.yaml' -o -name '*.md' -o -name '*.adoc' \
               -o -name '*.idr' -o -name '*.zig' -o -name '*.v' -o -name '*.jl' \
@@ -213,7 +213,7 @@ jobs:
           fi
 
           # Check for Groove endpoint code (Rust, Elixir, Zig, V)
-          if grep -rl 'well-known/groove' --include='*.rs' --include='*.ex' --include='*.zig' --include='*.v' --include='*.res' . 2>/dev/null | head -1 | grep -q .; then
+          if grep -rl 'well-known/groove' --include='*.rs' --include='*.ex' --include='*.zig' --include='*.v' --include='*.affine' . 2>/dev/null | head -1 | grep -q .; then
             HAS_GROOVE_CODE="true"
           fi
 

.github/workflows/e2e.yml

@@ -5,7 +5,7 @@
 #
 # Runs on every PR and push to main. Three jobs:
 #   structural   — fast structural checks (no compiler required)
-#   smoke        — Node.js smoke test (ReScript parser + example files)
+#   smoke        — Node.js smoke test (AffineScript parser + example files)
 #   build-e2e    — Full Idris2 + Zig build then E2E
 #   cargo-verify — Cargo workspace build + test (typed-wasm-verify crate)
 name: E2E Validation
@@ -38,7 +38,7 @@ jobs:
   # Job 2: Smoke test — Node.js parser validation
   # --------------------------------------------------------------------------
   smoke:
-    name: Smoke test (Node.js ReScript parser)
+    name: Smoke test (Node.js AffineScript parser)
     runs-on: ubuntu-latest
 
     steps:
@@ -53,7 +53,7 @@ jobs:
       - name: Install npm deps (rescript build prerequisite)
         run: npm install --no-audit --no-fund --silent
 
-      - name: Build ReScript parser
+      - name: Build AffineScript parser
         run: node_modules/.bin/rescript build
 
       - name: Run smoke test

.github/workflows/hypatia-scan.yml

@@ -406,7 +406,7 @@ jobs:
             comment += `</details>\n\n`;
             comment += `*Powered by Hypatia Neurosymbolic CI/CD Intelligence*`;
 
-            github.rest.issues.createComment({
+            github.affinet.issues.createComment({
               owner: context.repo.owner,
               repo: context.repo.repo,
               issue_number: context.issue.number,

.github/workflows/rhodibot.yml

@@ -150,7 +150,7 @@ jobs:
           # --- 7. Check dangerous patterns ---
           DANGEROUS=""
           for pattern in "believe_me" "assert_total" "Admitted" "sorry" "unsafeCoerce" "Obj.magic"; do
-            count=$(grep -r "$pattern" --include='*.idr' --include='*.v' --include='*.lean' --include='*.hs' --include='*.ml' --include='*.res' . 2>/dev/null | grep -v node_modules | wc -l || echo 0)
+            count=$(grep -r "$pattern" --include='*.idr' --include='*.v' --include='*.lean' --include='*.hs' --include='*.ml' --include='*.affine' . 2>/dev/null | grep -v node_modules | wc -l || echo 0)
             if [ "$count" -gt 0 ]; then
               DANGEROUS="$DANGEROUS\n- \`$pattern\`: $count occurrences"
             fi

.hypatia-ignore

@@ -5,7 +5,7 @@
 # Honored by hyperpolymath/standards/.github/workflows/governance-reusable.yml
 # (the "Check for ReScript / Go / Python (banned language files)" step).
 #
-# ReScript exemptions: the current parser surface is written in ReScript and
+# AffineScript exemptions: the current parser surface is written in AffineScript and
 # will be replaced by a tree-sitter-derived Idris2 parser (Track A in the
 # project roadmap). Until that work lands the source must remain checked in
 # so the smoke + aspect + level tests have something to import.

CHANGELOG.md

@@ -11,7 +11,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ## [Unreleased]
 
 ### Added
-- **typed-wasm-verify** Rust crate (`crates/typed-wasm-verify/`) — post-codegen verifier for L7 (aliasing) + L10 (linearity) on emitted wasm modules. Rust port of `hyperpolymath/affinescript:lib/{tw_verify,tw_interface}.ml`. 50/50 tests pass (40 unit + 10 cross-compat integration). Replaces the ReScript verifier path which is on its way out.
+- **typed-wasm-verify** Rust crate (`crates/typed-wasm-verify/`) — post-codegen verifier for L7 (aliasing) + L10 (linearity) on emitted wasm modules. Rust port of `hyperpolymath/affinescript:lib/{tw_verify,tw_interface}.ml`. 50/50 tests pass (40 unit + 10 cross-compat integration). Replaces the AffineScript verifier path which is on its way out.
   - C1 (#19) — Scaffold: crate skeleton, public types (`OwnershipKind`, `OwnershipError`, `CrossError`, `FuncInterface`, `VerifyError`), `OWNERSHIP_SECTION_NAME` constant, stubbed entry points.
   - C2 (#20) — `affinescript.ownership` custom-section codec (parse + encode), 11 unit tests covering wire-format round-trip and OCaml-parity leniency.
   - C3 (#21) — Per-path `(min, max)` use-range analysis with a control-flow frame stack over wasmparser's operator stream. `verify_function` + `verify_from_module` implement the intra-fn L7+L10 rules. 9 algorithmic + 9 end-to-end tests.
@@ -23,4 +23,4 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - TypedQLiser plugin exists at typedqliser/src/plugins/wasm.rs (541 lines, 9 tests)
 
 ### Changed
-- Repo is now polyglot Idris2 + Zig + Rust (added a Cargo workspace at the root, `crates/typed-wasm-verify/` is its first member). ReScript files in `src/parser/*.res` remain in tree as the v1.1 surface parser, but the post-codegen verifier no longer depends on them.
+- Repo is now polyglot Idris2 + Zig + Rust (added a Cargo workspace at the root, `crates/typed-wasm-verify/` is its first member). AffineScript files in `src/parser/*.affine` remain in tree as the v1.1 surface parser, but the post-codegen verifier no longer depends on them.

EXPLAINME.adoc

@@ -30,7 +30,7 @@ L11 and L12 are formally specified in `src/abi/TypedWasm/ABI/Tropical.idr` (L11:
 
 **From README**:
 ____
-When Module A (compiled from Rust) shares memory with Module B (compiled from ReScript), **neither source-level type system can verify the boundary.**
+When Module A (compiled from Rust) shares memory with Module B (compiled from AffineScript), **neither source-level type system can verify the boundary.**
 
 typed-wasm declares the shared schema once. Both modules import it. The typed-wasm checker verifies structural agreement at compile time, before any module runs.
 ____

Justfile

@@ -59,29 +59,29 @@ init:
 # BUILD & COMPILE
 # ═══════════════════════════════════════════════════════════════════════════════
 
-# Build the project — ReScript parser + Zig FFI
+# Build the project — AffineScript parser + Zig FFI
 build *args:
     @echo "Building {{project}}..."
-    rescript build
+    affinescript build
     cd ffi/zig && zig build
     @echo "Build complete"
 
 # Build in release mode with optimizations
 build-release *args:
     @echo "Building {{project}} (release)..."
-    rescript build
+    affinescript build
     cd ffi/zig && zig build -Doptimize=ReleaseFast
     @echo "Release build complete"
 
 # Build and watch for changes
 build-watch:
     @echo "Watching for changes..."
-    find src -name '*.res' | entr -c just build
+    find src -name '*.affine' | entr -c just build
 
 # Clean build artifacts [reversible: rebuild with `just build`]
 clean:
     @echo "Cleaning..."
-    rescript clean
+    affinescript clean
     rm -rf lib/bs lib/ocaml
     rm -rf ffi/zig/zig-out ffi/zig/.zig-cache
     rm -rf src/abi/build
@@ -94,10 +94,10 @@ clean-all: clean
 # TEST & QUALITY
 # ═══════════════════════════════════════════════════════════════════════════════
 
-# Run all tests — ReScript parser tests + Zig FFI tests
+# Run all tests — AffineScript parser tests + Zig FFI tests
 test *args:
-    @echo "Running ReScript parser tests..."
-    rescript build
+    @echo "Running AffineScript parser tests..."
+    affinescript build
     node tests/parser/ParserTests.mjs
     @echo ""
     @echo "Running contract tests..."
@@ -126,15 +126,15 @@ test *args:
 # Run tests with verbose output
 test-verbose:
     @echo "Running all tests (verbose)..."
-    rescript build
+    affinescript build
     node tests/parser/ParserTests.mjs
     cd ffi/zig && zig build test
     node tests/smoke/e2e-smoke.mjs
 
 # End-to-end smoke test — parse example, verify ABI correspondence
 test-smoke:
     @echo "Running E2E smoke test..."
-    rescript build
+    affinescript build
     node tests/smoke/e2e-smoke.mjs
 
 # ABI contract tests
@@ -145,7 +145,7 @@ test-contract:
 # End-to-end test surface
 test-e2e:
     @echo "Running end-to-end tests..."
-    rescript build
+    affinescript build
     node tests/smoke/e2e-smoke.mjs
     node tests/e2e/e2e-driver.mjs
 
@@ -168,7 +168,7 @@ test-proof:
 # Parser benchmark surface
 bench:
     @echo "Running parser benchmark..."
-    rescript build
+    affinescript build
     node benchmarks/parser-bench.mjs
 
 # Type-check Idris2 ABI modules (formal proofs)
@@ -192,19 +192,19 @@ fix: fmt
 # Format all source files [reversible: git checkout]
 fmt:
     @echo "Formatting source files..."
-    npx rescript format
+    affinescript format
     zig fmt ffi/zig/build.zig ffi/zig/src/main.zig ffi/zig/test/integration_test.zig ffi/zig/test/echidna_oracle_test.zig >/dev/null
 
 # Check formatting without changes
 fmt-check:
     @echo "Checking formatting..."
-    npx rescript format --check
+    affinescript format --check
     zig fmt --check ffi/zig/build.zig ffi/zig/src/main.zig ffi/zig/test/integration_test.zig ffi/zig/test/echidna_oracle_test.zig
 
 # Run linter
 lint:
-    @echo "Linting ReScript sources with warnings-as-errors..."
-    npx rescript build --warn-error "+3+4+45+102"
+    @echo "Linting AffineScript sources with warnings-as-errors..."
+    npx affinescript build --warn-error "+3+4+45+102"
 
 # ═══════════════════════════════════════════════════════════════════════════════
 # RUN & EXECUTE
@@ -580,11 +580,11 @@ release-tag version:
 
 # Count lines of code
 loc:
-    @find . \( -name "*.rs" -o -name "*.ex" -o -name "*.exs" -o -name "*.res" -o -name "*.gleam" -o -name "*.zig" -o -name "*.idr" -o -name "*.hs" -o -name "*.ncl" -o -name "*.scm" -o -name "*.adb" -o -name "*.ads" \) -not -path './target/*' -not -path './_build/*' 2>/dev/null | xargs wc -l 2>/dev/null | tail -1 || echo "0"
+    @find . \( -name "*.rs" -o -name "*.ex" -o -name "*.exs" -o -name "*.affine" -o -name "*.gleam" -o -name "*.zig" -o -name "*.idr" -o -name "*.hs" -o -name "*.ncl" -o -name "*.scm" -o -name "*.adb" -o -name "*.ads" \) -not -path './target/*' -not -path './_build/*' 2>/dev/null | xargs wc -l 2>/dev/null | tail -1 || echo "0"
 
 # Show TODO comments
 todos:
-    @grep -rn "TODO\|FIXME\|HACK\|XXX" --include="*.rs" --include="*.ex" --include="*.res" --include="*.gleam" --include="*.zig" --include="*.idr" --include="*.hs" . 2>/dev/null || echo "No TODOs"
+    @grep -rn "TODO\|FIXME\|HACK\|XXX" --include="*.rs" --include="*.ex" --include="*.affine" --include="*.gleam" --include="*.zig" --include="*.idr" --include="*.hs" . 2>/dev/null || echo "No TODOs"
 
 # Open in editor
 edit:
@@ -606,7 +606,7 @@ doctor:
     @command -v just >/dev/null 2>&1 && echo "  [OK] just" || echo "  [FAIL] just not found"
     @command -v git >/dev/null 2>&1 && echo "  [OK] git" || echo "  [FAIL] git not found"
     @echo "Checking for hardcoded paths..."
-    @grep -rn '$HOME\|$ECLIPSE_DIR' --include='*.rs' --include='*.ex' --include='*.res' --include='*.gleam' --include='*.sh' . 2>/dev/null | head -5 || echo "  [OK] No hardcoded paths"
+    @grep -rn '$HOME\|$ECLIPSE_DIR' --include='*.rs' --include='*.ex' --include='*.affine' --include='*.gleam' --include='*.sh' . 2>/dev/null | head -5 || echo "  [OK] No hardcoded paths"
     @echo "Diagnostics complete."
 
 # Auto-repair common issues

LEVEL-STATUS.md

@@ -28,12 +28,12 @@ natural home for "striation is cheaper" proofs once it lands.
 
 | Feature | Grammar | AST | Lexer | Parser | Checker | Tests |
 |---------|---------|-----|-------|--------|---------|-------|
-| `const` top-level | spec/grammar.ebnf | Ast.ConstDecl | Const | **DONE** parseConstDecl (Parser.res:2088) | Checker.constValueIsLiteral | **DONE** |
-| `match` on union | spec/grammar.ebnf | Ast.MatchStmt | Match | **DONE** (Parser.res:1191) | Checker.matchIsExhaustive | **DONE** |
-| Block-expr `if` | spec/grammar.ebnf | Ast.BlockIfExpr | Yield | **DONE** (Parser.res:529) | Checker.blockIfBranchesAgree | **DONE** |
-| Split `effects` | spec/grammar.ebnf | functionDecl.caps | (contextual) | **DONE** parseEffectsClause (Parser.res:1554) | (opaque until L15) | **DONE** |
+| `const` top-level | spec/grammar.ebnf | Ast.ConstDecl | Const | **DONE** parseConstDecl (Parser.affine:2088) | Checker.constValueIsLiteral | **DONE** |
+| `match` on union | spec/grammar.ebnf | Ast.MatchStmt | Match | **DONE** (Parser.affine:1191) | Checker.matchIsExhaustive | **DONE** |
+| Block-expr `if` | spec/grammar.ebnf | Ast.BlockIfExpr | Yield | **DONE** (Parser.affine:529) | Checker.blockIfBranchesAgree | **DONE** |
+| Split `effects` | spec/grammar.ebnf | functionDecl.caps | (contextual) | **DONE** parseEffectsClause (Parser.affine:1554) | (opaque until L15) | **DONE** |
 | `striated` regions | spec/grammar.ebnf | regionDecl.layout | Striated | **DONE** | Checker.striatedLayoutIsWellFormed | **DONE** |
-| Reserved keywords (L13-L16) | spec/L13-L16-reserved-syntax.adoc | — | contextual (per-block) | **DONE** (Parser.res:2685-2718) | — | **DONE** (v1.4/v1.5 rejection tests) |
+| Reserved keywords (L13-L16) | spec/L13-L16-reserved-syntax.adoc | — | contextual (per-block) | **DONE** (Parser.affine:2685-2718) | — | **DONE** (v1.4/v1.5 rejection tests) |
 
 **v1.1 surface sugar fully landed: parser, checker, tests all live.
 88/88 parser tests pass (verified 2026-04-18). LEVEL-STATUS table was stale
@@ -96,7 +96,7 @@ toolchain remains future work.
 | Effects.idr | 0 | 0 | 0 | In package |
 | Lifetime.idr | 0 | 0 | 0 | In package |
 | Linear.idr | 0 | 0 | 0 | In package |
-| MultiModule.idr | 0 | 0 | 0 | In package.  Flagship no-spoofing theorem proven A6 (2026-04-18): `FieldMatches`, `SchemaSub` preorder (`schemaSubRefl`, `schemaSubTrans`), `ModuleCompat` indexed on modules + schemas (`compatRefl`, `compatTrans`), and the flagship `noSpoofing : ModuleCompat from to imp exp -> FieldMatches f imp -> FieldMatches f exp`.  Worked Rust-exports / ReScript-imports example (4-field export, 2-field import subset) constructs a live certificate and applies the theorem. |
+| MultiModule.idr | 0 | 0 | 0 | In package.  Flagship no-spoofing theorem proven A6 (2026-04-18): `FieldMatches`, `SchemaSub` preorder (`schemaSubRefl`, `schemaSubTrans`), `ModuleCompat` indexed on modules + schemas (`compatRefl`, `compatTrans`), and the flagship `noSpoofing : ModuleCompat from to imp exp -> FieldMatches f imp -> FieldMatches f exp`.  Worked Rust-exports / AffineScript-imports example (4-field export, 2-field import subset) constructs a live certificate and applies the theorem. |
 | ModuleIsolation.idr | 0 | 0 | 0 | In package (v1.2 / L13) |
 | SessionProtocol.idr | 0 | 0 | 0 | In package (v1.3 / L14) |
 | ResourceCapabilities.idr | 0 | 0 | 0 | In package (v1.4 / L15) |