MVP kernel: L2 grade algebras + L1 graded checker + anytype-specific seam (Phases 2-4)

.github/workflows/idris2-proof.yml

@@ -0,0 +1,113 @@
+# SPDX-License-Identifier: MPL-2.0
+# Idris2 proof + kernel test gate — type-checks EVERY Idris2 module via
+# scripts/check-idris2-proofs.sh (the same script `just proof-check-idris2`
+# runs, so local green and CI green mean the same thing), then builds the
+# kernel and runs the golden matrix (the same pipeline as `just test`).
+#
+# This is the first workflow in this repository that checks any Idris2 at
+# all: the other workflows validate repo shape and run security scanners,
+# and the recipe this gate replaces (build/just/proofs.just) exited 0 when
+# the prover was absent. The script fails when idris2 is missing rather
+# than skipping, so a broken install step can never render as a green
+# proof run.
+#
+# Adapted from ideas-to-alphas .github/workflows/idris2-proof.yml, which
+# documents the estate history behind each rule.
+name: Idris2 Proof
+
+on:
+  push:
+    branches: [main]
+    paths:
+      - '**.idr'
+      - '*.ipkg'
+      - 'scripts/check-idris2-proofs.sh'
+      - 'scripts/check-cli.sh'
+      - 'src/interface/ffi/**'
+      - '.github/workflows/idris2-proof.yml'
+  pull_request:
+    paths:
+      - '**.idr'
+      - '*.ipkg'
+      - 'scripts/check-idris2-proofs.sh'
+      - 'scripts/check-cli.sh'
+      - 'src/interface/ffi/**'
+      - '.github/workflows/idris2-proof.yml'
+  workflow_dispatch:
+
+# Estate guardrail: one run per ref, cancel superseded runs. Read-only check.
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+env:
+  IDRIS2_VERSION: "0.7.0"
+
+jobs:
+  idris2-check:
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+    permissions:
+      contents: read
+    steps:
+      - name: Checkout
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+
+      - name: Install Chez Scheme (Idris2 backend)
+        run: |
+          set -euo pipefail
+          sudo apt-get update -qq
+          sudo apt-get install -y --no-install-recommends chezscheme libgmp-dev
+
+      - name: Build & install Idris2 ${{ env.IDRIS2_VERSION }}
+        run: |
+          set -euo pipefail
+          # Build OUTSIDE the checkout. The proof gate sweeps the working tree
+          # for every *.idr and errors on any not in its manifest -- that
+          # breadth is the point. The Idris2 source tarball ships hundreds of
+          # .idr files; extracting it into the checkout makes the gate fail on
+          # the compiler's own sources. Keep the tree the gate scans clean.
+          build_dir="$(mktemp -d)"
+          cd "$build_dir"
+          tarball="idris2-${IDRIS2_VERSION}.tar.gz"
+          curl -fsSL -o "$tarball" \
+            "https://codeload.github.com/idris-lang/Idris2/tar.gz/refs/tags/v${IDRIS2_VERSION}"
+          tar xzf "$tarball"
+          cd "Idris2-${IDRIS2_VERSION}"
+          make bootstrap SCHEME=chezscheme
+          make install SCHEME=chezscheme
+          echo "${HOME}/.idris2/bin" >> "$GITHUB_PATH"
+
+      - name: Build kernel, run golden matrix and seam tests
+        # Runs first so the anytype/anytype-abi packages are installed before
+        # the proof sweep checks modules that use -p flags.
+        run: |
+          set -euo pipefail
+          idris2 --install anytype.ipkg
+          idris2 --install abi.ipkg
+          idris2 --build anytype-tests.ipkg
+          ./build/exec/anytype-tests
+          idris2 --build anytype-cli.ipkg
+          ./scripts/check-cli.sh
+
+      - name: Type-check every Idris2 module
+        run: ./scripts/check-idris2-proofs.sh
+
+      - name: Install Zig 0.16.0 (checksum-pinned)
+        run: |
+          set -euo pipefail
+          cd "$(mktemp -d)"
+          curl -fsSL -o zig.tar.xz \
+            "https://ziglang.org/download/0.16.0/zig-x86_64-linux-0.16.0.tar.xz"
+          echo "70e49664a74374b48b51e6f3fdfbf437f6395d42509050588bd49abe52ba3d00  zig.tar.xz" | sha256sum -c -
+          tar xJf zig.tar.xz
+          echo "$PWD/zig-x86_64-linux-0.16.0" >> "$GITHUB_PATH"
+
+      - name: Zig seam tests (comptime layout asserts + kernel round trip)
+        run: |
+          set -euo pipefail
+          cd src/interface/ffi
+          zig build test --summary all

