Skip to content

Commit e32ae12

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
MVP kernel: L2 grade algebras + L1 graded checker + anytype-specific seam (Phases 2-4) (#12)
## What Implements route-to-mvp **Phases 2, 3 and 4** from STATE.a2ml — the repo's first actual kernel code — plus the honesty pass that keeps every doc inside what is built. - **L2 (Phase 2)**: `Anytype.Grade.Algebra` — a `GradeAlgebra` record whose ordered-semiring laws are *proof fields*, so an unlawful algebra is unrepresentable. Instances: affine `{0,1,ω}` (mirrors AffineScript `lib/quantity.ml` cell-for-cell, incl. the `ω·1=ω` BUG-001 rule) and exact-usage `ℕ`. - **L1 (Phase 3)**: usage-counting bidirectional checker for a simply-graded λ-calculus; the type-index language has no recursion constructor, so type-level computation is total *by construction* (syntactic totality gate, `%default total`, no `believe_me`/holes anywhere); conversion = normalise-and-compare at one site. - **Seam (Phase 4, both halves)**: `Abi.{Types,Layout,Foreign}` rewritten from template demos to anytype's wire contract (codes proven injective; request/response layouts proven `CABICompliant`); `anytype-check` CLI with a total fuel-bounded S-expression reader; Zig 0.16 `anytype_check` export with comptime layout asserts. MVP transport: spawned process (stated in the ffi README). - **Gates**: `just test` (kernel build + 19-case golden matrix + 8 seam tests + `zig build test`), `scripts/check-idris2-proofs.sh` (manifest over every `.idr`; **missing prover = FAIL**; the 5 never-compiling template proof modules are quarantined and must keep failing), and `.github/workflows/idris2-proof.yml` — the first CI in this repo that checks any Idris2. The fake exit-0 `build/just/proofs.just` recipes are deleted. - **Truth pass**: README status table + WARNING, EXPLAINME, AFFIRMATION (still an unsigned draft), STATE.a2ml (10→40%, Phases 2-4 → 100), ANCHOR.a2ml systemet pin discharged with commit `ba5930dc`, PROOF-STATUS/ROADMAP de-templated, `.tool-versions` idris2 0.7.0 + zig 0.16.0, mise.toml purged of template runtime residue. ## The headline demonstration The same rules under two algebras (golden matrix + CLI tests): ``` echo '(lam 1 bool tt)' | anytype-check --discipline affine # ACCEPT (drop ok: 0 <= 1) echo '(lam 1 bool tt)' | anytype-check --discipline exact # REJECT (0 /= 1) ``` Pick the algebra, get the discipline — now code, not prose. ## Verification - `just test`: 19/19 golden cases + 8/8 seam cases + 4/4 zig tests — green locally (Idris2 0.7.0, Zig 0.16.0). - `just proof-check-idris2`: 16 gated modules pass, 5 quarantined still fail as recorded, all 21 `.idr` files accounted for. - Every gate was **watched failing** (prover off PATH, sabotaged law proof, flipped golden expectation, kernel binary removed) before being made green. ## Out of scope (recorded in ROADMAP/STATE) Branching (needs a grade join beyond systemet's stated laws), L3 recursion, L0 lowering, L4/TEA (open in systemet), in-process RefC linkage, checker soundness proof. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
1 parent b71523e commit e32ae12

45 files changed

Lines changed: 2017 additions & 2231 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.github/workflows/idris2-proof.yml‎

Lines changed: 113 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,113 @@
1+
# SPDX-License-Identifier: MPL-2.0
2+
# Idris2 proof + kernel test gate — type-checks EVERY Idris2 module via
3+
# scripts/check-idris2-proofs.sh (the same script `just proof-check-idris2`
4+
# runs, so local green and CI green mean the same thing), then builds the
5+
# kernel and runs the golden matrix (the same pipeline as `just test`).
6+
#
7+
# This is the first workflow in this repository that checks any Idris2 at
8+
# all: the other workflows validate repo shape and run security scanners,
9+
# and the recipe this gate replaces (build/just/proofs.just) exited 0 when
10+
# the prover was absent. The script fails when idris2 is missing rather
11+
# than skipping, so a broken install step can never render as a green
12+
# proof run.
13+
#
14+
# Adapted from ideas-to-alphas .github/workflows/idris2-proof.yml, which
15+
# documents the estate history behind each rule.
16+
name: Idris2 Proof
17+
18+
on:
19+
push:
20+
branches: [main]
21+
paths:
22+
- '**.idr'
23+
- '*.ipkg'
24+
- 'scripts/check-idris2-proofs.sh'
25+
- 'scripts/check-cli.sh'
26+
- 'src/interface/ffi/**'
27+
- '.github/workflows/idris2-proof.yml'
28+
pull_request:
29+
paths:
30+
- '**.idr'
31+
- '*.ipkg'
32+
- 'scripts/check-idris2-proofs.sh'
33+
- 'scripts/check-cli.sh'
34+
- 'src/interface/ffi/**'
35+
- '.github/workflows/idris2-proof.yml'
36+
workflow_dispatch:
37+
38+
# Estate guardrail: one run per ref, cancel superseded runs. Read-only check.
39+
concurrency:
40+
group: ${{ github.workflow }}-${{ github.ref }}
41+
cancel-in-progress: true
42+
43+
permissions:
44+
contents: read
45+
46+
env:
47+
IDRIS2_VERSION: "0.7.0"
48+
49+
jobs:
50+
idris2-check:
51+
runs-on: ubuntu-latest
52+
timeout-minutes: 30
53+
permissions:
54+
contents: read
55+
steps:
56+
- name: Checkout
57+
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
58+
59+
- name: Install Chez Scheme (Idris2 backend)
60+
run: |
61+
set -euo pipefail
62+
sudo apt-get update -qq
63+
sudo apt-get install -y --no-install-recommends chezscheme libgmp-dev
64+
65+
- name: Build & install Idris2 ${{ env.IDRIS2_VERSION }}
66+
run: |
67+
set -euo pipefail
68+
# Build OUTSIDE the checkout. The proof gate sweeps the working tree
69+
# for every *.idr and errors on any not in its manifest -- that
70+
# breadth is the point. The Idris2 source tarball ships hundreds of
71+
# .idr files; extracting it into the checkout makes the gate fail on
72+
# the compiler's own sources. Keep the tree the gate scans clean.
73+
build_dir="$(mktemp -d)"
74+
cd "$build_dir"
75+
tarball="idris2-${IDRIS2_VERSION}.tar.gz"
76+
curl -fsSL -o "$tarball" \
77+
"https://codeload.github.com/idris-lang/Idris2/tar.gz/refs/tags/v${IDRIS2_VERSION}"
78+
tar xzf "$tarball"
79+
cd "Idris2-${IDRIS2_VERSION}"
80+
make bootstrap SCHEME=chezscheme
81+
make install SCHEME=chezscheme
82+
echo "${HOME}/.idris2/bin" >> "$GITHUB_PATH"
83+
84+
- name: Build kernel, run golden matrix and seam tests
85+
# Runs first so the anytype/anytype-abi packages are installed before
86+
# the proof sweep checks modules that use -p flags.
87+
run: |
88+
set -euo pipefail
89+
idris2 --install anytype.ipkg
90+
idris2 --install abi.ipkg
91+
idris2 --build anytype-tests.ipkg
92+
./build/exec/anytype-tests
93+
idris2 --build anytype-cli.ipkg
94+
./scripts/check-cli.sh
95+
96+
- name: Type-check every Idris2 module
97+
run: ./scripts/check-idris2-proofs.sh
98+
99+
- name: Install Zig 0.16.0 (checksum-pinned)
100+
run: |
101+
set -euo pipefail
102+
cd "$(mktemp -d)"
103+
curl -fsSL -o zig.tar.xz \
104+
"https://ziglang.org/download/0.16.0/zig-x86_64-linux-0.16.0.tar.xz"
105+
echo "70e49664a74374b48b51e6f3fdfbf437f6395d42509050588bd49abe52ba3d00 zig.tar.xz" | sha256sum -c -
106+
tar xJf zig.tar.xz
107+
echo "$PWD/zig-x86_64-linux-0.16.0" >> "$GITHUB_PATH"
108+
109+
- name: Zig seam tests (comptime layout asserts + kernel round trip)
110+
run: |
111+
set -euo pipefail
112+
cd src/interface/ffi
113+
zig build test --summary all

‎.gitignore‎

Lines changed: 4 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -109,17 +109,10 @@ deps/
109109
build/
110110
dist/
111111

112-
# /build/ is a tracked config directory (build orchestration: contractile.just,
113-
# guix.scm, just/*.just, etc.) introduced in chore/root-cleanup. Whitelist
114-
# root-level /build/ so its contents are tracked. The blanket `build/` rule
115-
# above still ignores any nested `build/` directories (e.g. Rust crate
116-
# target/build/) — only the root-level path is exempt.
117-
!/build/
118-
!/build/**
119-
120-
# ...but never track Idris2 typecheck output. `idris2 --typecheck abi.ipkg`
121-
# writes compiled .ttc/.ttm under build/ttc/; these are generated artifacts.
122-
/build/ttc/
112+
# build/ is generated output only (Idris2 .ttc/.ttm and executables, Zig
113+
# artifacts). The old tracked build/ config directory (contractile.just,
114+
# guix.scm, just/*.just) was removed with the fake-gate recipes; nothing
115+
# under build/ is source any more.
123116

124117
# Arrival-pack build artifact (regenerated from a2ml)
125118
.machine_readable/arrival-pack/claude-md-data.json

‎.machine_readable/6a2/STATE.a2ml‎

Lines changed: 11 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -6,25 +6,25 @@
66
[metadata]
77
project = "anytype"
88
version = "0.1.0"
9-
last-updated = "2026-06-28"
9+
last-updated = "2026-07-21"
1010
status = "active" # active | paused | archived
1111

1212
[project-context]
1313
name = "anytype"
1414
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."
15-
completion-percentage = 10
15+
completion-percentage = 40
1616

1717
[position]
18-
phase = "design" # design | implementation | testing | maintenance | archived
18+
phase = "implementation" # design | implementation | testing | maintenance | archived
1919
maturity = "experimental" # experimental | alpha | beta | production | lts
2020

2121
[route-to-mvp]
2222
milestones = [
2323
{ name = "Phase 0: Split kernel out of the EveryType draft; instantiate RSR repo", completion = 100 },
2424
{ name = "Phase 1: Design write-up (pluggable grades, L1 conversion, gates)", completion = 80 },
25-
{ name = "Phase 2: L2 grade-algebra interface + first concrete grade (affine)", completion = 0 },
26-
{ name = "Phase 3: L1 conversion checker + totality gate", completion = 0 },
27-
{ name = "Phase 4: anytype-specific typed ABI/FFI seam (replace template seam)", completion = 0 },
25+
{ name = "Phase 2: L2 grade-algebra interface + first concrete grade (affine)", completion = 100 },
26+
{ name = "Phase 3: L1 conversion checker + totality gate", completion = 100 },
27+
{ name = "Phase 4: anytype-specific typed ABI/FFI seam (replace template seam)", completion = 100 },
2828
{ name = "Phase 5: L3 guarded recursion; L0 lowering target", completion = 0 },
2929
{ name = "Phase 6: L4 effect handlers + TEA-erasure (gated on systemet OPEN-A)", completion = 0 },
3030
]
@@ -34,10 +34,11 @@ milestones = [
3434

3535
[critical-next-actions]
3636
actions = [
37-
"Define the L2 grade-algebra interface against systemet's stated laws.",
38-
"Implement the L1 conversion checker (normalize + compare) and the totality gate.",
39-
"Replace the template ABI/FFI seam with an anytype-specific one.",
40-
"Keep README/EXPLAINME inside what is built; no 'usable checker' claim until it exists.",
37+
"Add branching to L1: needs a join (least upper bound) on grades beyond the semiring+order laws -- design the extension against systemet first.",
38+
"L3 guarded recursion (Phase 5), then L0 lowering target.",
39+
"In-process seam: link the kernel via the RefC backend instead of spawning anytype-check.",
40+
"Decide the fate of the five quarantined RSR template proof modules (fix or delete; tracked in scripts/check-idris2-proofs.sh MANIFEST).",
41+
"Keep README/EXPLAINME inside what is built; the MVP claim is 'distinct disciplines from one rule set', not 'usable general-purpose checker'.",
4142
]
4243

4344
[maintenance-status]

‎.machine_readable/6a2/anchors/ANCHOR.a2ml‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,9 @@ domain = "programming-language implementation / type checkers"
2929
semantic-authority = "hyperpolymath/systemet"
3030
relationship = "implements"
3131
pin-required = true
32+
# Discharged 2026-07-21: the systemet commit this kernel implements.
33+
pinned-commit = "ba5930dc478c80b1f968eea4ca28acd0f9d67966"
34+
pinned-date = "2026-07-18"
3235
extend-not-redefine = true
3336

3437
[semantic-authority]

‎.tool-versions‎

Lines changed: 2 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,3 @@
1-
# Uncomment and customize for your project
2-
# rust nightly
3-
# just 1.40.0
4-
# nickel 1.10.0
5-
# gleam 1.8.0
6-
# elixir 1.18.0
7-
# erlang 27.2
8-
# zig 0.14.0
9-
# idris2 0.7.0
101
rust nightly
2+
idris2 0.7.0
3+
zig 0.16.0

‎AFFIRMATION.adoc‎

Lines changed: 10 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -35,14 +35,17 @@ file is a draft.
3535

3636
== What we do NOT claim
3737

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

4750
== Provenance note
4851

‎EXPLAINME.adoc‎

Lines changed: 44 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -23,18 +23,28 @@ its current state*.
2323

2424
Claim: anytype is the reference kernel for Equality Theory.
2525

26-
Reality at this commit:
27-
28-
* There is *no working checker yet*. `src/` contains RSR scaffolding
29-
(`src/interface/Abi/*.idr`, `src/interface/ffi/*.zig`, READMEs, AI-manifests), not
30-
an anytype implementation.
31-
* `tests/` and `verification/proofs/` are template stubs, not anytype tests/proofs.
32-
* What is real today: the repository *shape* (RSR), the *design* of the kernel in
33-
this file and the README, and the *split* that makes systemet the theory and
34-
anytype the engine.
35-
36-
Everything below describes the *intended* mapping. Where a file does not yet exist or
37-
is a stub, it is named as such. The dated, signed snapshot is `AFFIRMATION.adoc`.
26+
Reality at this commit (2026-07-21, MVP kernel):
27+
28+
* The kernel *exists for the MVP cut*: `src/kernel/` is a usage-counting
29+
bidirectional checker for a simply-graded λ-calculus, parameterised by a
30+
`GradeAlgebra` record whose ordered-semiring laws are proof fields. Two
31+
instances ship — affine `{0,1,ω}` (mirroring AffineScript `lib/quantity.ml`)
32+
and exact-usage `ℕ` — and the 19-case golden matrix shows the same rules
33+
yielding distinct disciplines (affine accepts drop, exact rejects it).
34+
* The seam is anytype's own: `src/interface/Abi/` (wire types with injective
35+
codes; layouts proven `CABICompliant`), the `anytype-check` CLI
36+
(`src/cli/`), and the Zig `anytype_check` export (`src/interface/ffi/`)
37+
with comptime asserts against the proven layouts. MVP transport is a
38+
spawned process; in-process RefC linkage is future work.
39+
* Gates are real and hard-fail: `just test`, `just proof-check-idris2`
40+
(manifest over every `.idr`; missing prover = FAIL), and CI
41+
`idris2-proof.yml`. Five never-compiling template modules under
42+
`verification/proofs/idris2/` are quarantined, not hidden.
43+
* Not built: dependent types, branching (needs a grade join beyond the
44+
stated laws), L3 recursion, L0 lowering, L4 effects (TEA is open in
45+
systemet), and any soundness proof for the checker itself.
46+
47+
The dated snapshot is `AFFIRMATION.adoc`.
3848

3949
== Pluggable grades (the L2 mechanism)
4050

@@ -52,9 +62,14 @@ Division of responsibility:
5262
* systemet *defines the laws* a grade algebra must satisfy.
5363
* anytype *implements the interface and checks candidates against those laws*.
5464

55-
Caveat:
65+
State:
5666

57-
* None of this interface exists in code yet. It is the kernel's first build target.
67+
* Built (MVP): `src/kernel/Anytype/Grade/Algebra.idr` is the interface — a record
68+
whose law fields make an unlawful algebra unrepresentable. `Affine.idr` and
69+
`Exact.idr` are the first two instances. The richer grades (cost,
70+
information-flow lattice, probability-like, privacy budget) remain future
71+
instances; branching additionally needs a join operation the record does not
72+
yet carry.
5873

5974
== L1 equality and the totality gate
6075

@@ -67,10 +82,16 @@ Intended implementation:
6782
* A totality checker that rejects non-terminating type-level functions, so conversion
6883
terminates.
6984

70-
Caveat:
85+
State and caveat:
7186

87+
* Built (MVP): `Anytype.Core.Normalise` + `Anytype.Core.Conversion`, invoked at the
88+
single check/infer mode switch in `Anytype.Core.Check`. The MVP totality gate is
89+
*syntactic*: the type-index language (`TNat`) has no recursion constructor, and the
90+
normaliser is `%default total` — machine-checked, but a gate by construction, not a
91+
termination analysis over a type-level function space (there is no type-level
92+
function space yet).
7293
* The strength of "equality is conversion" is exactly the strength of the totality
73-
checker. Any escape hatch must be recorded as an explicit unsafe boundary in
94+
gate. Any escape hatch must be recorded as an explicit unsafe boundary in
7495
`AFFIRMATION.adoc`, never folded silently into equality. The *theorem* that this is
7596
sound is systemet's obligation; this repo only has to *implement the check*.
7697

@@ -123,10 +144,14 @@ How this is implemented:
123144
* `src/interface/Abi/` holds Idris2 interface/layout descriptions; `src/interface/ffi/`
124145
holds the Zig FFI; `src/interface/generated/` is where generated C headers land.
125146

126-
Caveat:
147+
State:
127148

128-
* These are currently the *template's* seam files, not anytype-specific ones. They
129-
demonstrate the pattern; they do not yet describe an anytype ABI.
149+
* Built (MVP): `Abi.Types` (discipline/verdict codes, injectivity + round-trip
150+
proofs), `Abi.Layout` (`anytype_request_t`/`anytype_response_t` proven
151+
`CABICompliant`), `Abi.Foreign` (the `anytype_check` contract), and the Zig side
152+
comptime-asserting the same layouts. Transport is a spawned `anytype-check`
153+
process; `src/interface/generated/` C headers and in-process linkage are future
154+
work.
130155

131156
== RSR integration
132157

‎Justfile‎

Lines changed: 23 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -129,26 +129,29 @@ clean-all: clean
129129
# TEST & QUALITY
130130
# ═══════════════════════════════════════════════════════════════════════════════
131131

132-
# Run all tests
132+
# Hard-fails if idris2 is absent -- a gate that cannot fail is not a gate
133+
# (see scripts/check-idris2-proofs.sh for the history).
134+
# Typecheck the ABI seam, build the kernel, run the golden matrix
133135
test *args:
134-
@echo "Running tests..."
135-
# TODO: Replace with your test command
136-
# Examples:
137-
# cargo test {{args}}
138-
# mix test {{args}}
139-
# zig build test {{args}}
140-
# deno test {{args}}
141-
@echo "Tests passed!"
136+
@command -v idris2 >/dev/null || { echo "FAIL: idris2 not on PATH (install Idris2 0.7.0)"; exit 1; }
137+
idris2 --install anytype.ipkg
138+
idris2 --install abi.ipkg
139+
idris2 --build anytype-tests.ipkg
140+
./build/exec/anytype-tests
141+
idris2 --build anytype-cli.ipkg
142+
./scripts/check-cli.sh
143+
@command -v zig >/dev/null || { echo "FAIL: zig not on PATH (Zig seam tests need it)"; exit 1; }
144+
cd src/interface/ffi && zig build test
142145

143146
# Run tests with verbose output
144147
test-verbose:
145148
@echo "Running tests (verbose)..."
146149
# TODO: Replace with verbose test command
147150

148-
# Smoke test
151+
# Smoke test: does the kernel package typecheck at all?
149152
test-smoke:
150-
@echo "Smoke test..."
151-
# TODO: Add basic sanity checks
153+
@command -v idris2 >/dev/null || { echo "FAIL: idris2 not on PATH"; exit 1; }
154+
idris2 --typecheck anytype.ipkg
152155

153156
# Run end-to-end tests (full pipeline: build → run → verify)
154157
e2e:
@@ -593,7 +596,14 @@ help-me:
593596
# FORMAL VERIFICATION (PROOFS) — see build/just/proofs.just
594597
# ═══════════════════════════════════════════════════════════════════════════════
595598
596-
import? "build/just/proofs.just"
599+
# Proof gates replace the deleted build/just/proofs.just, whose recipes
600+
# exited 0 when the prover was absent (the estate fake-gate flaw).
601+
# Type-check every Idris2 module against the MANIFEST (hard-fail gate)
602+
proof-check-idris2:
603+
./scripts/check-idris2-proofs.sh
604+
605+
# Run all proof gates
606+
proof-check: proof-check-idris2
597607
598608
# ═══════════════════════════════════════════════════════════════════════════════
599609
# SESSION MANAGEMENT (THIN BINDINGS TO CENTRAL STANDARDS)

0 commit comments

Comments
 (0)