Skip to content

EXPLAINME.adoc

Latest commit

 

History

History
190 lines (135 loc) · 7.56 KB

EXPLAINME.adoc

File metadata and controls

190 lines (135 loc) · 7.56 KB
Raw

anytype — EXPLAINME

Table of Contents

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.

Important

Boundary. anytype is the kernel (implementation). The theory it implements — the meaning of the layers, the gates, and the proof obligations — lives in systemet. Claims about what the theory says belong in systemet’s EXPLAINME.adoc; claims here are about code and its current state.

1. Current state (read this first)

Claim: anytype is the reference kernel for Equality Theory.

Reality at this commit (2026-07-21, MVP kernel):

  • The kernel exists for the MVP cut: src/kernel/ is a usage-counting bidirectional checker for a simply-graded λ-calculus, parameterised by a GradeAlgebra record whose ordered-semiring laws are proof fields. Two instances ship — affine {0,1,ω} (mirroring AffineScript lib/quantity.ml) and exact-usage ℕ — and the 19-case golden matrix shows the same rules yielding distinct disciplines (affine accepts drop, exact rejects it).

  • The seam is anytype’s own: src/interface/Abi/ (wire types with injective codes; layouts proven CABICompliant), the anytype-check CLI (src/cli/), and the Zig anytype_check export (src/interface/ffi/) with comptime asserts against the proven layouts. MVP transport is a spawned process; in-process RefC linkage is future work.

  • Gates are real and hard-fail: just test, just proof-check-idris2 (manifest over every .idr; missing prover = FAIL), and CI idris2-proof.yml. Five never-compiling template modules under verification/proofs/idris2/ are quarantined, not hidden.

  • Not built: dependent types, branching (needs a grade join beyond the stated laws), L3 recursion, L0 lowering, L4 effects (TEA is open in systemet), and any soundness proof for the checker itself.

The dated snapshot is AFFIRMATION.adoc.

2. Pluggable grades (the L2 mechanism)

Claim: a new discipline is a change of the L2 grade algebra, not a change of checker.

Intended implementation:

  • 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.

Division of responsibility:

  • systemet defines the laws a grade algebra must satisfy.

  • anytype implements the interface and checks candidates against those laws.

State:

  • Built (MVP): src/kernel/Anytype/Grade/Algebra.idr is the interface — a record whose law fields make an unlawful algebra unrepresentable. Affine.idr and Exact.idr are the first two instances. The richer grades (cost, information-flow lattice, probability-like, privacy budget) remain future instances; branching additionally needs a join operation the record does not yet carry.

3. L1 equality and the totality gate

Claim: equality is normalize then compare, with no coercion language, made decidable by a totality check on type-level computation.

Intended implementation:

  • A normaliser + structural comparison for the conversion relation.

  • A totality checker that rejects non-terminating type-level functions, so conversion terminates.

State and caveat:

  • Built (MVP): Anytype.Core.Normalise + Anytype.Core.Conversion, invoked at the single check/infer mode switch in Anytype.Core.Check. The MVP totality gate is syntactic: the type-index language (TNat) has no recursion constructor, and the normaliser is %default total — machine-checked, but a gate by construction, not a termination analysis over a type-level function space (there is no type-level function space yet).

  • The strength of "equality is conversion" is exactly the strength of the totality gate. Any escape hatch must be recorded as an explicit unsafe boundary in AFFIRMATION.adoc, never folded silently into equality. The theorem that this is sound is systemet’s obligation; this repo only has to implement the check.

4. Structural and polarity gates

Claim: shallow CAR/CDR projection is admitted; deep variance is refused. Casts are polarized (A → ? lossless, ? -| A blame-graded); there is no universal any.

Intended implementation:

  • Projection from additive products &; refusal of deep co/contravariant rewriting.

  • A blame grade !_{blame} carried as part of L2 accounting on backward casts.

Caveat:

  • These are design boundaries the kernel must enforce; the justification for why they avoid the Coherence Cliff is systemet’s, not this repo’s.

5. Roles to tropes

Claim: global roles/coercions are replaced by local finite trope machines A@t1 → A@t2 → A@t3.

Intended implementation:

  • A representation of finite, model-checkable transition machines.

  • Per-API machines (file handles, sockets, transactions, streams, WASM capabilities).

Caveat:

  • The preservation result is systemet’s proof obligation. anytype implements the machines and the runtime check; it does not, by existing, prove them sound.

6. TEA erasure (L4)

Claim: a Total + Effect-graded + Affine handler should erase completely.

Reality:

  • 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.

7. Typed ABI/FFI seam

Claim: anytype has a formally-typed ABI/FFI seam.

How this is implemented:

  • src/interface/Abi/ holds Idris2 interface/layout descriptions; src/interface/ffi/ holds the Zig FFI; src/interface/generated/ is where generated C headers land.

State:

  • Built (MVP): Abi.Types (discipline/verdict codes, injectivity + round-trip proofs), Abi.Layout (anytype_request_t/anytype_response_t proven CABICompliant), Abi.Foreign (the anytype_check contract), and the Zig side comptime-asserting the same layouts. Transport is a spawned anytype-check process; src/interface/generated/ C headers and in-process linkage are future work.

8. RSR integration

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 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:

  • 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.

9. Dependency updates

Claim: dependency bumps land fast and safely.

How this is implemented:

  • 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.

10. Licence

  • 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.