.gitignore

@@ -109,17 +109,10 @@ deps/
 build/
 dist/
 
-# /build/ is a tracked config directory (build orchestration: contractile.just,
-# guix.scm, just/*.just, etc.) introduced in chore/root-cleanup. Whitelist
-# root-level /build/ so its contents are tracked. The blanket `build/` rule
-# above still ignores any nested `build/` directories (e.g. Rust crate
-# target/build/) — only the root-level path is exempt.
-!/build/
-!/build/**
-
-# ...but never track Idris2 typecheck output. `idris2 --typecheck abi.ipkg`
-# writes compiled .ttc/.ttm under build/ttc/; these are generated artifacts.
-/build/ttc/
+# build/ is generated output only (Idris2 .ttc/.ttm and executables, Zig
+# artifacts). The old tracked build/ config directory (contractile.just,
+# guix.scm, just/*.just) was removed with the fake-gate recipes; nothing
+# under build/ is source any more.
 
 # Arrival-pack build artifact (regenerated from a2ml)
 .machine_readable/arrival-pack/claude-md-data.json

.machine_readable/6a2/STATE.a2ml

@@ -6,25 +6,25 @@
 [metadata]
 project = "anytype"
 version = "0.1.0"
-last-updated = "2026-06-28"
+last-updated = "2026-07-21"
 status = "active"  # active | paused | archived
 
 [project-context]
 name = "anytype"
 purpose = "Reference kernel for systemet (Equality Theory): a parameterised checker whose discipline is the chosen L2 grade algebra. Implementation side of the systemet/anytype split."
-completion-percentage = 10
+completion-percentage = 40
 
 [position]
-phase = "design"           # design | implementation | testing | maintenance | archived
+phase = "implementation"   # design | implementation | testing | maintenance | archived
 maturity = "experimental"  # experimental | alpha | beta | production | lts
 
 [route-to-mvp]
 milestones = [
   { name = "Phase 0: Split kernel out of the EveryType draft; instantiate RSR repo", completion = 100 },
   { name = "Phase 1: Design write-up (pluggable grades, L1 conversion, gates)", completion = 80 },
-  { name = "Phase 2: L2 grade-algebra interface + first concrete grade (affine)", completion = 0 },
-  { name = "Phase 3: L1 conversion checker + totality gate", completion = 0 },
-  { name = "Phase 4: anytype-specific typed ABI/FFI seam (replace template seam)", completion = 0 },
+  { name = "Phase 2: L2 grade-algebra interface + first concrete grade (affine)", completion = 100 },
+  { name = "Phase 3: L1 conversion checker + totality gate", completion = 100 },
+  { name = "Phase 4: anytype-specific typed ABI/FFI seam (replace template seam)", completion = 100 },
   { name = "Phase 5: L3 guarded recursion; L0 lowering target", completion = 0 },
   { name = "Phase 6: L4 effect handlers + TEA-erasure (gated on systemet OPEN-A)", completion = 0 },
 ]
@@ -34,10 +34,11 @@ milestones = [
 
 [critical-next-actions]
 actions = [
-  "Define the L2 grade-algebra interface against systemet's stated laws.",
-  "Implement the L1 conversion checker (normalize + compare) and the totality gate.",
-  "Replace the template ABI/FFI seam with an anytype-specific one.",
-  "Keep README/EXPLAINME inside what is built; no 'usable checker' claim until it exists.",
+  "Add branching to L1: needs a join (least upper bound) on grades beyond the semiring+order laws -- design the extension against systemet first.",
+  "L3 guarded recursion (Phase 5), then L0 lowering target.",
+  "In-process seam: link the kernel via the RefC backend instead of spawning anytype-check.",
+  "Decide the fate of the five quarantined RSR template proof modules (fix or delete; tracked in scripts/check-idris2-proofs.sh MANIFEST).",
+  "Keep README/EXPLAINME inside what is built; the MVP claim is 'distinct disciplines from one rule set', not 'usable general-purpose checker'.",
 ]
 
 [maintenance-status]

.machine_readable/6a2/anchors/ANCHOR.a2ml

@@ -29,6 +29,9 @@ domain = "programming-language implementation / type checkers"
 semantic-authority = "hyperpolymath/systemet"
 relationship = "implements"
 pin-required = true
+# Discharged 2026-07-21: the systemet commit this kernel implements.
+pinned-commit = "ba5930dc478c80b1f968eea4ca28acd0f9d67966"
+pinned-date = "2026-07-18"
 extend-not-redefine = true
 
 [semantic-authority]

.tool-versions

@@ -1,10 +1,3 @@
-# Uncomment and customize for your project
-# rust nightly
-# just 1.40.0
-# nickel 1.10.0
-# gleam 1.8.0
-# elixir 1.18.0
-# erlang 27.2
-# zig 0.14.0
-# idris2 0.7.0
 rust nightly
+idris2 0.7.0
+zig 0.16.0

AFFIRMATION.adoc

@@ -35,14 +35,17 @@ file is a draft.
 
 == What we do NOT claim
 
-* *There is no working type checker yet.* `src/`, `tests/`, and `verification/proofs/`
-  are RSR *scaffolding* inherited from the template, not an anytype implementation.
-* *The pluggable-grade interface does not exist in code yet.* It is the first build
-  target, not a shipped feature.
-* *No layer is implemented.* The L0–L4 table in the README is intent + status, not a
-  record of working code.
+* *The kernel is an MVP cut, not a general-purpose type checker.* No dependent
+  types, no branching, no L3 recursion, no L0 lowering, no L4 effects.
+* *No soundness proof for the checker.* The grade-algebra laws are machine-checked
+  proof fields and the golden matrix is real, but progress/preservation for the
+  L1 checker is not proven.
+* *The totality gate is syntactic* (no recursion constructor in the type-index
+  language), not a termination analysis.
 * *TEA-erasure is OPEN* (in systemet) and not started here. Do not cite it.
-* *The ABI/FFI seam files are the template's*, not yet an anytype-specific ABI.
+* *The seam transport is a spawned process*, not in-process linkage; five
+  never-compiling template proof modules are quarantined in
+  `scripts/check-idris2-proofs.sh`, not fixed.
 
 == Provenance note
 

EXPLAINME.adoc

@@ -23,18 +23,28 @@ its current state*.
 
 Claim: anytype is the reference kernel for Equality Theory.
 
-Reality at this commit:
-
-* There is *no working checker yet*. `src/` contains RSR scaffolding
-  (`src/interface/Abi/*.idr`, `src/interface/ffi/*.zig`, READMEs, AI-manifests), not
-  an anytype implementation.
-* `tests/` and `verification/proofs/` are template stubs, not anytype tests/proofs.
-* What is real today: the repository *shape* (RSR), the *design* of the kernel in
-  this file and the README, and the *split* that makes systemet the theory and
-  anytype the engine.
-
-Everything below describes the *intended* mapping. Where a file does not yet exist or
-is a stub, it is named as such. The dated, signed snapshot is `AFFIRMATION.adoc`.
+Reality at this commit (2026-07-21, MVP kernel):
+
+* The kernel *exists for the MVP cut*: `src/kernel/` is a usage-counting
+  bidirectional checker for a simply-graded λ-calculus, parameterised by a
+  `GradeAlgebra` record whose ordered-semiring laws are proof fields. Two
+  instances ship — affine `{0,1,ω}` (mirroring AffineScript `lib/quantity.ml`)
+  and exact-usage `ℕ` — and the 19-case golden matrix shows the same rules
+  yielding distinct disciplines (affine accepts drop, exact rejects it).
+* The seam is anytype's own: `src/interface/Abi/` (wire types with injective
+  codes; layouts proven `CABICompliant`), the `anytype-check` CLI
+  (`src/cli/`), and the Zig `anytype_check` export (`src/interface/ffi/`)
+  with comptime asserts against the proven layouts. MVP transport is a
+  spawned process; in-process RefC linkage is future work.
+* Gates are real and hard-fail: `just test`, `just proof-check-idris2`
+  (manifest over every `.idr`; missing prover = FAIL), and CI
+  `idris2-proof.yml`. Five never-compiling template modules under
+  `verification/proofs/idris2/` are quarantined, not hidden.
+* Not built: dependent types, branching (needs a grade join beyond the
+  stated laws), L3 recursion, L0 lowering, L4 effects (TEA is open in
+  systemet), and any soundness proof for the checker itself.
+
+The dated snapshot is `AFFIRMATION.adoc`.
 
 == Pluggable grades (the L2 mechanism)
 
@@ -52,9 +62,14 @@ Division of responsibility:
 * systemet *defines the laws* a grade algebra must satisfy.
 * anytype *implements the interface and checks candidates against those laws*.
 
-Caveat:
+State:
 
-* None of this interface exists in code yet. It is the kernel's first build target.
+* Built (MVP): `src/kernel/Anytype/Grade/Algebra.idr` is the interface — a record
+  whose law fields make an unlawful algebra unrepresentable. `Affine.idr` and
+  `Exact.idr` are the first two instances. The richer grades (cost,
+  information-flow lattice, probability-like, privacy budget) remain future
+  instances; branching additionally needs a join operation the record does not
+  yet carry.
 
 == L1 equality and the totality gate
 
@@ -67,10 +82,16 @@ Intended implementation:
 * A totality checker that rejects non-terminating type-level functions, so conversion
   terminates.
 
-Caveat:
+State and caveat:
 
+* Built (MVP): `Anytype.Core.Normalise` + `Anytype.Core.Conversion`, invoked at the
+  single check/infer mode switch in `Anytype.Core.Check`. The MVP totality gate is
+  *syntactic*: the type-index language (`TNat`) has no recursion constructor, and the
+  normaliser is `%default total` — machine-checked, but a gate by construction, not a
+  termination analysis over a type-level function space (there is no type-level
+  function space yet).
 * The strength of "equality is conversion" is exactly the strength of the totality
-  checker. Any escape hatch must be recorded as an explicit unsafe boundary in
+  gate. Any escape hatch must be recorded as an explicit unsafe boundary in
   `AFFIRMATION.adoc`, never folded silently into equality. The *theorem* that this is
   sound is systemet's obligation; this repo only has to *implement the check*.
 
@@ -123,10 +144,14 @@ How this is implemented:
 * `src/interface/Abi/` holds Idris2 interface/layout descriptions; `src/interface/ffi/`
   holds the Zig FFI; `src/interface/generated/` is where generated C headers land.
 
-Caveat:
+State:
 
-* These are currently the *template's* seam files, not anytype-specific ones. They
-  demonstrate the pattern; they do not yet describe an anytype ABI.
+* Built (MVP): `Abi.Types` (discipline/verdict codes, injectivity + round-trip
+  proofs), `Abi.Layout` (`anytype_request_t`/`anytype_response_t` proven
+  `CABICompliant`), `Abi.Foreign` (the `anytype_check` contract), and the Zig side
+  comptime-asserting the same layouts. Transport is a spawned `anytype-check`
+  process; `src/interface/generated/` C headers and in-process linkage are future
+  work.
 
 == RSR integration
 

Justfile

@@ -129,26 +129,29 @@ clean-all: clean
 # TEST & QUALITY
 # ═══════════════════════════════════════════════════════════════════════════════
 
-# Run all tests
+# Hard-fails if idris2 is absent -- a gate that cannot fail is not a gate
+# (see scripts/check-idris2-proofs.sh for the history).
+# Typecheck the ABI seam, build the kernel, run the golden matrix
 test *args:
-    @echo "Running tests..."
-    # TODO: Replace with your test command
-    # Examples:
-    #   cargo test {{args}}
-    #   mix test {{args}}
-    #   zig build test {{args}}
-    #   deno test {{args}}
-    @echo "Tests passed!"
+    @command -v idris2 >/dev/null || { echo "FAIL: idris2 not on PATH (install Idris2 0.7.0)"; exit 1; }
+    idris2 --install anytype.ipkg
+    idris2 --install abi.ipkg
+    idris2 --build anytype-tests.ipkg
+    ./build/exec/anytype-tests
+    idris2 --build anytype-cli.ipkg
+    ./scripts/check-cli.sh
+    @command -v zig >/dev/null || { echo "FAIL: zig not on PATH (Zig seam tests need it)"; exit 1; }
+    cd src/interface/ffi && zig build test
 
 # Run tests with verbose output
 test-verbose:
     @echo "Running tests (verbose)..."
     # TODO: Replace with verbose test command
 
-# Smoke test
+# Smoke test: does the kernel package typecheck at all?
 test-smoke:
-    @echo "Smoke test..."
-    # TODO: Add basic sanity checks
+    @command -v idris2 >/dev/null || { echo "FAIL: idris2 not on PATH"; exit 1; }
+    idris2 --typecheck anytype.ipkg
 
 # Run end-to-end tests (full pipeline: build → run → verify)
 e2e:
@@ -593,7 +596,14 @@ help-me:
 # FORMAL VERIFICATION (PROOFS) — see build/just/proofs.just
 # ═══════════════════════════════════════════════════════════════════════════════
 
-import? "build/just/proofs.just"
+# Proof gates replace the deleted build/just/proofs.just, whose recipes
+# exited 0 when the prover was absent (the estate fake-gate flaw).
+# Type-check every Idris2 module against the MANIFEST (hard-fail gate)
+proof-check-idris2:
+    ./scripts/check-idris2-proofs.sh
+
+# Run all proof gates
+proof-check: proof-check-idris2
 
 # ═══════════════════════════════════════════════════════════════════════════════
 # SESSION MANAGEMENT (THIN BINDINGS TO CENTRAL STANDARDS)