diff --git a/.machine_readable/6a2/CLADE.a2ml b/.machine_readable/6a2/CLADE.a2ml index b14389c..ef5ec20 100644 --- a/.machine_readable/6a2/CLADE.a2ml +++ b/.machine_readable/6a2/CLADE.a2ml @@ -3,24 +3,29 @@ # See: https://github.com/hyperpolymath/gv-clade-index [identity] -uuid = "a5ea1382-a34c-5334-8a46-a2ebe904c810" +# uuid: PROVISIONAL — deterministic UUIDv5 of the canonical forge URL +# (uuid5(URL-namespace, "https://github.com/hyperpolymath/anytype")). +# Reproducible, not invented; confirm/register the canonical id in gv-clade-index. +uuid = "967a6646-b2be-5b10-9fa6-fa0bb1db090c" primary-forge = "github" primary-owner = "hyperpolymath" -canonical-name = "rsr-template-repo" -prefixed-name = "rm-rsr-template-repo" +canonical-name = "anytype" +prefixed-name = "at-anytype" [clade] -primary = "rm" -secondary = ["gv"] -assigned = "2026-03-16" -rationale = "" +# PROVISIONAL clade codes — confirm/assign in gv-clade-index (the authority). +# "at" = anytype kernel; secondary "et" = it implements Equality Theory. Not yet registry-verified. +primary = "at" +secondary = ["et"] +assigned = "2026-06-28" +rationale = "at = the anytype kernel (reference implementation); secondary et = it implements systemet (Equality Theory). PROVISIONAL pending gv-clade-index registration." [forges] -github = "hyperpolymath/rsr-template-repo" -gitlab = "hyperpolymath/rsr-template-repo" -bitbucket = "hyperpolymath/rsr-template-repo" +github = "hyperpolymath/anytype" +gitlab = "hyperpolymath/anytype" +bitbucket = "hyperpolymath/anytype" [lineage] type = "standalone" -parent = "RSR template — scaffold for new repos" -born = "2026-03-16" +parent = "Split out of the combined 'EveryType' draft (2026-06-28): anytype is the kernel half; the theory half is the systemet repo." +born = "2026-06-28" diff --git a/.machine_readable/6a2/ECOSYSTEM.a2ml b/.machine_readable/6a2/ECOSYSTEM.a2ml index 0757418..528ade1 100644 --- a/.machine_readable/6a2/ECOSYSTEM.a2ml +++ b/.machine_readable/6a2/ECOSYSTEM.a2ml @@ -1,45 +1,31 @@ # SPDX-License-Identifier: MPL-2.0 -# ECOSYSTEM.a2ml — Ecosystem position (META-TEMPLATE) -# -# This is the ECOSYSTEM file for rsr-template-repo itself. It records the -# TEMPLATE's own position in the estate. When consumed by a new project, -# replace these fields with the target project's ecosystem position and -# related projects (see the NOTE FOR CONSUMERS at the bottom). +# ECOSYSTEM.a2ml — Ecosystem position for anytype (the Equality Theory kernel). [metadata] -project = "rsr-template-repo" +project = "anytype" ecosystem = "hyperpolymath" [position] -type = "repository-template" -purpose = "Canonical RSR-compliant repository template: scaffolding (CI/CD, AI manifests, ABI/FFI standards, container ecosystem, governance) that new hyperpolymath projects are instantiated from." +type = "type-checker-kernel" +purpose = "The reference kernel for systemet (Equality Theory): a small parameterised checker whose discipline is chosen by choosing the L2 resource algebra. 'Pick the algebra, get the discipline.' Implements the theory; does not define it." # IS-NOT — anti-identity (the boundary-erosion guard; each line is a real past confusion) what-this-is-not = [ - "a project in its own right", - "Scaffoldia (the full-featured repo designer)", - "standards (the canon source this template operationalises)", + "the theory (that is the systemet repo — anytype pins it upstream and extends-not-redefines it)", + "EveryType (the over-claiming former name; there is no universal 'every type' relation here)", + "AffineScript (a downstream product profile of this kernel)", + "a working type checker yet (the implementation is at scaffolding stage — see AFFIRMATION)", ] [pipeline] -position = "foundation" -chain = "standards → rsr-template-repo → (every estate repo)" -notes = "rsr-template-repo turns the RSR standard into runnable scaffolding. New repos are created from it via `just init`, which substitutes the {{PLACEHOLDER}} tokens." +position = "kernel" +chain = "systemet (theory) → anytype (kernel) → AffineScript (profile)" +notes = "anytype implements systemet's Equality Theory. It must pin systemet upstream as semantic authority and may extend but not redefine the theory." coordination = "standards" [related-projects] projects = [ - { name = "standards", relationship = "standard-source", notes = "Defines the RSR standard, contractile canon, and policies that this template operationalises." }, - { name = "stapeln", relationship = "build-tooling", notes = "Layer-based container build system; the template ships stapeln.toml scaffolding." }, - { name = "selur-compose", relationship = "build-tooling", notes = "Service composition; the template ships selur-compose.toml scaffolding." }, - { name = "k9-svc", relationship = "validation-tooling", notes = "Runs the self-validating k9.ncl checks (.machine_readable/self-validating/)." }, - { name = "cerro-torre", relationship = "signing-tooling", notes = "Container/image signing provider referenced by the container scaffolding." }, - { name = "svalinn", relationship = "verification-tooling", notes = "Supply-chain verification referenced by the container scaffolding." }, - { name = "vordr", relationship = "verification-tooling", notes = "Build/artifact verification referenced by the container scaffolding." }, + { name = "systemet", relationship = "upstream-theory", notes = "The theory (Equality Theory) this kernel implements and pins as semantic authority." }, + { name = "AffineScript", relationship = "downstream-profile", notes = "One product profile (grade = affine + cost) built on this kernel; targets WASM contracts/edge functions." }, + { name = "standards", relationship = "standard-source", notes = "Defines the RSR standard, contractile canon, and policies this repo operationalises." }, + { name = "proven", relationship = "verification-tooling", notes = "Idris2/proof tooling for the typed ABI/FFI seam and kernel obligations." }, ] - -# --------------------------------------------------------------------------- -# NOTE FOR CONSUMERS: When using this template to create a new repo, replace -# the project/purpose above and rewrite [related-projects] to describe YOUR -# project's actual ecosystem. The entries above describe the TEMPLATE's own -# position, not yours. -# --------------------------------------------------------------------------- diff --git a/.machine_readable/6a2/META.a2ml b/.machine_readable/6a2/META.a2ml index d66fb7b..c5da7c1 100644 --- a/.machine_readable/6a2/META.a2ml +++ b/.machine_readable/6a2/META.a2ml @@ -6,17 +6,22 @@ [metadata] version = "0.1.0" -last-updated = "2026-04-11" +last-updated = "2026-06-28" [project-info] -type = "library" # TODO: update type (library|binary|service|website|monorepo) # library | binary | monorepo | service | website -languages = [] # e.g. ["rust", "zig", "idris2"] +type = "binary" # a type-checker kernel / engine +languages = ["rust", "idris2", "zig"] # planned kernel + typed ABI/FFI seam license = "MPL-2.0" author = "Jonathan D.A. Jewell (hyperpolymath)" [architecture-decisions] # ADR format: status = proposed | accepted | deprecated | superseded | rejected -# - { id = "ADR-001", title = "Use Zig for FFI", status = "accepted", date = "2026-02-14" } +adrs = [ + { id = "ADR-001", title = "Rename EveryType -> anytype: no universal 'every type' claim; pick any L2 algebra", status = "accepted", date = "2026-06-28" }, + { id = "ADR-002", title = "Split: theory -> systemet (semantic authority), kernel -> anytype (this repo); pin systemet upstream", status = "accepted", date = "2026-06-28" }, + { id = "ADR-003", title = "Discipline is a parameter (the L2 grade algebra), checked by one set of rules", status = "accepted", date = "2026-06-28" }, + { id = "ADR-004", title = "Equality is conversion (normalize+compare); totality gate makes it decidable; no coercions", status = "accepted", date = "2026-06-28" }, +] [development-practices] build-tool = "just" diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 3d2d647..475a1cc 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -1,49 +1,43 @@ # SPDX-License-Identifier: MPL-2.0 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) # -# STATE.a2ml — Project state checkpoint (META-TEMPLATE) -# -# This is the STATE file for rsr-template-repo itself. -# When consumed by a new project, replace {{PLACEHOLDER}} tokens -# and customize sections below for the target project. +# STATE.a2ml — Project state checkpoint for anytype (the Equality Theory kernel). [metadata] -project = "rsr-template-repo" -version = "0.2.0" -last-updated = "2026-02-28" +project = "anytype" +version = "0.1.0" +last-updated = "2026-06-28" status = "active" # active | paused | archived [project-context] -name = "rsr-template-repo" -purpose = "Canonical RSR-compliant repository template providing scaffolding for all hyperpolymath projects — including CI/CD, AI manifests, ABI/FFI standards, container ecosystem, and governance infrastructure." -completion-percentage = 95 +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 [position] -phase = "maintenance" # design | implementation | testing | maintenance | archived -maturity = "production" # experimental | alpha | beta | production | lts +phase = "design" # design | implementation | testing | maintenance | archived +maturity = "experimental" # experimental | alpha | beta | production | lts [route-to-mvp] milestones = [ - { name = "Phase 0: Core scaffolding (justfile, CI/CD, .machine_readable)", completion = 100 }, - { name = "Phase 1: ABI/FFI standard (Idris2/Zig templates)", completion = 100 }, - { name = "Phase 1b: AI Gatekeeper Protocol (0-AI-MANIFEST.a2ml)", completion = 100 }, - { name = "Phase 1c: TOPOLOGY.md standard and guide", completion = 100 }, - { name = "Phase 1d: Maintenance gate (axes, checklist, approach)", completion = 100 }, - { name = "Phase 1e: Trustfile / contractiles", completion = 100 }, - { name = "Phase 2: Container ecosystem templates (stapeln)", completion = 100 }, - { name = "Phase 3: Multi-forge sync hardening", completion = 0 }, - { name = "Phase 4: Guix reproducible shells", completion = 50 }, + { 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 5: L3 guarded recursion; L0 lowering target", completion = 0 }, + { name = "Phase 6: L4 effect handlers + TEA-erasure (gated on systemet OPEN-A)", completion = 0 }, ] [blockers-and-issues] -# No active blockers +# L4/TEA work is gated on systemet's open TEA-erasure result (not a code blocker yet). [critical-next-actions] actions = [ - "Container templates complete — test with `just container-init`", - "Validate container templates across wolfi-base and static Chainguard images", - "Harden multi-forge sync for GitLab/Bitbucket mirroring edge cases", - "Expand Guix development shell templates", + "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.", ] [maintenance-status] @@ -54,11 +48,5 @@ open-warnings = 0 open-failures = 0 [ecosystem] -part-of = ["RSR Framework", "stapeln ecosystem"] -depends-on = ["stapeln", "selur-compose", "cerro-torre", "svalinn", "vordr", "k9-svc"] - -# --------------------------------------------------------------------------- -# NOTE FOR CONSUMERS: When using this template to create a new repo, reset -# the fields above to your project's values and replace all {{PLACEHOLDER}} -# tokens. The milestones above describe the TEMPLATE's evolution, not yours. -# --------------------------------------------------------------------------- +part-of = ["hyperpolymath estate"] +depends-on = ["systemet"] diff --git a/.machine_readable/6a2/anchors/ANCHOR.a2ml b/.machine_readable/6a2/anchors/ANCHOR.a2ml index 8723899..77347a9 100644 --- a/.machine_readable/6a2/anchors/ANCHOR.a2ml +++ b/.machine_readable/6a2/anchors/ANCHOR.a2ml @@ -1,41 +1,54 @@ # SPDX-License-Identifier: MPL-2.0 -# Copyright (c) {{CURRENT_YEAR}} {{AUTHOR}} ({{OWNER}}) <{{AUTHOR_EMAIL}}> +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) # # ANCHOR.a2ml - authoritative anchor for this repository [metadata] version = "1.0.0" -last-updated = "{{CURRENT_DATE}}" +last-updated = "2026-06-28" [anchor] schema = "hyperpolymath.anchor/1" -repo = "{{OWNER}}/{{REPO}}" -authority = "upstream-canonical" +repo = "hyperpolymath/anytype" +authority = "satellite" # downstream of systemet for the theory; canonical for the engine purpose = [ - "Define canonical semantics and policy boundaries for this repository.", - "Declare what downstream/satellite repos can extend but not redefine.", + "Define the canonical behaviour of the anytype kernel (the engine).", + "Pin systemet upstream as the semantic authority for the theory, and extend-not-redefine it.", "Provide a stable golden path and invariant contract for release readiness.", ] [identity] -project = "{{PROJECT_NAME}}" -kind = "{{PROJECT_KIND}}" # language | library | service | tool -one-sentence = "{{PROJECT_PURPOSE}}" -domain = "{{PROJECT_DOMAIN}}" +project = "anytype" +kind = "tool" # a type-checker kernel / engine +one-sentence = "Reference kernel for Equality Theory: pick the L2 resource algebra, get the discipline." +domain = "programming-language implementation / type checkers" + +[upstream] +# anytype is a satellite of systemet (the theory). It must not redefine the theory. +semantic-authority = "hyperpolymath/systemet" +relationship = "implements" +pin-required = true +extend-not-redefine = true [semantic-authority] -policy = "canonical" +policy = "extends-upstream" owns = [ - "Project semantics and specification", - "Invariant definitions and contractiles", - "Reference implementation behavior", + "anytype kernel behaviour (the checker, normaliser, grade-algebra interface)", + "The typed ABI/FFI seam and its layout proofs", + "Lowering/runtime behaviour (L0 target)", +] + +defers-to-upstream = [ + "Meaning of the layers and the gates (systemet)", + "The laws an L2 grade algebra must satisfy (systemet)", + "All proof obligations: L1 totality/soundness, trope preservation, TEA erasure (systemet)", ] [implementation-policy] allowed = ["Rust", "Idris2", "Zig", "Scheme", "Shell", "Just", "AsciiDoc", "Markdown"] -forbidden = ["Node.js", "npm"] +forbidden = ["Node.js", "npm", "TypeScript", "Python", "Go"] [golden-path] smoke-test-command = [ @@ -54,9 +67,3 @@ must-pin-upstream = true must-declare-authority = true must-have-anchor = true must-have-golden-path = true - -[semantic-authority-files] -language-spec = "SPECIFICATION.md" -formal-proofs = "docs/proofs/PROOFS.adoc" -type-theory = "docs/theory/THEORY.adoc" -algorithms = "docs/theory/ALGORITHMS.adoc" diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml index 68aad8c..493362b 100644 --- a/0-AI-MANIFEST.a2ml +++ b/0-AI-MANIFEST.a2ml @@ -5,11 +5,11 @@ # [metadata] version = "0.1.0" -last-updated = "{{CURRENT_DATE}}" +last-updated = "2026-06-28" [project] -name = "[YOUR-REPO-NAME]" -purpose = "{{PROJECT_DESCRIPTION}}" +name = "anytype" +purpose = "Reference kernel for systemet (Equality Theory): a parameterised type checker whose discipline is chosen by choosing the L2 resource algebra. 'Pick the algebra, get the discipline.' Implements the theory; pins systemet upstream. Early/scaffolding — no working checker yet." [ai-allocation] agents = [ diff --git a/AFFIRMATION.adoc b/AFFIRMATION.adoc index 3a840b4..83af40a 100644 --- a/AFFIRMATION.adoc +++ b/AFFIRMATION.adoc @@ -1,95 +1,70 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell -= AFFIRMATION — {{PROJECT_NAME}}, as of += AFFIRMATION — anytype, as of :toc: macro :toclevels: 2 _the No-Bullshit file: what we affirm was true and checkable at this moment._ -[NOTE] -==== -*This file is a template.* Replace the `{{…}}` placeholders and the `<…>` anchor -fields, then re-run your project's own checks in the same session before signing. - -An *affirmation* is a solemn declaration of the truth of a statement, made by -someone who _declines to swear an oath_ — our truth-as-best-believed at a stamped -instant, binding on our honesty, not a claim of infallibility. It is the third of -the README / EXPLAINME / AFFIRMATION trio: - -[cols="1,3,2",options="header"] -|=== -| File | Answers | Tense -| `README.adoc` | _Where is this going, and why?_ — steering, intent, vision | future / aspirational -| `EXPLAINME.adoc` | _How is it built, and what's the evidence?_ — engineering | descriptive / mechanism -| *`AFFIRMATION.adoc`* (this file) | _What can we honestly affirm was *true and checkable* at a stamped moment?_ | a frozen instant, falsifiable -|=== -==== - toc::[] -== What this is, and how it works - -*What it is.* A short, dated, signed snapshot of what {{OWNER}} can honestly and -verifiably claim about *{{PROJECT_NAME}}* at one exact commit. Nothing here is -marketing and nothing is a promise about the future — those live in the README. -This file is the receipt. +== What this is -*How it stays trustworthy.* Three moving parts: +A short, dated, signed snapshot of what can be honestly and verifiably claimed about +*anytype* — the reference kernel for Equality Theory — at one exact commit. The README +is the vision; `EXPLAINME.adoc` is the mechanism; this file is the receipt. It is our +best honest belief at a stamped instant, binding on our honesty, not a claim of +infallibility. -. *Ground truth, not memory.* Every claim below must be produced by _running the - project's own checks_ in the session that writes this file (build, tests, - typecheck, `just audit`). Where a status doc, the `Justfile`, or memory says - otherwise, the live run wins and the contradiction is flagged here. -. *A frozen anchor.* The file names the exact commit SHA, branch, UTC timestamp, - and toolchain (see <>), so "true" always means "true _at - this point_". Move the SHA and this file is a draft until it is re-run. -. *A real signature.* It is landed by a *signed git commit*; that signature over - this content at the anchored SHA is what makes the affirmation tamper-evident - and attributable — not the prose alone. - -*We are fallible.* This is our best honest belief, not a proof of its own -correctness. Treat it as a falsifiable claim, not gospel. - -== The epistemic contract (read this before you trust _or_ attack) - -This document records {{OWNER}}'s *best belief* at the timestamp below. It is -*not a guarantee of correctness.* The only guarantee is *no intentional -overclaim*: where something is proven we say "proven"; where it is a documented -trust boundary, an experiment, or an unwired module, we say so; where a claim is -the README's aspiration rather than a checked result, we say so. An honest claim -that later turns out false is an *error to be fixed* — not a lie. - -*Standing invitation to refute.* You are invited to bulldoze any claim in this -file. Bring a counter-example, a failing run, or a contradicting source. +[NOTE] +==== +The anchor below carries `<…>` fields (commit SHA, timestamp, toolchain) that are +filled in *at signing time*, in the same session that runs the checks. Until then this +file is a draft. +==== -== What we affirm (fill in — delete the examples) +== What we affirm -[cols="2,1,3",options="header"] +[cols="3,1,3",options="header"] |=== -| Claim | Status | Evidence (command / `file:line`) -| _e.g. The library builds clean_ | affirmed | `just build` at the anchor SHA -| _e.g. The ABI seam typechecks_ | affirmed | `idris2 --typecheck abi.ipkg` -| _e.g. Feature X is complete_ | aspiration | README §… (not yet checked) +| Claim | Status | Evidence +| The repository is RSR-shaped and validates | affirmed-pending-run | `just validate` at the anchor SHA +| The kernel's design is written down (pluggable L2 grades; L1 conversion; gates) | affirmed | `README.adoc`, `EXPLAINME.adoc` +| anytype is the implementation; `systemet` is the theory it pins upstream | affirmed | `.machine_readable/6a2/anchors/ANCHOR.a2ml`, `ECOSYSTEM.a2ml` |=== == What we do NOT claim -* List the known gaps, trust boundaries, postulates, unwired modules, and stale - docs here. Silence is not affirmation — name what you have *not* verified. +* *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. +* *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. + +== Provenance note + +This kernel was first drafted under the over-claiming name *EveryType*, which wrongly +implied a universal "every type" relation and conflated the theory, the kernel, and a +product profile in one repo. It is renamed *anytype* (pick *any* resource algebra, get +*that* discipline). The theory now lives in +link:https://github.com/hyperpolymath/systemet[systemet]; the profile is AffineScript. [#verifiable-anchor] == Verifiable anchor [cols="1,3"] |=== -| Project | {{PROJECT_NAME}} -| Repository | https://{{FORGE}}/{{OWNER}}/{{REPO}} +| Project | anytype +| Repository | https://github.com/hyperpolymath/anytype | Commit (SHA) | -| Branch | {{MAIN_BRANCH}} +| Branch | main | Timestamp (UTC) | | Toolchain | -| Affirmed by | {{AUTHOR}} <{{AUTHOR_EMAIL}}> +| Affirmed by | Jonathan D.A. Jewell |=== -_Landed by a signed git commit. Verify with `git log --show-signature` that the -anchor SHA above matches the commit that introduced this affirmation._ +_Landed by a signed git commit. Verify with `git log --show-signature` that the anchor +SHA above matches the commit that introduced this affirmation._ diff --git a/CHANGELOG.md b/CHANGELOG.md index ec7f2e1..3b3e8a5 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -13,3 +13,25 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ## [Unreleased] + +### Changed +- **Renamed EveryType → anytype.** The old name over-claimed a universal "every type" + relation (exactly the System-Fc trap this design refuses). The honest claim is the + opposite: pick *any* L2 resource algebra, get *that* discipline. +- Re-scoped this repository to the **kernel/engine** only. The theory it implements + was split out into the **systemet** repo (Equality Theory), which is now the + semantic authority; anytype pins it upstream and extends-not-redefines it. +- Rewrote `README.adoc` and `EXPLAINME.adoc` for the kernel, with an explicit honesty + notice that no working checker exists yet (the `src/`/`tests/`/`verification/` trees + are RSR scaffolding). + +### Added +- Instantiated identity descriptiles (CLADE/ECOSYSTEM/ANCHOR/STATE/META) and the + AFFIRMATION honesty snapshot with the anytype identity and an honest early-stage + status; ANCHOR pins systemet upstream. + +### Notes +- `uuid` is a PROVISIONAL deterministic UUIDv5 of the forge URL; `clade` is + PROVISIONAL. Both must be confirmed/registered in `gv-clade-index`. +- `CLAUDE.md` is generated from the descriptiles — run `just claude-md` to refresh it + where `nickel`/`just` are available. diff --git a/CITATION.cff b/CITATION.cff index 5de4710..65f9d2d 100644 --- a/CITATION.cff +++ b/CITATION.cff @@ -1,17 +1,20 @@ cff-version: 1.2.0 message: "If you use this software, please cite it as below." authors: -- family-names: "{{AUTHOR_LAST}}" - given-names: "{{AUTHOR_FIRST}}" - orcid: "https://orcid.org/0000-0000-0000-0000" # Placeholder -title: "{{PROJECT_NAME}}" +- family-names: "Jewell" + given-names: "Jonathan D.A." + orcid: "https://orcid.org/0000-0000-0000-0000" # TODO(owner): replace with real ORCID +title: "anytype — the Equality Theory kernel" version: 0.1.0 -date-released: "{{CURRENT_DATE}}" -url: "https://{{FORGE}}/{{OWNER}}/{{REPO}}" -repository-code: "https://{{FORGE}}/{{OWNER}}/{{REPO}}" +date-released: "2026-06-28" +url: "https://github.com/hyperpolymath/anytype" +repository-code: "https://github.com/hyperpolymath/anytype" license: MPL-2.0 keywords: + - "type-checker" + - "equality-theory" + - "systemet" + - "graded-modal-types" + - "pluggable-grades" - "rsr" - "formal-verification" - - "neurosymbolic" - - "provenance" diff --git a/CLAUDE.md b/CLAUDE.md index b352a59..35fc38f 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -6,7 +6,7 @@ SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell - + # You are in the hyperpolymath estate — orient before acting @@ -54,14 +54,14 @@ Deny: **Nix, Node/npm, TypeScript, Python, Go, AGPL**. (Guix, not Nix.) --- -# This repo: `rsr-template-repo` · clade `rm-rsr-template-repo` +# This repo: `anytype` · clade `at-anytype` -- **Identity** — uuid `a5ea1382-a34c-5334-8a46-a2ebe904c810`; clade `rm` (secondary `gv`); born 2026-03-16; forge `hyperpolymath/rsr-template-repo`. -- **IS** — Canonical RSR-compliant repository template: scaffolding (CI/CD, AI manifests, ABI/FFI standards, container ecosystem, governance) that new hyperpolymath projects are instantiated from. -- **IS-NOT** — a project in its own right · Scaffoldia (the full-featured repo designer) · standards (the canon source this template operationalises) -- **Where it sits** — pipeline position **foundation**; chain `standards → rsr-template-repo → (every estate repo)`; coordination = `standards`. +- **Identity** — uuid `967a6646-b2be-5b10-9fa6-fa0bb1db090c`; clade `at` (secondary `et`); born 2026-06-28; forge `hyperpolymath/anytype`. +- **IS** — The reference kernel for systemet (Equality Theory): a small parameterised checker whose discipline is chosen by choosing the L2 resource algebra. 'Pick the algebra, get the discipline.' Implements the theory; does not define it. +- **IS-NOT** — the theory (that is the systemet repo — anytype pins it upstream and extends-not-redefines it) · EveryType (the over-claiming former name; there is no universal 'every type' relation here) · AffineScript (a downstream product profile of this kernel) · a working type checker yet (the implementation is at scaffolding stage — see AFFIRMATION) +- **Where it sits** — pipeline position **kernel**; chain `systemet (theory) → anytype (kernel) → AffineScript (profile)`; coordination = `standards`. - **Constraints here** (AGENTIC) — fail-closed; evidence-per-step; no-silent-skip; rerun-after-fix; release-claim-requires-hard-pass. Never: banned langs (above), secrets, state files in repo root, AGPL. Details: `.machine_readable/bot_directives/{methodology,coverage,debt}.a2ml`. - **Golden path** (ANCHOR) — `just test && just quality` → Core tests pass; Quality gates pass; No unresolved critical security findings. -- **State** — phase maintenance; maturity production; 95% complete; status active. +- **State** — phase design; maturity experimental; 10% complete; status active. - + diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index 66527a0..d80430a 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -1,251 +1,165 @@ -= EveryType - EXPLAINME -How the README claims map to real files. +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2024-2026 Jonathan D.A. Jewell (hyperpolymath) += anytype — EXPLAINME +How the README claims map to real files, and where the engine actually is today. :toc: left :sectnums: :icons: font -This file explains how EveryType’s main claims map to implementation files, proof boundaries, repository machinery, and caveats. +The README is the public orientation: where the anytype kernel is going. This file +is the engineering account: what exists, what is scaffolding, and where the evidence +stops. -The README is the public orientation. +[IMPORTANT] +==== +*Boundary.* anytype is the *kernel* (implementation). The *theory* it implements — +the meaning of the layers, the gates, and the proof obligations — lives in +link:https://github.com/hyperpolymath/systemet[systemet]. Claims about *what the +theory says* belong in systemet's `EXPLAINME.adoc`; claims here are about *code and +its current state*. +==== -This file is the engineering account. +== Current state (read this first) -== SystemET Layering +Claim: anytype is the reference kernel for Equality Theory. -Claim: EveryType implements the open-source kernel for SystemET, a five-layer stratified type theory. +Reality at this commit: -How this is implemented: +* 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. -* L0 runtime target lives under `src/` and target-specific backend modules. -* L1 equality is implemented as normalization plus comparison, not a coercion calculus. -* L2 resources are implemented through the graded-modal substrate and pluggable semiring machinery. -* L3 guarded recursion is represented with `▶`. -* L4 effects are currently an amber/open proof area under the TEA-erasure programme. +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`. -Caveat: +== Pluggable grades (the L2 mechanism) -* The README describes the intended SystemET architecture. -* The current implementation status is bounded by `AFFIRMATION.adoc`, `AUDIT.adoc`, and the test suite. -* L4 TEA erasure is not to be described as complete until `OPEN-A` is closed. +Claim: a new discipline is a change of the L2 grade algebra, not a change of checker. -== Totality Gate +Intended implementation: -Claim: At L1, type-level functions must terminate, so equality is conversion. +* The checker is parameterised over a grade-algebra interface (a semiring with the + ordering the rules need). +* Concrete grades (affine, cost, information-flow lattice, probability-like, privacy + budget, latency×billing) are instances of that interface. -How this is implemented: +Division of responsibility: -* The totality checker rejects non-terminating type-level computation. -* Equality checking normalizes both sides and compares normal forms. -* There is no System-Fc-style coercion language. +* systemet *defines the laws* a grade algebra must satisfy. +* anytype *implements the interface and checks candidates against those laws*. Caveat: -* The guarantee is only as strong as the implemented totality checker and the proof status recorded in `AFFIRMATION.adoc`. -* Any accepted escape hatch must be documented as an assumption or unsafe boundary. +* None of this interface exists in code yet. It is the kernel's first build target. -== Structural Gate +== L1 equality and the totality gate -Claim: EveryType admits shallow structural projection but refuses deep co/contravariant rewriting. +Claim: equality is `normalize` then `compare`, with no coercion language, made +decidable by a totality check on type-level computation. -How this is implemented: +Intended implementation: -* Rows, variants, refinements, and record-like products are handled through shallow CAR/CDR-style projection. -* The permitted structural behaviour is projection from additive product structure. -* Deep variance through function spaces, effects, resources, lifetimes, or linear positions is intentionally not admitted as a general rule. +* A normaliser + structural comparison for the conversion relation. +* A totality checker that rejects non-terminating type-level functions, so conversion + terminates. Caveat: -* This is a design boundary, not an omission. -* Contributions that reintroduce deep variance must justify why they do not recreate the Coherence Cliff. +* 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 + `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*. -== Polarity Gate +== Structural and polarity gates -Claim: EveryType admits polarized casts, not true gradual `any`. +Claim: shallow `CAR`/`CDR` projection is admitted; deep variance is refused. Casts +are polarized (`A -> ?` lossless, `? -| A` blame-graded); there is no universal `any`. -How this is implemented: +Intended implementation: -* Forward casts `A -> ?` are treated as lossless forgetting. -* Backward casts `? -| A` are treated as lossy recovery attempts. -* Lossy recovery is marked with a blame grade such as `!_{blame}`. +* Projection from additive products `&`; refusal of deep co/contravariant rewriting. +* A blame grade `!_{blame}` carried as part of L2 accounting on backward casts. Caveat: -* There is no universal `any` that silently escapes the type system. -* A backward cast is not magic. It is a graded loss event. +* These are design boundaries the kernel must enforce; the justification for *why* + they avoid the Coherence Cliff is systemet's, not this repo's. -== Pluggable Grades +== Roles to tropes -Claim: EveryType can express different disciplines by changing the L2 algebra. +Claim: global roles/coercions are replaced by local finite trope machines +`A@t1 -> A@t2 -> A@t3`. -How this is implemented: +Intended implementation: -* The checker is parameterised over a grade algebra. -* Example grades include affine usage, costs, security lattices, probability-like grades, privacy budgets, and latency/billing products. +* A representation of finite, model-checkable transition machines. +* Per-API machines (file handles, sockets, transactions, streams, WASM capabilities). Caveat: -* A proposed grade must satisfy the laws required by the checker. -* “Pick the algebra” does not mean arbitrary metadata. The algebra must support the relevant operations and ordering discipline. - -== TEA Erasure - -Claim: Total, effect-graded, affine handlers should erase when the TEA discipline proves them observationally harmless. +* The *preservation result* is systemet's proof obligation. anytype implements the + machines and the runtime check; it does not, by existing, prove them sound. -How this is implemented: +== TEA erasure (L4) -* TEA is treated as an L4 erasure target. -* The intended condition is Total + Effect-graded + Affine. -* Effects are not assumed free merely because they are typed. +Claim: a Total + Effect-graded + Affine handler should erase completely. -Caveat: +Reality: -* This is currently an open proof area. -* The README must describe TEA erasure as a target or amber claim until the formal proof is complete. +* This is *OPEN* in systemet and *not started* here. The kernel must not emit code or + documentation claiming TEA erasure until systemet proves the condition and it is + recorded in `AFFIRMATION.adoc`. -== Roles to Tropes +== Typed ABI/FFI seam -Claim: EveryType replaces global roles and coercions with local finite trope transitions. +Claim: anytype has a formally-typed ABI/FFI seam. How this is implemented: -* Rather than proving global representational equality, EveryType represents state-indexed movement as `A@t1 -> A@t2 -> A@t3`. -* Tropes are finite transition machines. -* API protocols such as file handles, sockets, transactions, and streams can be modelled as finite movement through states. +* `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: -* Tropes do not mean “all role problems are solved automatically.” -* Each real API needs a finite machine and preservation story. +* These are currently the *template's* seam files, not anytype-specific ones. They + demonstrate the pattern; they do not yet describe an anytype ABI. -== RSR Integration +== RSR integration -Claim: EveryType uses the Rhodium Standard Repository structure without making that infrastructure part of the language kernel. +Claim: anytype uses the Rhodium Standard Repository structure without that +infrastructure being part of the kernel. How this is implemented: -* `0-AI-MANIFEST.a2ml` is the universal entry point for AI agents. -* `.machine_readable/` stores project metadata, policies, anchors, contractiles, and agent-readable state. -* `Justfile` provides the task surface. -* `just validate` checks the repository shape. -* `AFFIRMATION.adoc` records the dated honesty snapshot. -* `AUDIT.adoc` acts as the release audit gate. +* `0-AI-MANIFEST.a2ml` is the AI-agent entry point; `.machine_readable/` holds + metadata, policy, contractiles, anchors, and agent-readable state; `just validate` + checks repository shape; `AFFIRMATION.adoc` is the dated honesty snapshot; + `AUDIT.adoc` is the release gate. Caveat: -* RSR machinery is repository infrastructure. -* It is not part of the EveryType type theory. -* Passing RSR validation does not prove SystemET soundness. +* Passing RSR validation proves the repository is well-formed. It proves nothing about + the kernel's correctness or about systemet's soundness. Separate claims, separate + evidence. -== Central Session Protocol Authority +== Dependency updates -Claim: Session protocols are centrally maintained and not duplicated in this repository. +Claim: dependency bumps land fast and safely. How this is implemented: -* `session/dispatch.sh` maps canonical commands to central protocol paths in `standards/session-management-standards`. -* Local files such as `session/custom-checks.k9`, `session/local-hooks.sh`, and `coordination.k9` are integration-only. - -Caveat: - -* If `SESSION_STANDARDS_DIR` is unset and no adjacent standards checkout exists, the dispatcher records the command but cannot resolve central checklist paths. - -== Canonical Command Surface - -Claim: Template bindings align to one canonical command model. - -How this is implemented: - -* `Justfile` provides thin aliases such as: - ** `intake-repo` - ** `checkpoint-change` - ** `verify-maintenance` - ** `verify-substantial` - ** `verify-release` - ** `close-planned` - ** `close-urgent` - ** `recover-repo` - ** `handover-*` - -* Every alias calls `session/dispatch.sh` with canonical verb-object pairs. - -Caveat: - -* Recipes are wrappers only. -* They do not replace protocol content from the central standards repository. - -== Runtime State Is Local - -Claim: Session state is per-repository runtime output, not standards text. - -How this is implemented: - -* `session/dispatch.sh` writes command and continuity-core capture stubs to `.session/LAST-CANONICAL-COMMAND.md`. - -Caveat: - -* Runtime files are intentionally lightweight. -* They require human or agent completion. - -== Template Token Policy - -Claim: Placeholders are explicit template content until initialization. - -How this is implemented: - -* Template files keep `{{TOKEN}}` placeholders visible. -* `just init` performs token replacement. - -Caveat: - -* Uninitialized placeholders must not be treated as project-specific truth. - -== Dependency Updates - -Claim: Dependency bumps land fast and safely, without manual chasing. - -How this is implemented: - -* `dependabot.yml` watches supported ecosystems used by the estate: - ** `github-actions` - ** `cargo` - ** `mix` - ** `docker` - -* `dependabot-automerge.yml` auto-merges bumps only once required checks are green. - -Caveat: - -* A broken bump fails CI and stays open. -* It does not land on a red main. -* Dependabot has no direct Deno or Bun ecosystem. -* Do not add Dependabot as a ruleset bypass actor, because that lets bumps skip required checks. - -== Julia Registry Packages - -Claim: If this template is used to create a Julia package, it must remain a standalone repository registered with the Julia package registry. - -How this is implemented: - -* Julia’s package registry expects each registered package to be a standalone repository. -* `Project.toml` must live at the repository root. -* `Pkg.add()`, dependency resolution, and package discovery depend on the canonical structure. - -Caveat: - -* Do not move a registered Julia package into a monorepo subdirectory. -* Non-registry Julia packages can be organized differently if they are not published to a registry. +* `dependabot.yml` watches the supported ecosystems (`github-actions`, `cargo`, `mix`, + `docker`); `dependabot-automerge.yml` merges bumps only once required checks are + green. A broken bump fails CI and stays open; it does not land on a red `main`. +* Do not add Dependabot as a ruleset bypass actor — that would let bumps skip required + safety checks. == Licence -Claim: The project uses split licensing. - -How this is implemented: - -* Code, configuration, and scripts use MPL-2.0. -* Prose documentation uses CC-BY-SA-4.0. -* Per-file SPDX headers are authoritative. - -Caveat: - -* The root `LICENSE` controls GitHub’s detected licence. -* Documentation licensing must be preserved through explicit SPDX headers. +* Code/config/scripts: `MPL-2.0`. Prose documentation: `CC-BY-SA-4.0`. +* Per-file `SPDX-License-Identifier` headers are authoritative; the root `LICENSE` + controls GitHub's detected licence. diff --git a/README.adoc b/README.adoc index 03ffc3a..72296ca 100644 --- a/README.adoc +++ b/README.adoc @@ -1,322 +1,130 @@ -= EveryType +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2024-2026 Jonathan D.A. Jewell (hyperpolymath) += anytype Pick the algebra. Get the discipline. :toc: left :sectnums: :icons: font -image:https://www.bestpractices.dev/projects/TODO/badge[OpenSSF Best Practices] -image:https://img.shields.io/badge/license-MPL--2.0-blue[License: MPL-2.0] -image:https://img.shields.io/badge/docs-CC--BY--SA--4.0-lightgrey[Docs: CC-BY-SA-4.0] -image:https://img.shields.io/badge/provenance-quantum--safe-informational[Quantum-Safe Provenance] -image:https://img.shields.io/badge/standard-Rhodium-success[Rhodium Standard Repository] -image:https://img.shields.io/badge/idris-inside-purple[Idris Inside] +image:https://img.shields.io/badge/License-MPL_2.0-blue.svg[License: MPL-2.0,link="https://opensource.org/licenses/MPL-2.0"] +image:https://img.shields.io/badge/Docs-CC--BY--SA--4.0-blue.svg[Docs: CC-BY-SA-4.0,link="https://creativecommons.org/licenses/by-sa/4.0/"] +image:https://img.shields.io/badge/RSR-Rhodium_Standard-9C27B0[Rhodium Standard Repository,link="https://github.com/hyperpolymath/rhodium-standard-repositories"] +image:https://img.shields.io/badge/Idris-Inside-5E5086?logo=idris&logoColor=white[Idris Inside,link="https://github.com/hyperpolymath/proven"] +image:https://img.shields.io/badge/status-kernel_(early%2C_scaffolding)-orange[Status: early] + +*anytype* is the reference *kernel* for +link:https://github.com/hyperpolymath/systemet[*systemet*] (Equality Theory): a +small, parameterised type checker whose discipline you choose by choosing the +algebra at the resource layer. The wager it implements is one sentence — *do not +add a new type relation when a layer discipline will do.* + +[IMPORTANT] +==== +*Why "anytype" and not "EveryType".* This kernel was first drafted under the name +*EveryType*. That name over-claimed: it suggested a universal "every type" relation, +which is exactly the System-F~c~ trap this design refuses. The honest claim is the +opposite of universal coercion — pick *any* resource algebra you like, and the same +kernel gives you *that* discipline. Hence *anytype*. (See `AFFIRMATION.adoc` for the +no-overclaim posture.) -EveryType is the open-source kernel for **SystemET**: a five-layer, stratified type theory designed to avoid the **Coherence Cliff**. - -It is not a Haskell replacement. - -It is an experiment in a different bargain: - -> What if we make the totality cut at L1, keep equality as conversion, and refuse to pay the System Fc tax ever again? - -If that sounds like hand-waving, start with <>. That file maps the claims in this README to the actual implementation files, proof boundaries, caveats, and current evidence. - -== What this is - -EveryType is a small kernel for building disciplined type systems by changing the algebra at the resource layer. - -The core wager is: - -> Do not add a new type relation when a layer discipline will do. - -SystemET keeps one primitive relation at L1: - -## [source,text] - -## equality = normalize + compare - -Everything else is layered above it: - -[cols="1,2,3",options="header"] +[cols="1,3",options="header"] |=== -| Layer | Meaning | Status in EveryType - -| **L4 · effects `◇`** -| Effect handlers under erasure discipline -| *AMBER* — target: make `◇` statically erasable like `□` under TEA-purity - -| **L3 · recursion `▶`** -| Guarded recursion -| DONE - -| **L2 · resources `□`** -| Graded-modal substrate -| DONE — this is the main product - -| **L1 · equality** -| The totality cut: equality is conversion -| DONE — no Fc, no roles, no coercion language - -| **L0 · runtime** -| WASM/C target -| DONE +| Repository | Role +| `anytype` (this repo) | The kernel — the reference engine that implements Equality Theory. "Pick the algebra, get the discipline." +| link:https://github.com/hyperpolymath/systemet[`systemet`] | The theory — Equality Theory. Semantic authority: spec, invariants, proof obligations. +| AffineScript | One opinionated product profile of this kernel (`grade = affine + cost`). |=== +==== -EveryType is the kernel. - -SystemET is the theory. - -AffineScript is one product profile built from it. - -== The problem: the Coherence Cliff - -Modern type systems often grow by adding new relations on types. - -Examples: - -* Haskell: equality `a ~ b`, roles, and representational equality -* TypeScript: structural compatibility plus gradual escape hatches -* Rust: lifetimes, variance, ownership, trait solving, and region constraints - -Each new relation interacts with the others. - -Two features do not create two obligations. They create a square of interactions. - -Three features do not create three obligations. They create a grid. - -Eventually, the compiler is no longer merely checking programs. It is managing a treaty between equality, subtyping, variance, effects, resources, inference, and runtime casts. - -That is the **Coherence Cliff**. - -EveryType calls the failure mode the **anti-stack**: - -> features accrete sideways as new type relations instead of stacking vertically as disciplined layers. - -The anti-stack does not stratify. - -== The SystemET alternative - -System Fc puts a great deal of expressive pressure into equality. - -SystemET cuts earlier. - -At L1, type-level computation must terminate. Equality is conversion. There is no coercion language, no global role system, and no representational equality proof calculus. - -The expressive pressure moves upward into: - -* graded resources -* modalities -* finite state transitions -* guarded recursion -* effect erasure conditions - -The fork is simple: - -## [source,text] - -System Fc: equality becomes a proof-carrying subsystem. - -## SystemET: equality remains conversion; discipline moves into layers. - -== The three gates +== What this is -EveryType works by refusing three tempting collapses. +anytype is a kernel for *building disciplined type systems by changing the algebra at +the resource layer (L2)*, rather than by bolting on new type relations. It is the +*implementation* side of the split: -=== 1. The Totality Gate +* the *theory* — what the layers mean, which collapses are refused, and what must be + proven — lives in link:https://github.com/hyperpolymath/systemet[systemet]; +* the *engine* — the checker, the pluggable grade machinery, the runtime/ABI seam — + lives here. -At L1, type-level functions must terminate. +anytype *pins systemet upstream* and may *extend, not redefine* it. If implementation +pressure ever demands a change to the theory, that is an ADR in systemet, not a quiet +edit here. -That means equality is: +== The one mechanism that matters: pluggable grades -## [source,text] +The whole point of the kernel is that a new discipline is a one-line change of the L2 +grade algebra, checked by the *same* rules: -normalize -compare -done +[source,text] ---- - -No coercion language. - -No roles. - -No representational equality proof calculus. - -No “trust me, these two types are the same at runtime.” - -If a type-level function does not terminate, it does not belong at L1. - -See <>. - -=== 2. The Structural Gate - -At L2, EveryType admits **shallow structural subtyping** where it is just projection. - -That includes width-like behaviour for: - -* rows -* variants -* refinements -* record-like products - -The discipline is: - -## [source,text] - -CAR/CDR projection is allowed. -Deep co/contravariant rewriting is not. ---------------------------------------- - -Shallow structural access is projection from an additive product `&`. - -Deep variance is different. It pushes structure through function spaces, resources, effects, lifetimes, and linearity. That is where coherence starts to leak. - -So EveryType allows shallow CAR/CDR structure and refuses deep variance. - -See <>. - -=== 3. The Polarity Gate - -EveryType admits **polarized casts**, not true gradual typing. - -## [source,text] - -A -> ? forward, lossless, forgetful -? -| A backward, lossy, echo-graded ------------------------------------------- - -The forward direction is ordinary forgetting. - -The backward direction is not treated as a magical runtime check. It is marked with a blame grade: - -## [source,text] - -## !_{blame} - -That grade is part of the resource story. - -EveryType does not have a universal `any` that silently punches a hole through the type system. - -It has directed loss, explicit polarity, and graded blame. - -See <>. - -== What EveryType makes cheap - -EveryType is not mainly a syntax project. - -It is a kernel for generating disciplined type systems by changing the algebra at L2. - -=== 1. Invent a discipline in one line - -## [source,text] - grade = Affine grade = Cost * Nat -grade = Low <= High -grade = [0,1] +grade = Low <= High (an information-flow lattice) +grade = [0,1] (a probability-like grade) grade = PrivacyBudget grade = Latency x Billing -------------------------- - -Same checker. - -Different algebra. - -Different discipline. - -That is the point. - -See <>. - -=== 2. Zero-cost effects, when justified - -A handler that is: - -* **Total** -* **Effect-graded** -* **Affine** - -is a TEA handler. - -The goal of L4 is to prove when such handlers erase completely. - -This is not “effects are free.” - -It is: - -> effects erase only when the layer discipline proves they are observationally harmless. - -See <>. - -=== 3. Roles become tropes - -System Fc asks whether two types are representationally equal under a global role discipline. - -EveryType avoids that question. - -Instead of: - -## [source,text] - -x : A -coerce x : B ------------- - -EveryType uses finite state-indexed transitions: - -## [source,text] - -## A@t1 -> A@t2 -> A@t3 - -A trope is a local, finite, model-checkable transition machine. +---- -This moves the burden from global representational equality to explicit state movement. +A candidate grade is admissible only if it satisfies the laws the checker requires +(the relevant semiring/ordering operations). "Pick the algebra" is not "attach +arbitrary metadata". The *laws* a grade must satisfy are systemet's to define; the +*checking* against them is anytype's to perform. -No `coerce`. +== What the kernel implements (and how far) -No role inference. +These are the layers of Equality Theory as the *kernel* sees them. For what each layer +*means*, read link:https://github.com/hyperpolymath/systemet[systemet]; this table is +only the implementation status. -No hidden representational treaty. +[cols="1,2,2",options="header"] +|=== +| Layer | Kernel responsibility | Implementation status -See <>. +| *L4 · effects `◇`* +| Effect handlers; detect when a Total+Effect-graded+Affine (TEA) handler erases +| *not started* — depends on systemet's open TEA-erasure result -=== 4. Dependent types, rows, and refinements live together +| *L3 · recursion `▶`* +| Guarded recursion checking +| *not started* -Dependent types, rows, and refinements do not need to add new primitive relations. +| *L2 · resources `□`* +| The graded-modal substrate + the pluggable grade-algebra interface +| *design* — this is the kernel's centre of gravity -They live at L2 as structured uses of the graded substrate. +| *L1 · equality* +| Equality as `normalize` + `compare`; the totality check that makes it decidable +| *design* -That is the SystemET wager: +| *L0 · runtime* +| Lowering to a WASM/C target +| *not started* +|=== -> do not add a new relation when a layer discipline will do. +[WARNING] +==== +*Honesty check.* At this commit there is *no working kernel*. The `src/`, `tests/`, +and `verification/proofs/` trees are RSR *scaffolding* inherited from the template, +not a checker. This README states intent (where anytype is going); the engineering +state lives in `EXPLAINME.adoc` and the dated snapshot in `AFFIRMATION.adoc`. Do not +cite anytype as a usable type checker yet. +==== == Quick start -## [source,sh] - -# Build the kernel - -dune build @everytype - -# Run the test suite - -dune runtest - -# Validate the repository shape +[source,sh] +---- +# See the available repository tasks +just +# Validate the repository shape (this works today — it checks RSR structure) just validate -# See available repository tasks - -## just - -If this repository has just been created from the RSR template, run: - -## [source,sh] - -## just init - -That command replaces template placeholders, validates the result, and prepares the repository-specific metadata. +# Build / test the kernel (placeholder targets until the kernel exists) +just test +just quality +---- == Repository map @@ -324,225 +132,77 @@ That command replaces template placeholders, validates the result, and prepares |=== | Path | What lives there -| `0-AI-MANIFEST.a2ml` -| Universal entry point for AI agents. Read this before making changes. - -| `.machine_readable/` -| Project metadata, policies, contractiles, AI configs, 6A2 state, anchors, and machine-readable governance. - -| `src/` -| EveryType kernel implementation. - -| `src/interface/` -| Typed ABI/FFI seam where applicable: Idris2 interface descriptions, Zig FFI, and generated headers. - -| `docs/` -| Explanatory material, status notes, decisions, diagrams, and design records. - -| `EXPLAINME.adoc` -| Engineering deep-dive. Maps README claims to implementation files, caveats, and evidence boundaries. - -| `AFFIRMATION.adoc` -| Dated honesty snapshot of what the repository currently does and does not prove. - -| `AUDIT.adoc` -| Release audit gate. +| `0-AI-MANIFEST.a2ml` | Universal entry point for AI agents. Read this before making changes. +| `.machine_readable/` | Project metadata, policies, contractiles, AI configs, 6A2 state, anchors. +| `src/` | (Planned) anytype kernel implementation. +| `src/interface/` | Typed ABI/FFI seam: Idris2 interface descriptions, Zig FFI, generated headers. +| `verification/` | (Planned) proofs/tests that the kernel honours systemet's obligations. +| `docs/` | Status notes, decisions, diagrams, design records. +| `EXPLAINME.adoc` | Engineering deep-dive: how README claims map to files, caveats, evidence. +| `AFFIRMATION.adoc` | Dated honesty snapshot of what the kernel currently does and does not do. +| `AUDIT.adoc` | Release audit gate. +| `Justfile` | Task surface. Thin aliases delegate to the build/session machinery. +|=== -| `Justfile` -| Task surface. Thin command aliases delegate to the build/session machinery. +== anytype vs the world -| `.github/` -| CI, security workflows, community health files, and repository automation. +The interesting comparison is *the theory* — see systemet's README for the full +table. As an *engine*, anytype's distinguishing bet is that the discipline is a +parameter (the L2 grade algebra), not a fixed feature set: -| `tests/` -| Kernel tests, examples, and regression checks. +[cols="1,2,2,2",options="header"] |=== +| | anytype | Haskell / System Fc | Rust -== EveryType vs the world +| *Discipline source* +| *pluggable L2 grade algebra* +| fixed relation set (equality evidence, roles) +| fixed (ownership, lifetimes, variance) -[cols="1,2,2,2,2,2",options="header"] -|=== -| | EveryType | Haskell / System Fc | Idris2 | Rust | TypeScript - -| **L1 equality** -| conversion -| coercion proofs / equality evidence -| conversion -| trait and region solving -| structural compatibility - -| **Coercions** -| **NO** -| **YES** -| mostly no at the core -| lifetime and representation-sensitive coercions -| casts and escape hatches - -| **L2 resources** -| **pluggable semiring** -| limited / plugin-dependent -| quantity discipline `0,1,ω` -| affine ownership -| none - -| **Roles** -| **tropes `A@t`** +| *Coercions* +| *none* (equality is conversion) +| *yes* +| representation/lifetime-sensitive + +| *Roles* +| *tropes `A@t`* (local finite machines) | global role system -| none | lifetime / variance discipline -| none - -| **Deep variance** -| **REFUSED** -| controlled but external to ET’s wager -| limited -| **YES** -| **YES, often unsound around mutation/callbacks** - -| **Effects erase** -| TEA-purity target -| no general erasure theorem -| no general erasure theorem -| no general erasure theorem -| no |=== -== Status - -The current repository status is intentionally split between this README and the evidence files. - -Current implementation target: - -* `v0.1` - ** L0-L3 kernel in OCaml - ** QTT-style core - ** pluggable semiring grades - ** totality checker using sized types - ** guarded recursion `▶` - -* `v0.2` - ** tropes prototype - ** split/rejoin discipline for handles +== Relationship to systemet and AffineScript -* `OPEN-A` - ** formal TEA-purity proof - -For the current evidence boundary, see: - -* <> -* <> -* <> +* link:https://github.com/hyperpolymath/systemet[*systemet*] is the *theory* anytype + implements; it is the semantic authority. anytype must not silently diverge from it. +* *AffineScript* is one *product profile* of this kernel (`grade = affine + cost`), + aimed at WASM contracts and edge functions. It is downstream of anytype. == RSR integration -This repository uses the Rhodium Standard Repository pattern. - -That means it includes: - -* machine-readable metadata under `.machine_readable/` -* AI-agent entry protocol through `0-AI-MANIFEST.a2ml` -* repository validation through `just validate` -* session command dispatch through `session/dispatch.sh` -* governance and release gates -* CI/CD and security workflows -* SPDX-based licensing - -The RSR machinery is integration infrastructure. It is not part of the EveryType kernel. - -See <> for the claim-to-file mapping. - -== Session protocol authority - -Session protocols are centrally maintained and not duplicated in this repository. - -Local files are integration-only: - -* `session/dispatch.sh` -* `session/custom-checks.k9` -* `session/local-hooks.sh` -* `coordination.k9` - -The dispatcher maps canonical commands to central protocol paths in `standards/session-management-standards`. - -If `SESSION_STANDARDS_DIR` is unset and no adjacent standards checkout exists, the dispatcher records the command but cannot resolve central checklist paths. - -== Dependency updates - -Dependabot watches the supported ecosystems used by the estate: - -* GitHub Actions -* Cargo -* Mix / Elixir -* Docker - -Automated merges are allowed only after required checks pass. - -A broken bump fails CI and stays open. It does not land on a red main. - -Dependabot does not support Deno or Bun ecosystems directly. For Deno-first repositories, dependency currency is managed through `deno.json` and `deno.lock`, not Dependabot. - -Do not add Dependabot as a ruleset bypass actor. That would allow dependency bumps to skip required safety checks such as secret scanning and SAST. - -== What is AffineScript? - -AffineScript is one profile of EveryType: - -## [source,text] - -## grade = affine + cost - -AffineScript is the product language for WASM contracts and edge functions. - -EveryType is the kernel. - -SystemET is the theory. - -AffineScript is the opinionated deployment. +This repository uses the Rhodium Standard Repository pattern: machine-readable +metadata under `.machine_readable/`, the `0-AI-MANIFEST.a2ml` agent entry point, +`just validate` for repository shape, governance and release gates, and SPDX-based +licensing. *The RSR machinery is repository infrastructure — it is not part of the +anytype kernel, and passing RSR validation proves nothing about the kernel's +correctness.* See `EXPLAINME.adoc#_rsr_integration`. == Contributing -We are not currently looking for syntax bikeshedding. - -Useful contributions include: - -* new L2 semirings: - ** security lattices - ** differential privacy budgets - ** latency / cost models - ** information-flow grades - -* proofs: - ** TEA erasure - ** trope preservation - ** shallow structural soundness - ** guarded recursion interaction with grades - -* finite trope machines for real APIs: - ** file handles - ** sockets - ** database transactions - ** web streams - ** WASM capabilities +Most of the deep work is *theory and proof* and belongs in +link:https://github.com/hyperpolymath/systemet[systemet]. Engine-side contributions +that belong here: -Open issues with one of: +* the L2 grade-algebra interface and concrete grade instances (affine, cost, + information-flow lattice, privacy budget) *that satisfy systemet's laws*; +* the L1 conversion checker and its totality gate; +* the typed ABI/FFI seam (`src/interface/`). -## [source,text] - -[ET-L2] -[ET-L3] -[ET-L4] -[TROPE] -[TEA] ------ +Open issues with one of: `[ET-L2]`, `[ET-L3]`, `[ET-L4]`, `[TROPE]`, `[TEA]`. == Licence -Code, configuration, and scripts are licensed under the Mozilla Public License 2.0. - -Prose documentation is licensed under CC-BY-SA-4.0. - -Per-file `SPDX-License-Identifier` headers are authoritative. - -The GitHub-detected licence is MPL-2.0 through the root `LICENSE`. - -Long-term attribution uses Quantum-Safe Provenance. See PMPL Exhibit B where present. +Code, configuration, and scripts are licensed under the Mozilla Public License 2.0 +(`MPL-2.0`); prose documentation under `CC-BY-SA-4.0`. Per-file +`SPDX-License-Identifier` headers are authoritative; the GitHub-detected licence is +MPL-2.0 via the root `LICENSE`. Long-term attribution uses Quantum-Safe Provenance +(PMPL Exhibit B where present).