MVP kernel: L2 grade algebras + L1 graded checker + anytype-specific seam (Phases 2-4)#12
Merged
Merged
Conversation
The build/ tree held template guix/just scaffolding whose proof-check recipes exit 0 when the prover is absent (the estate-wide fake-green gate flaw). Real, hard-failing test and proof-check recipes land directly in the Justfile and scripts/ in the following commits. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…1 graded checker
Phases 2-3 of route-to-mvp, no longer scaffolding:
- Anytype.Grade.Algebra: GradeAlgebra record whose semiring and order
laws are proof fields -- an unlawful algebra is unrepresentable.
- Anytype.Grade.Affine: {0,1,omega} mirroring affinescript
lib/quantity.ml cell-for-cell (1+1=omega saturation, omega*1=omega);
all laws discharged by exhaustive enumeration, %default total,
no believe_me/assert_total/holes anywhere.
- Anytype.Grade.Exact: exact-usage Nat instance (order = equality),
the same-rules-distinct-disciplines demonstration systemet requires.
- Anytype.Core.*: bidirectional simply-graded lambda calculus with
usage counting; TNat index language total by construction (the MVP
L1 totality gate); conversion = normalise-and-compare at a single
mode-switch site.
- Golden matrix (19 cases): affine accepts drop where exact rejects it;
omega-arrow scaling rejection; TBits conversion accept/reject.
- scripts/check-idris2-proofs.sh: manifest-driven hard-fail proof gate
(missing toolchain = FAIL; unlisted .idr = FAIL; quarantined template
modules must keep failing). Adapted from ideas-to-alphas.
- Justfile: test / test-smoke / proof-check-idris2 are real commands,
replacing the template echo placeholders.
All gates watched failing (toolchain absent, sabotaged proof, flipped
golden expectation) before being made green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…pe-check CLI Phase 4 (Idris half): replaces the RSR template's generic librsr demo with anytype's actual seam: - Abi.Types: Discipline/Verdict wire types; codes proven injective, decode proven inverse of encode. - Abi.Layout: template's Divides/StructLayout machinery re-scoped to the real anytype_request_t / anytype_response_t layouts (16 bytes, align 8), both proven CABICompliant. abi.ipkg renamed anytype-abi. - Abi.Foreign: seam contract for the Zig-exported anytype_check symbol; MVP transport is a spawned process (Zig binding pending). - Anytype.Sexp (total S-expression reader, fuel-bounded, scope-checked de Bruijn) + Anytype.Main: the anytype-check executable. Exit codes are verdictCode values: 0 accept, 1 reject, 2 ill-formed. - scripts/check-cli.sh: 8 seam golden tests (verdict line + exit code); wired into just test and CI alongside the proof sweep. - Proof MANIFEST extended to the CLI modules (coverage rule caught them first, as designed). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…rts, round-trip tests
Replaces the un-instantiated {{project}} template. checkWith spawns the
anytype-check kernel binary and maps its exit code (= verdictCode) back
to the C return value; wire structs are comptime-asserted against the
layouts proven in Abi.Layout, so a drift on either side breaks a gate.
zig build test wired into just test and CI (toolchain checksum-pinned;
missing zig or missing kernel binary FAILS, never skips).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
… built kernel - README: L1/L2 rows design->built (MVP); honesty WARNING rewritten to enumerate what is and is not built. - EXPLAINME: current-state section describes the real kernel, gates and seam; per-section caveats updated from 'intended' to 'built (MVP)'. - AFFIRMATION: what-we-do-NOT-claim updated (still an unsigned draft -- signing requires the anchor checklist). - STATE.a2ml: completion 10->40, phase design->implementation, Phases 2/3/4 -> 100, new critical-next-actions (branching join, L3/L0, in-process seam, quarantined template proofs). - ANCHOR.a2ml: systemet pin discharged with a concrete commit (ba5930dc478c80b1f968eea4ca28acd0f9d67966, 2026-07-18). - PROOF-STATUS/ROADMAP: de-templated; MANIFEST is the source of truth. - .tool-versions: idris2 0.7.0 + zig 0.16.0 active; mise.toml purged of template runtime residue (node/python/go/bun/npm etc). - ffi README: seam contract + process-boundary transport stated. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The !/build/ negations existed for the old tracked build/ config directory; after its removal they were re-including Idris2's compiled artifacts (.so/.ss executables), which landed in the previous commits. build/ is generated output only now. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
|
hyperpolymath
added a commit
to hyperpolymath/affinescript
that referenced
this pull request
Jul 21, 2026
) Resolves the long-standing `// TODO: link the SystemET / Anytype design notes once they have stable locations.` at README.adoc:115. Both locations are now stable — and as of hyperpolymath/anytype#12 the kernel is real code, not prose: AffineScript's `{0,1,ω}` quantity semiring (`lib/quantity.ml`) is one instantiation of anytype's L2 grade-algebra interface (its affine instance mirrors `q_add`/`q_mul`/`q_le` cell-for-cell, verified by anytype's golden matrix). Docs-only change. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
hyperpolymath
marked this pull request as ready for review
July 21, 2026 06:48
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
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.
Anytype.Grade.Algebra— aGradeAlgebrarecord whose ordered-semiring laws are proof fields, so an unlawful algebra is unrepresentable. Instances: affine{0,1,ω}(mirrors AffineScriptlib/quantity.mlcell-for-cell, incl. theω·1=ωBUG-001 rule) and exact-usageℕ.%default total, nobelieve_me/holes anywhere); conversion = normalise-and-compare at one site.Abi.{Types,Layout,Foreign}rewritten from template demos to anytype's wire contract (codes proven injective; request/response layouts provenCABICompliant);anytype-checkCLI with a total fuel-bounded S-expression reader; Zig 0.16anytype_checkexport with comptime layout asserts. MVP transport: spawned process (stated in the ffi README).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-0build/just/proofs.justrecipes are deleted.ba5930dc, PROOF-STATUS/ROADMAP de-templated,.tool-versionsidris2 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):
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.idrfiles accounted for.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