diff --git a/.github/workflows/idris2-proof.yml b/.github/workflows/idris2-proof.yml new file mode 100644 index 0000000..bd99a37 --- /dev/null +++ b/.github/workflows/idris2-proof.yml @@ -0,0 +1,113 @@ +# SPDX-License-Identifier: MPL-2.0 +# Idris2 proof + kernel test gate — type-checks EVERY Idris2 module via +# scripts/check-idris2-proofs.sh (the same script `just proof-check-idris2` +# runs, so local green and CI green mean the same thing), then builds the +# kernel and runs the golden matrix (the same pipeline as `just test`). +# +# This is the first workflow in this repository that checks any Idris2 at +# all: the other workflows validate repo shape and run security scanners, +# and the recipe this gate replaces (build/just/proofs.just) exited 0 when +# the prover was absent. The script fails when idris2 is missing rather +# than skipping, so a broken install step can never render as a green +# proof run. +# +# Adapted from ideas-to-alphas .github/workflows/idris2-proof.yml, which +# documents the estate history behind each rule. +name: Idris2 Proof + +on: + push: + branches: [main] + paths: + - '**.idr' + - '*.ipkg' + - 'scripts/check-idris2-proofs.sh' + - 'scripts/check-cli.sh' + - 'src/interface/ffi/**' + - '.github/workflows/idris2-proof.yml' + pull_request: + paths: + - '**.idr' + - '*.ipkg' + - 'scripts/check-idris2-proofs.sh' + - 'scripts/check-cli.sh' + - 'src/interface/ffi/**' + - '.github/workflows/idris2-proof.yml' + workflow_dispatch: + +# Estate guardrail: one run per ref, cancel superseded runs. Read-only check. +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +permissions: + contents: read + +env: + IDRIS2_VERSION: "0.7.0" + +jobs: + idris2-check: + runs-on: ubuntu-latest + timeout-minutes: 30 + permissions: + contents: read + steps: + - name: Checkout + uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + + - name: Install Chez Scheme (Idris2 backend) + run: | + set -euo pipefail + sudo apt-get update -qq + sudo apt-get install -y --no-install-recommends chezscheme libgmp-dev + + - name: Build & install Idris2 ${{ env.IDRIS2_VERSION }} + run: | + set -euo pipefail + # Build OUTSIDE the checkout. The proof gate sweeps the working tree + # for every *.idr and errors on any not in its manifest -- that + # breadth is the point. The Idris2 source tarball ships hundreds of + # .idr files; extracting it into the checkout makes the gate fail on + # the compiler's own sources. Keep the tree the gate scans clean. + build_dir="$(mktemp -d)" + cd "$build_dir" + tarball="idris2-${IDRIS2_VERSION}.tar.gz" + curl -fsSL -o "$tarball" \ + "https://codeload.github.com/idris-lang/Idris2/tar.gz/refs/tags/v${IDRIS2_VERSION}" + tar xzf "$tarball" + cd "Idris2-${IDRIS2_VERSION}" + make bootstrap SCHEME=chezscheme + make install SCHEME=chezscheme + echo "${HOME}/.idris2/bin" >> "$GITHUB_PATH" + + - name: Build kernel, run golden matrix and seam tests + # Runs first so the anytype/anytype-abi packages are installed before + # the proof sweep checks modules that use -p flags. + run: | + set -euo pipefail + idris2 --install anytype.ipkg + idris2 --install abi.ipkg + idris2 --build anytype-tests.ipkg + ./build/exec/anytype-tests + idris2 --build anytype-cli.ipkg + ./scripts/check-cli.sh + + - name: Type-check every Idris2 module + run: ./scripts/check-idris2-proofs.sh + + - name: Install Zig 0.16.0 (checksum-pinned) + run: | + set -euo pipefail + cd "$(mktemp -d)" + curl -fsSL -o zig.tar.xz \ + "https://ziglang.org/download/0.16.0/zig-x86_64-linux-0.16.0.tar.xz" + echo "70e49664a74374b48b51e6f3fdfbf437f6395d42509050588bd49abe52ba3d00 zig.tar.xz" | sha256sum -c - + tar xJf zig.tar.xz + echo "$PWD/zig-x86_64-linux-0.16.0" >> "$GITHUB_PATH" + + - name: Zig seam tests (comptime layout asserts + kernel round trip) + run: | + set -euo pipefail + cd src/interface/ffi + zig build test --summary all diff --git a/.gitignore b/.gitignore index ccf874b..998a123 100644 --- a/.gitignore +++ b/.gitignore @@ -109,17 +109,10 @@ deps/ build/ dist/ -# /build/ is a tracked config directory (build orchestration: contractile.just, -# guix.scm, just/*.just, etc.) introduced in chore/root-cleanup. Whitelist -# root-level /build/ so its contents are tracked. The blanket `build/` rule -# above still ignores any nested `build/` directories (e.g. Rust crate -# target/build/) — only the root-level path is exempt. -!/build/ -!/build/** - -# ...but never track Idris2 typecheck output. `idris2 --typecheck abi.ipkg` -# writes compiled .ttc/.ttm under build/ttc/; these are generated artifacts. -/build/ttc/ +# build/ is generated output only (Idris2 .ttc/.ttm and executables, Zig +# artifacts). The old tracked build/ config directory (contractile.just, +# guix.scm, just/*.just) was removed with the fake-gate recipes; nothing +# under build/ is source any more. # Arrival-pack build artifact (regenerated from a2ml) .machine_readable/arrival-pack/claude-md-data.json diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 475a1cc..6ea61a1 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -6,25 +6,25 @@ [metadata] project = "anytype" version = "0.1.0" -last-updated = "2026-06-28" +last-updated = "2026-07-21" status = "active" # active | paused | archived [project-context] name = "anytype" purpose = "Reference kernel for systemet (Equality Theory): a parameterised checker whose discipline is the chosen L2 grade algebra. Implementation side of the systemet/anytype split." -completion-percentage = 10 +completion-percentage = 40 [position] -phase = "design" # design | implementation | testing | maintenance | archived +phase = "implementation" # design | implementation | testing | maintenance | archived maturity = "experimental" # experimental | alpha | beta | production | lts [route-to-mvp] milestones = [ { name = "Phase 0: Split kernel out of the EveryType draft; instantiate RSR repo", completion = 100 }, { name = "Phase 1: Design write-up (pluggable grades, L1 conversion, gates)", completion = 80 }, - { name = "Phase 2: L2 grade-algebra interface + first concrete grade (affine)", completion = 0 }, - { name = "Phase 3: L1 conversion checker + totality gate", completion = 0 }, - { name = "Phase 4: anytype-specific typed ABI/FFI seam (replace template seam)", completion = 0 }, + { name = "Phase 2: L2 grade-algebra interface + first concrete grade (affine)", completion = 100 }, + { name = "Phase 3: L1 conversion checker + totality gate", completion = 100 }, + { name = "Phase 4: anytype-specific typed ABI/FFI seam (replace template seam)", completion = 100 }, { name = "Phase 5: L3 guarded recursion; L0 lowering target", completion = 0 }, { name = "Phase 6: L4 effect handlers + TEA-erasure (gated on systemet OPEN-A)", completion = 0 }, ] @@ -34,10 +34,11 @@ milestones = [ [critical-next-actions] actions = [ - "Define the L2 grade-algebra interface against systemet's stated laws.", - "Implement the L1 conversion checker (normalize + compare) and the totality gate.", - "Replace the template ABI/FFI seam with an anytype-specific one.", - "Keep README/EXPLAINME inside what is built; no 'usable checker' claim until it exists.", + "Add branching to L1: needs a join (least upper bound) on grades beyond the semiring+order laws -- design the extension against systemet first.", + "L3 guarded recursion (Phase 5), then L0 lowering target.", + "In-process seam: link the kernel via the RefC backend instead of spawning anytype-check.", + "Decide the fate of the five quarantined RSR template proof modules (fix or delete; tracked in scripts/check-idris2-proofs.sh MANIFEST).", + "Keep README/EXPLAINME inside what is built; the MVP claim is 'distinct disciplines from one rule set', not 'usable general-purpose checker'.", ] [maintenance-status] diff --git a/.machine_readable/6a2/anchors/ANCHOR.a2ml b/.machine_readable/6a2/anchors/ANCHOR.a2ml index 77347a9..65bd644 100644 --- a/.machine_readable/6a2/anchors/ANCHOR.a2ml +++ b/.machine_readable/6a2/anchors/ANCHOR.a2ml @@ -29,6 +29,9 @@ domain = "programming-language implementation / type checkers" semantic-authority = "hyperpolymath/systemet" relationship = "implements" pin-required = true +# Discharged 2026-07-21: the systemet commit this kernel implements. +pinned-commit = "ba5930dc478c80b1f968eea4ca28acd0f9d67966" +pinned-date = "2026-07-18" extend-not-redefine = true [semantic-authority] diff --git a/.tool-versions b/.tool-versions index ce60c32..968684a 100644 --- a/.tool-versions +++ b/.tool-versions @@ -1,10 +1,3 @@ -# Uncomment and customize for your project -# rust nightly -# just 1.40.0 -# nickel 1.10.0 -# gleam 1.8.0 -# elixir 1.18.0 -# erlang 27.2 -# zig 0.14.0 -# idris2 0.7.0 rust nightly +idris2 0.7.0 +zig 0.16.0 diff --git a/AFFIRMATION.adoc b/AFFIRMATION.adoc index 83af40a..df145e5 100644 --- a/AFFIRMATION.adoc +++ b/AFFIRMATION.adoc @@ -35,14 +35,17 @@ file is a draft. == What we do NOT claim -* *There is no working type checker yet.* `src/`, `tests/`, and `verification/proofs/` - are RSR *scaffolding* inherited from the template, not an anytype implementation. -* *The pluggable-grade interface does not exist in code yet.* It is the first build - target, not a shipped feature. -* *No layer is implemented.* The L0–L4 table in the README is intent + status, not a - record of working code. +* *The kernel is an MVP cut, not a general-purpose type checker.* No dependent + types, no branching, no L3 recursion, no L0 lowering, no L4 effects. +* *No soundness proof for the checker.* The grade-algebra laws are machine-checked + proof fields and the golden matrix is real, but progress/preservation for the + L1 checker is not proven. +* *The totality gate is syntactic* (no recursion constructor in the type-index + language), not a termination analysis. * *TEA-erasure is OPEN* (in systemet) and not started here. Do not cite it. -* *The ABI/FFI seam files are the template's*, not yet an anytype-specific ABI. +* *The seam transport is a spawned process*, not in-process linkage; five + never-compiling template proof modules are quarantined in + `scripts/check-idris2-proofs.sh`, not fixed. == Provenance note diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index d80430a..7a18652 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -23,18 +23,28 @@ its current state*. Claim: anytype is the reference kernel for Equality Theory. -Reality at this commit: - -* There is *no working checker yet*. `src/` contains RSR scaffolding - (`src/interface/Abi/*.idr`, `src/interface/ffi/*.zig`, READMEs, AI-manifests), not - an anytype implementation. -* `tests/` and `verification/proofs/` are template stubs, not anytype tests/proofs. -* What is real today: the repository *shape* (RSR), the *design* of the kernel in - this file and the README, and the *split* that makes systemet the theory and - anytype the engine. - -Everything below describes the *intended* mapping. Where a file does not yet exist or -is a stub, it is named as such. The dated, signed snapshot is `AFFIRMATION.adoc`. +Reality at this commit (2026-07-21, MVP kernel): + +* The kernel *exists for the MVP cut*: `src/kernel/` is a usage-counting + bidirectional checker for a simply-graded λ-calculus, parameterised by a + `GradeAlgebra` record whose ordered-semiring laws are proof fields. Two + instances ship — affine `{0,1,ω}` (mirroring AffineScript `lib/quantity.ml`) + and exact-usage `ℕ` — and the 19-case golden matrix shows the same rules + yielding distinct disciplines (affine accepts drop, exact rejects it). +* The seam is anytype's own: `src/interface/Abi/` (wire types with injective + codes; layouts proven `CABICompliant`), the `anytype-check` CLI + (`src/cli/`), and the Zig `anytype_check` export (`src/interface/ffi/`) + with comptime asserts against the proven layouts. MVP transport is a + spawned process; in-process RefC linkage is future work. +* Gates are real and hard-fail: `just test`, `just proof-check-idris2` + (manifest over every `.idr`; missing prover = FAIL), and CI + `idris2-proof.yml`. Five never-compiling template modules under + `verification/proofs/idris2/` are quarantined, not hidden. +* Not built: dependent types, branching (needs a grade join beyond the + stated laws), L3 recursion, L0 lowering, L4 effects (TEA is open in + systemet), and any soundness proof for the checker itself. + +The dated snapshot is `AFFIRMATION.adoc`. == Pluggable grades (the L2 mechanism) @@ -52,9 +62,14 @@ Division of responsibility: * systemet *defines the laws* a grade algebra must satisfy. * anytype *implements the interface and checks candidates against those laws*. -Caveat: +State: -* None of this interface exists in code yet. It is the kernel's first build target. +* Built (MVP): `src/kernel/Anytype/Grade/Algebra.idr` is the interface — a record + whose law fields make an unlawful algebra unrepresentable. `Affine.idr` and + `Exact.idr` are the first two instances. The richer grades (cost, + information-flow lattice, probability-like, privacy budget) remain future + instances; branching additionally needs a join operation the record does not + yet carry. == L1 equality and the totality gate @@ -67,10 +82,16 @@ Intended implementation: * A totality checker that rejects non-terminating type-level functions, so conversion terminates. -Caveat: +State and caveat: +* Built (MVP): `Anytype.Core.Normalise` + `Anytype.Core.Conversion`, invoked at the + single check/infer mode switch in `Anytype.Core.Check`. The MVP totality gate is + *syntactic*: the type-index language (`TNat`) has no recursion constructor, and the + normaliser is `%default total` — machine-checked, but a gate by construction, not a + termination analysis over a type-level function space (there is no type-level + function space yet). * The strength of "equality is conversion" is exactly the strength of the totality - checker. Any escape hatch must be recorded as an explicit unsafe boundary in + gate. Any escape hatch must be recorded as an explicit unsafe boundary in `AFFIRMATION.adoc`, never folded silently into equality. The *theorem* that this is sound is systemet's obligation; this repo only has to *implement the check*. @@ -123,10 +144,14 @@ How this is implemented: * `src/interface/Abi/` holds Idris2 interface/layout descriptions; `src/interface/ffi/` holds the Zig FFI; `src/interface/generated/` is where generated C headers land. -Caveat: +State: -* These are currently the *template's* seam files, not anytype-specific ones. They - demonstrate the pattern; they do not yet describe an anytype ABI. +* Built (MVP): `Abi.Types` (discipline/verdict codes, injectivity + round-trip + proofs), `Abi.Layout` (`anytype_request_t`/`anytype_response_t` proven + `CABICompliant`), `Abi.Foreign` (the `anytype_check` contract), and the Zig side + comptime-asserting the same layouts. Transport is a spawned `anytype-check` + process; `src/interface/generated/` C headers and in-process linkage are future + work. == RSR integration diff --git a/Justfile b/Justfile index c6c157e..c737dc4 100644 --- a/Justfile +++ b/Justfile @@ -129,26 +129,29 @@ clean-all: clean # TEST & QUALITY # ═══════════════════════════════════════════════════════════════════════════════ -# Run all tests +# Hard-fails if idris2 is absent -- a gate that cannot fail is not a gate +# (see scripts/check-idris2-proofs.sh for the history). +# Typecheck the ABI seam, build the kernel, run the golden matrix test *args: - @echo "Running tests..." - # TODO: Replace with your test command - # Examples: - # cargo test {{args}} - # mix test {{args}} - # zig build test {{args}} - # deno test {{args}} - @echo "Tests passed!" + @command -v idris2 >/dev/null || { echo "FAIL: idris2 not on PATH (install Idris2 0.7.0)"; exit 1; } + idris2 --install anytype.ipkg + idris2 --install abi.ipkg + idris2 --build anytype-tests.ipkg + ./build/exec/anytype-tests + idris2 --build anytype-cli.ipkg + ./scripts/check-cli.sh + @command -v zig >/dev/null || { echo "FAIL: zig not on PATH (Zig seam tests need it)"; exit 1; } + cd src/interface/ffi && zig build test # Run tests with verbose output test-verbose: @echo "Running tests (verbose)..." # TODO: Replace with verbose test command -# Smoke test +# Smoke test: does the kernel package typecheck at all? test-smoke: - @echo "Smoke test..." - # TODO: Add basic sanity checks + @command -v idris2 >/dev/null || { echo "FAIL: idris2 not on PATH"; exit 1; } + idris2 --typecheck anytype.ipkg # Run end-to-end tests (full pipeline: build → run → verify) e2e: @@ -593,7 +596,14 @@ help-me: # FORMAL VERIFICATION (PROOFS) — see build/just/proofs.just # ═══════════════════════════════════════════════════════════════════════════════ -import? "build/just/proofs.just" +# Proof gates replace the deleted build/just/proofs.just, whose recipes +# exited 0 when the prover was absent (the estate fake-gate flaw). +# Type-check every Idris2 module against the MANIFEST (hard-fail gate) +proof-check-idris2: + ./scripts/check-idris2-proofs.sh + +# Run all proof gates +proof-check: proof-check-idris2 # ═══════════════════════════════════════════════════════════════════════════════ # SESSION MANAGEMENT (THIN BINDINGS TO CENTRAL STANDARDS) diff --git a/README.adoc b/README.adoc index 72296ca..f0e776f 100644 --- a/README.adoc +++ b/README.adoc @@ -91,11 +91,17 @@ only the implementation status. | *L2 · resources `□`* | The graded-modal substrate + the pluggable grade-algebra interface -| *design* — this is the kernel's centre of gravity +| *built (MVP)* — `Anytype.Grade.Algebra` is an ordered-semiring record whose laws +are proof fields; instances exist for affine `{0,1,ω}` (AffineScript's discipline) +and exact-usage `ℕ`. Same rules, distinct disciplines — demonstrated in the golden +matrix. | *L1 · equality* | Equality as `normalize` + `compare`; the totality check that makes it decidable -| *design* +| *built (MVP cut)* — a bidirectional simply-graded λ-calculus whose type-index +language has no recursion constructor, so type-level computation is total *by +construction* (a syntactic gate, machine-checked via `%default total`, not a +termination analysis). Conversion is normalise-and-compare at one site. | *L0 · runtime* | Lowering to a WASM/C target @@ -104,11 +110,19 @@ only the implementation status. [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. +*Honesty check.* At this commit the kernel exists *for the MVP cut only*: +a simply-graded λ-calculus (`src/kernel/`) with pluggable grade algebras, a +process-boundary seam (`anytype-check` + the Zig `anytype_check` export), and +real gates (`just test`, `just proof-check-idris2`, CI `idris2-proof.yml`). +What it is *not* yet: no dependent types, no branching (`if` needs a grade +join beyond the stated semiring+order laws), no L3 guarded recursion, no L0 +lowering, no L4 effects (gated on systemet's open TEA-erasure result), and +the seam transport is a spawned process, not in-process linkage. Five RSR +template modules under `verification/proofs/idris2/` never compiled and are +quarantined in `scripts/check-idris2-proofs.sh` rather than deleted. Do not +cite anytype as a general-purpose type checker; cite it as a working +demonstration that one set of rules yields distinct disciplines by choosing +the algebra. ==== == Quick start diff --git a/abi.ipkg b/abi.ipkg index 4b62c0b..66f55d8 100644 --- a/abi.ipkg +++ b/abi.ipkg @@ -19,7 +19,7 @@ -- The RSR validators accept either Abi/ (canonical, case-consistent) or a -- lowercase abi/ for downstream repos that ship lowercase — but never both. -package abi +package anytype-abi version = 0.1.0 diff --git a/anytype-cli.ipkg b/anytype-cli.ipkg new file mode 100644 index 0000000..d30b603 --- /dev/null +++ b/anytype-cli.ipkg @@ -0,0 +1,13 @@ +package anytype-cli +version = 0.1.0 +authors = "hyperpolymath" +license = "MPL-2.0" +brief = "anytype-check: process-boundary entry point for the kernel" + +sourcedir = "src/cli" +depends = base, anytype, anytype-abi + +modules = Anytype.Sexp + , Anytype.Main +main = Anytype.Main +executable = anytype-check diff --git a/anytype-tests.ipkg b/anytype-tests.ipkg new file mode 100644 index 0000000..54e86d2 --- /dev/null +++ b/anytype-tests.ipkg @@ -0,0 +1,12 @@ +package anytype-tests +version = 0.1.0 +authors = "hyperpolymath" +license = "MPL-2.0" +brief = "Golden matrix for the anytype kernel" + +sourcedir = "verification/tests/kernel" +depends = base, anytype + +modules = Tests.Main +main = Tests.Main +executable = anytype-tests diff --git a/anytype.ipkg b/anytype.ipkg new file mode 100644 index 0000000..df90e63 --- /dev/null +++ b/anytype.ipkg @@ -0,0 +1,20 @@ +-- anytype kernel package. +-- Module namespace matches the physical path under src/kernel exactly +-- (case-sensitive on every filesystem) — see abi.ipkg for the lesson. +package anytype +version = 0.1.0 +authors = "hyperpolymath" +license = "MPL-2.0" +brief = "Parameterised graded type checker: pick the algebra, get the discipline" + +sourcedir = "src/kernel" +depends = base + +modules = Anytype.Grade.Algebra + , Anytype.Grade.Affine + , Anytype.Grade.Exact + , Anytype.Core.Syntax + , Anytype.Core.Normalise + , Anytype.Core.Conversion + , Anytype.Core.Check + , Anytype.Kernel diff --git a/build/.guix-channel b/build/.guix-channel deleted file mode 100644 index 3a51e72..0000000 --- a/build/.guix-channel +++ /dev/null @@ -1,22 +0,0 @@ -;; SPDX-License-Identifier: MPL-2.0 -;; Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -;; -;; Guix channel definition for anytype -;; -;; To use this channel, add to ~/.config/guix/channels.scm: -;; -;; (channel -;; (name 'anytype) -;; (url "https://github.com/hyperpolymath/anytype") -;; (branch "main")) -;; -;; Then: guix pull - -(channel - (version 0) - (url "https://github.com/hyperpolymath/anytype") - (dependencies - (channel - (name 'guix) - (url "https://git.savannah.gnu.org/git/guix.git") - (branch "master")))) diff --git a/build/contractile.just b/build/contractile.just deleted file mode 100644 index 9a5827b..0000000 --- a/build/contractile.just +++ /dev/null @@ -1,75 +0,0 @@ -# Auto-generated by: contractile gen-just -# Source directory: contractiles -# Re-generate with: contractile gen-just --dir contractiles -# -# SPDX-License-Identifier: MPL-2.0 - -# === DUST (Recovery & Rollback) === -# Source: Dustfile.a2ml - -# List available dust recovery actions -dust-status: - @echo ' dust-source-rollback: Revert all source changes to last commit [rollback]' - -# Revert all source changes to last commit -dust-source-rollback: - @echo 'Executing rollback for source-rollback' - git checkout HEAD -- . - - -# === INTEND (Declared Future Intent) === -# Source: Intentfile.a2ml - -# Display declared future intents -intend-list: - @echo '=== Declared Intent ===' - @echo '' - @echo 'Features:' - @echo '' - @echo 'Quality:' - - -# === MUST (Physical State Checks) === -# Source: Mustfile.a2ml - -# Run all must checks -must-check: must-license-present must-readme-present must-spdx-headers must-no-banned-files - @echo 'All must checks passed' - -# LICENSE file must exist -must-license-present: - test -f LICENSE - -# README must exist -must-readme-present: - test -f README.adoc || test -f README.md - -# Source files should have SPDX license headers -must-spdx-headers: - find . -name '*.rs' -o -name '*.res' -o -name '*.gleam' | head -20 | xargs -r grep -L 'SPDX-License-Identifier' | wc -l | grep -q '^0$' - -# No Dockerfiles or Makefiles -must-no-banned-files: - test ! -f Dockerfile && test ! -f Makefile - - -# === TRUST (Integrity & Provenance Verification) === -# Source: Trustfile.a2ml - -# Run all trust verifications -trust-verify: trust-license-content trust-no-secrets-committed trust-container-images-pinned - @echo 'All trust verifications passed' - -# LICENSE contains expected SPDX identifier -trust-license-content: - grep -q 'SPDX\|License\|MIT\|Apache\|PMPL\|MPL' LICENSE - -# No .env or credential files in repo -trust-no-secrets-committed: - test ! -f .env && test ! -f credentials.json && test ! -f .env.local - -# Containerfile base images use pinned digests -trust-container-images-pinned: - test ! -f Containerfile || grep -q '@sha256:' Containerfile - - diff --git a/build/guix.scm b/build/guix.scm deleted file mode 100644 index cc0ab49..0000000 --- a/build/guix.scm +++ /dev/null @@ -1,71 +0,0 @@ -;; SPDX-License-Identifier: MPL-2.0 -;; Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -;; -;; Guix package definition for anytype -;; -;; Usage: -;; guix shell -D -f guix.scm # Enter development shell -;; guix build -f guix.scm # Build package -;; -;; TODO: Replace anytype and customize inputs for your language/stack. -;; See: https://guix.gnu.org/manual/en/html_node/Defining-Packages.html - -(use-modules (guix packages) - (guix gexp) - (guix git-download) - (guix build-system gnu) - (guix licenses) - (gnu packages base)) - -(package - (name "anytype") - (version "0.1.0") - (source (local-file "." "source" - #:recursive? #t - #:select? (lambda (file stat) - (not (string-contains file ".git"))))) - (build-system gnu-build-system) - (arguments - '(#:phases - (modify-phases %standard-phases - ;; TODO: Customize build phases for your project - ;; Examples for common stacks: - ;; - ;; Rust: - ;; (replace 'build (lambda _ (invoke "cargo" "build" "--release"))) - ;; (replace 'check (lambda _ (invoke "cargo" "test"))) - ;; - ;; Elixir: - ;; (replace 'build (lambda _ (invoke "mix" "compile"))) - ;; (replace 'check (lambda _ (invoke "mix" "test"))) - ;; - ;; Zig: - ;; (replace 'build (lambda _ (invoke "zig" "build"))) - ;; (replace 'check (lambda _ (invoke "zig" "build" "test"))) - (delete 'configure) - (delete 'build) - (delete 'check) - (replace 'install - (lambda* (#:key outputs #:allow-other-keys) - (let ((out (assoc-ref outputs "out"))) - (mkdir-p (string-append out "/share/doc")) - (copy-file "README.adoc" - (string-append out "/share/doc/README.adoc")))))))) - (native-inputs - (list - ;; TODO: Add build-time dependencies - ;; Examples: - ;; rust (gnu packages rust) - ;; elixir (gnu packages elixir) - ;; zig (gnu packages zig) - )) - (inputs - (list - ;; TODO: Add runtime dependencies - )) - (home-page "https://github.com/hyperpolymath/anytype") - (synopsis "The reference type-checker kernel that implements systemet (Equality Theory).") - (description "RSR-compliant project. See README.adoc for details.") - (license (list - ;; MPL-2.0 extends MPL-2.0 - mpl2.0))) diff --git a/build/just/assess.just b/build/just/assess.just deleted file mode 100644 index 6e2a128..0000000 --- a/build/just/assess.just +++ /dev/null @@ -1,225 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -# -# PROJECT SELF-ASSESSMENT + OPENSSF COMPLIANCE VERIFICATION -# -# Imported by ../../Justfile via `import? "build/just/assess.just"`. -# Recipes here advise on what to keep/remove (`self-assess`, read-only) and -# verify that OpenSSF Best Practices prerequisites are present (`verify`, -# called by `init` and CI). - -# Analyse this project and advise what to keep, remove, or leave for later. -# Does NOT modify any files — only prints recommendations. -self-assess: - #!/usr/bin/env bash - set -euo pipefail - - echo "═══════════════════════════════════════════════════" - echo " RSR Project Self-Assessment" - echo "═══════════════════════════════════════════════════" - echo "" - echo "Scanning project structure to identify what's" - echo "relevant, removable, or worth keeping for later..." - echo "" - - # Detect project characteristics - HAS_RUST=false; [ -f "Cargo.toml" ] && HAS_RUST=true - HAS_ELIXIR=false; [ -f "mix.exs" ] && HAS_ELIXIR=true - HAS_RESCRIPT=false; [ -f "rescript.json" ] || [ -f "bsconfig.json" ] && HAS_RESCRIPT=true - HAS_IDRIS=false; ls *.ipkg >/dev/null 2>&1 && HAS_IDRIS=true - HAS_ZIG=false; [ -f "build.zig" ] || [ -d "ffi/zig" ] && HAS_ZIG=true - HAS_GLEAM=false; [ -f "gleam.toml" ] && HAS_GLEAM=true - HAS_CONTAINER=false; [ -f "Containerfile" ] || [ -f "container/Containerfile" ] && HAS_CONTAINER=true - HAS_TESTS=false; [ -d "test" ] || [ -d "tests" ] || [ -d "__tests__" ] && HAS_TESTS=true - HAS_API=false; grep -rq 'port\|listen\|endpoint' --include="*.exs" --include="*.rs" --include="*.toml" . 2>/dev/null && HAS_API=true - IS_LIBRARY=false; [ -f "Cargo.toml" ] && grep -q '\[lib\]' Cargo.toml 2>/dev/null && IS_LIBRARY=true - - echo "Detected: Rust=$HAS_RUST Elixir=$HAS_ELIXIR ReScript=$HAS_RESCRIPT" - echo " Idris=$HAS_IDRIS Zig=$HAS_ZIG Gleam=$HAS_GLEAM" - echo " Container=$HAS_CONTAINER Tests=$HAS_TESTS API=$HAS_API" - echo "" - - # ── ESSENTIAL (removing these breaks RSR compliance) ────────── - echo "── ESSENTIAL (removing breaks Rhodium Standard) ──────────" - echo "" - - for f in LICENSE SECURITY.md CODE_OF_CONDUCT.md CONTRIBUTING.md .editorconfig .gitignore; do - if [ -f "$f" ]; then - echo " ✓ $f — KEEP (RSR required)" - else - echo " ✗ $f — MISSING (RSR violation!)" - fi - done - - if [ -d ".machine_readable/6a2" ]; then - echo " ✓ .machine_readable/6a2/ — KEEP (SCM checkpoint files)" - else - echo " ✗ .machine_readable/6a2/ — MISSING (RSR violation!)" - fi - - if [ -d ".github/workflows" ]; then - WF_COUNT=$(ls .github/workflows/*.yml 2>/dev/null | wc -l) - echo " ✓ .github/workflows/ — KEEP ($WF_COUNT workflows, RSR CI/CD)" - fi - echo "" - - # ── RELEVANT (useful for your project type) ─────────────────── - echo "── RELEVANT (matches your project) ───────────────────────" - echo "" - - if $HAS_IDRIS && { [ -d "src/interface/abi" ] || [ -d "src/interface/Abi" ]; }; then - echo " ✓ src/interface/abi/ — KEEP (Idris2 ABI definitions)" - elif ! $HAS_IDRIS && { [ -d "src/interface/abi" ] || [ -d "src/interface/Abi" ]; }; then - echo " ? src/interface/abi/ — No Idris2 detected." - echo " → KEEP if you plan to add formal verification later." - echo " → SAFE TO REMOVE if this project will never use Idris2." - echo " ⚠ Consequence: no formally verified interface definitions." - fi - - if $HAS_ZIG && [ -d "src/interface/ffi" ]; then - echo " ✓ src/interface/ffi/ — KEEP (Zig FFI bridge)" - elif ! $HAS_ZIG && [ -d "src/interface/ffi" ]; then - echo " ? src/interface/ffi/ — No Zig detected." - echo " → KEEP if you plan C ABI interop later." - echo " → SAFE TO REMOVE if this is a pure web/scripting project." - echo " ⚠ Consequence: no C-compatible FFI bridge." - fi - - if $HAS_API && [ -f ".machine_readable/integrations/groove.a2ml" ]; then - PORT=$(grep '(port ' .machine_readable/integrations/groove.a2ml 2>/dev/null | sed 's/.*(port \([0-9]*\)).*/\1/') - if [ "$PORT" = "0" ]; then - echo " ⚠ groove.a2ml — Port not assigned. Run 'just groove-setup'." - else - echo " ✓ groove.a2ml — KEEP (Groove discovery on port $PORT)" - fi - elif $HAS_API; then - echo " ✗ groove.a2ml — MISSING. Your project has an API but no Groove manifest." - echo " → Run 'just groove-setup' to enable snap-on/snap-off discovery." - fi - - if $HAS_CONTAINER && [ -d "container" ]; then - echo " ✓ container/ — KEEP (Containerfile + compose)" - elif ! $HAS_CONTAINER && [ -d "container" ]; then - echo " ? container/ — No Containerfile detected in use." - echo " → KEEP if you plan to containerise later." - echo " → SAFE TO REMOVE for libraries and CLI tools (run: just no-container)." - fi - - echo "" - - # ── SAFE TO REMOVE (not relevant, no consequences) ──────────── - echo "── SAFE TO REMOVE (no RSR consequences) ──────────────────" - echo "" - - if ! $HAS_RESCRIPT && [ -d "examples" ] && ls examples/*.res >/dev/null 2>&1; then - echo " ○ examples/*.res — Template ReScript examples. Not your code." - fi - - if [ -f ".machine_readable/ai/PLACEHOLDERS.adoc" ]; then - echo " ○ .machine_readable/ai/PLACEHOLDERS.adoc — Template doc. Remove after init." - fi - - if { [ -f "build/flake.nix" ] || [ -f "flake.nix" ]; } && ! command -v nix >/dev/null 2>&1; then - echo " ○ flake.nix — Nix flake. Safe to remove if you don't use Nix." - echo " → KEEP if others might build with Nix." - fi - - if { [ -f "build/guix.scm" ] || [ -f "guix.scm" ]; } && ! command -v guix >/dev/null 2>&1; then - echo " ○ guix.scm — Guix package. Safe to remove if you don't use Guix." - echo " → KEEP if others might build with Guix." - fi - - echo "" - - # ── FUTURE VALUE (not needed now, worth keeping) ────────────── - echo "── KEEP FOR FUTURE (not active, but valuable later) ──────" - echo "" - - if [ -d ".machine_readable/contractiles" ]; then - echo " ◆ contractiles/ — Must/Trust/Dust/Lust contracts." - echo " Not enforced until you configure them, but ready when you need" - echo " automated compliance checking. Zero cost to keep." - fi - - if [ -d ".machine_readable/bot_directives" ]; then - echo " ◆ bot_directives/ — Gitbot fleet configuration." - echo " Not active until gitbot-fleet is connected. Keeps your repo" - echo " ready for automated maintenance when the fleet arrives." - fi - - if [ -d ".machine_readable/bot_directives" ]; then - echo " ◆ bot_directives/ — AI agent methodology config." - echo " Guides Claude/Gemini/etc on how to work in this repo." - echo " No cost to keep. Improves AI assistance quality." - fi - - if [ -d "docs/governance" ]; then - echo " ◆ docs/governance/ — TSDM, CRG, maintenance checklists." - echo " Not needed for solo projects. Essential when you add contributors." - fi - - if [ -d "verification" ]; then - echo " ◆ verification/ — Proofs, benchmarks, fuzzing, safety case." - echo " Empty scaffolds until you add formal verification." - echo " Worth keeping for any project that claims safety properties." - fi - - echo "" - echo "═══════════════════════════════════════════════════" - echo " Assessment complete. No files were modified." - echo "═══════════════════════════════════════════════════" - -# Verify OpenSSF Best Practices prerequisites — fails if any required file is missing -verify: - #!/usr/bin/env bash - set -euo pipefail - - echo "=== OpenSSF Best Practices Verification ===" - ERRORS=0 - - check_file() { - if [ ! -f "$1" ]; then - echo " FAIL: $1 missing" - ERRORS=$((ERRORS + 1)) - else - echo " OK: $1" - fi - } - - # Accept either .md or .adoc for documentation files - check_either() { - if [ ! -f "$1" ] && [ ! -f "$2" ]; then - echo " FAIL: $1 (or $2) missing" - ERRORS=$((ERRORS + 1)) - else - local found="$1" - [ -f "$2" ] && found="$2" - [ -f "$1" ] && found="$1" - echo " OK: $found" - fi - } - - check_either "SECURITY.md" "SECURITY.adoc" - check_file "LICENSE" - check_either "CONTRIBUTING.md" "CONTRIBUTING.adoc" - check_either "README.adoc" "README.md" - check_file ".machine_readable/6a2/STATE.a2ml" - check_file ".machine_readable/6a2/META.a2ml" - check_file ".machine_readable/6a2/ECOSYSTEM.a2ml" - check_either "CHANGELOG.md" "CHANGELOG.adoc" - - # Check at least 1 workflow exists - WORKFLOW_COUNT=$(find .github/workflows -name '*.yml' -o -name '*.yaml' 2>/dev/null | wc -l) - if [ "$WORKFLOW_COUNT" -eq 0 ]; then - echo " FAIL: No workflows in .github/workflows/" - ERRORS=$((ERRORS + 1)) - else - echo " OK: .github/workflows/ ($WORKFLOW_COUNT workflows)" - fi - - echo "" - if [ "$ERRORS" -gt 0 ]; then - echo "FAIL: $ERRORS OpenSSF prerequisites missing — repo cannot ship." - exit 1 - fi - echo "PASS: All OpenSSF Best Practices prerequisites satisfied." diff --git a/build/just/container.just b/build/just/container.just deleted file mode 100644 index c5728a9..0000000 --- a/build/just/container.just +++ /dev/null @@ -1,284 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -# -# CONTAINERS — three-tier containerisation -# -# Imported by ../../Justfile via `import? "build/just/container.just"`. -# Variables (project, OWNER, ...) and `set shell` are inherited from the root. -# -# Tier A — OCI standard: container/Containerfile, container/.containerignore -# Tier B — portable engine: container/compose.yaml (podman | nerdctl | docker) -# Tier C — stapeln sovereign: container/stapeln/ (cerro-torre, svalinn, -# vordr, selur, rokur, k9) -# -# Engine is auto-selected: $CONTAINER_ENGINE, else the first of podman / -# nerdctl / docker found on PATH. Override with: CONTAINER_ENGINE=docker just … -# -# Narrow the template to the tiers you want (see the Narrowing section below): -# just container-keep oci portable # keep image + portable compose, drop the rest -# just no-stapeln | no-devcontainer | no-container # convenience aliases - -# ── Engine detection (shared snippet) ────────────────────────────────────── -# Resolves the OCI engine into $ENGINE. Sourced at the top of each recipe. -_engine := ''' - ENGINE="${CONTAINER_ENGINE:-}" - if [ -z "$ENGINE" ]; then - for e in podman nerdctl docker; do - if command -v "$e" >/dev/null 2>&1; then ENGINE="$e"; break; fi - done - fi - if [ -z "$ENGINE" ]; then - echo "No container engine found (looked for podman, nerdctl, docker)." >&2 - echo "Install one or set CONTAINER_ENGINE." >&2 - exit 1 - fi -''' - -# Initialise container templates — substitute placeholders with project values -container-init: - #!/usr/bin/env bash - set -euo pipefail - - if [ ! -d "container" ]; then - echo "Error: container/ directory not found." - echo "This repo may not have been created from rsr-template-repo," - echo "or containerisation was removed with 'just no-container'." - exit 1 - fi - - echo "=== Container Template Initialisation ===" - echo "" - - # Load RSR defaults if available - DEFAULTS="${XDG_CONFIG_HOME:-$HOME/.config}/rsr/defaults" - if [ -f "$DEFAULTS" ]; then - echo "Loading defaults from $DEFAULTS" - # shellcheck source=/dev/null - source "$DEFAULTS" - echo "" - fi - - # Prompt for container-specific values - read -rp "Service name (e.g. my-api) [{{project}}]: " _SERVICE_NAME - SERVICE_NAME="${_SERVICE_NAME:-{{project}}}" - - read -rp "Primary port [8080]: " _PORT - PORT="${_PORT:-8080}" - - read -rp "Container registry [ghcr.io/${OWNER:-{{OWNER}}}]: " _REGISTRY - REGISTRY="${_REGISTRY:-ghcr.io/${OWNER:-{{OWNER}}}}" - - echo "" - echo " Service: $SERVICE_NAME" - echo " Port: $PORT" - echo " Registry: $REGISTRY" - echo "" - read -rp "Proceed? [Y/n] " CONFIRM - [[ "${CONFIRM:-Y}" =~ ^[Nn] ]] && echo "Aborted." && exit 0 - - echo "" - echo "Replacing container placeholders..." - - # Brace tokens as variables (hex escapes avoid just interpolation) - LB=$(printf '\x7b\x7b') - RB=$(printf '\x7d\x7d') - - SED_ARGS=( - -e "s|${LB}SERVICE_NAME${RB}|${SERVICE_NAME}|g" - -e "s|${LB}PORT${RB}|${PORT}|g" - -e "s|${LB}REGISTRY${RB}|${REGISTRY}|g" - ) - - # Recurses into container/stapeln/ as well. - find container/ -type f | while read -r file; do - if file --brief "$file" | grep -qi 'text\|ascii\|utf'; then - sed -i "${SED_ARGS[@]}" "$file" - fi - done - - echo "Container templates initialised." - echo "" - echo "Next steps:" - echo " 1. Edit container/Containerfile — add your build commands (Tier A)" - echo " 2. Edit container/entrypoint.sh — set your application binary" - echo " 3. Review container/compose.yaml — portable stack (Tier B)" - echo " 4. Review container/stapeln/ — sovereign stack (Tier C)" - echo " 5. Build: just container-build" - -# Build container image (cerro-torre pipeline if present, else plain OCI build) -container-build *args: - #!/usr/bin/env bash - set -euo pipefail - {{_engine}} - if [ -f "container/stapeln/ct-build.sh" ]; then - cd container/stapeln && CONTAINER_ENGINE="$ENGINE" ./ct-build.sh {{args}} - elif [ -f "container/Containerfile" ]; then - "$ENGINE" build -t {{project}}:latest -f container/Containerfile . - elif [ -f "Containerfile" ]; then - "$ENGINE" build -t {{project}}:latest -f Containerfile . - else - echo "No Containerfile found in container/ or project root" - exit 1 - fi - -# Pick the compose path: selur-compose (sovereign) if installed, else portable -_compose action *args: - #!/usr/bin/env bash - set -euo pipefail - {{_engine}} - if command -v selur-compose >/dev/null 2>&1 && [ -f "container/stapeln/compose.toml" ]; then - ( cd container/stapeln && selur-compose {{action}} {{args}} ) - elif [ -f "container/compose.yaml" ]; then - "$ENGINE" compose -f container/compose.yaml {{action}} {{args}} - else - echo "No compose file found (container/stapeln/compose.toml or container/compose.yaml)" - exit 1 - fi - -# Verify compose configuration (selur-compose verify, else compose config) -container-verify: - #!/usr/bin/env bash - set -euo pipefail - {{_engine}} - if command -v selur-compose >/dev/null 2>&1 && [ -f "container/stapeln/compose.toml" ]; then - ( cd container/stapeln && selur-compose verify ) - elif [ -f "container/compose.yaml" ]; then - "$ENGINE" compose -f container/compose.yaml config - else - echo "No compose file found (container/stapeln/compose.toml or container/compose.yaml)" - exit 1 - fi - -# Start the container stack (selur-compose if available, else $ENGINE compose) -container-up *args: - @just _compose up {{args}} - -# Stop the container stack -container-down *args: - @just _compose down {{args}} - -# Sign and verify the container bundle (cerro-torre: build + pack + sign + verify) -container-sign: - #!/usr/bin/env bash - set -euo pipefail - if [ -f "container/stapeln/ct-build.sh" ]; then - cd container/stapeln && ./ct-build.sh - else - echo "No container/stapeln/ct-build.sh found" - exit 1 - fi - -# Push the signed bundle (or plain image) to the registry -container-push: - #!/usr/bin/env bash - set -euo pipefail - {{_engine}} - if [ -f "container/stapeln/ct-build.sh" ]; then - cd container/stapeln && CONTAINER_ENGINE="$ENGINE" ./ct-build.sh --push - else - echo "No container/stapeln/ct-build.sh found — falling back to $ENGINE push" - "$ENGINE" push {{project}}:latest - fi - -# Run the container interactively (for debugging) -container-run *args: - #!/usr/bin/env bash - set -euo pipefail - {{_engine}} - "$ENGINE" run --rm -it {{project}}:latest {{args}} - -# Container matrix: [build|run|push|shell|scan] x [registry] x [tag] -container-matrix action="build" registry="ghcr.io/{{OWNER}}" tag="latest": - @echo "Container matrix: action={{action}} registry={{registry}} tag={{tag}}" - -# ── Narrowing / opt-out ────────────────────────────────────────────────────── -# -# `container-keep` is the workhorse: declare exactly which tiers to KEEP; the -# rest are removed. Tiers: oci (A) · portable (B) · stapeln (C) · devcontainer. -# Idempotent — safe to re-run. The aliases below are thin wrappers. -# -# just container-keep oci # bare OCI image only -# just container-keep oci portable # image + portable compose -# just container-keep oci portable stapeln # full prod stack, no dev container -# just container-keep all # no-op (keep everything) -# just container-keep none # remove everything (= no-container) -# DRY_RUN=1 just container-keep oci # show what would change, do nothing -# FORCE=1 just container-keep oci # skip the confirm prompt -# -# Accepts space- or comma-separated tokens, and aliases: a/A, b/B/compose, -# c/C/sovereign, dev. 'portable'/'stapeln' require 'oci' (they build the image). -container-keep +tiers: - #!/usr/bin/env bash - set -euo pipefail - - sel="$(echo "$@" | tr ',' ' ')" - keep_oci=false keep_port=false keep_stap=false keep_dev=false - for t in $sel; do - case "$t" in - all) keep_oci=true; keep_port=true; keep_stap=true; keep_dev=true ;; - none) : ;; - oci|a|A) keep_oci=true ;; - portable|compose|b|B) keep_port=true ;; - stapeln|sovereign|c|C) keep_stap=true ;; - devcontainer|dev) keep_dev=true ;; - *) echo "Unknown tier '$t'. Valid: oci portable stapeln devcontainer | all | none" >&2; exit 1 ;; - esac - done - - # Coherence: tiers B and C build the OCI image, so they need tier A. - if { $keep_port || $keep_stap; } && ! $keep_oci; then - echo "Incoherent selection: 'portable'/'stapeln' build the OCI image — add 'oci'." >&2 - exit 1 - fi - - # Build the removal plan. - plan=() - $keep_dev || plan+=(".devcontainer/ (dev container)") - if $keep_oci; then - $keep_stap || plan+=("container/stapeln/ (cerro-torre, svalinn, vordr, selur, rokur, k9)") - $keep_port || plan+=("container/compose.yaml + compose.example.yaml (portable stack)") - else - plan+=("container/ (entire image + compose + stapeln)") - plan+=("build/just/container.just (this module) + its Justfile import") - [ -f .github/workflows/container-build.yml ] && plan+=(".github/workflows/container-build.yml") - fi - - echo "Keeping: oci=$keep_oci portable=$keep_port stapeln=$keep_stap devcontainer=$keep_dev" - if [ ${#plan[@]} -eq 0 ]; then echo "Nothing to remove — selection already matches."; exit 0; fi - echo "Will remove:"; printf ' - %s\n' "${plan[@]}" - - if [ "${DRY_RUN:-}" = "1" ]; then echo "(DRY_RUN — no changes made)"; exit 0; fi - if [ "${FORCE:-}" != "1" ]; then - read -rp "Proceed? [y/N] " c; [[ "${c:-N}" =~ ^[Yy] ]] || { echo "Aborted."; exit 0; } - fi - - # Apply. - $keep_dev || rm -rf .devcontainer - if $keep_oci; then - $keep_stap || rm -rf container/stapeln - $keep_port || rm -f container/compose.yaml container/compose.example.yaml - else - rm -rf container - rm -f .machine_readable/configs/selur-compose.toml - rm -f .github/workflows/container-build.yml - rm -f build/just/container.just - [ -f Justfile ] && sed -i '/# >>> container-module/,/# <<< container-module/d' Justfile - for jf in Justfile .machine_readable/contractiles/Justfile; do - [ -f "$jf" ] && sed -i '\|import? "build/just/container.just"|d' "$jf" - done - fi - - echo "" - echo "Done. Review .github/workflows/ for image build/publish jobs you no longer need." - -# Remove ALL containerisation (image, compose, stapeln, dev container) -no-container: - @just container-keep none - -# Drop only the stapeln sovereign tier (keep OCI image + portable compose + dev container) -no-stapeln: - @just container-keep oci portable devcontainer - -# Drop only the dev container (keep the full image/compose/stapeln stack) -no-devcontainer: - @just container-keep oci portable stapeln diff --git a/build/just/groove.just b/build/just/groove.just deleted file mode 100644 index 029a9bd..0000000 --- a/build/just/groove.just +++ /dev/null @@ -1,98 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -# -# GROOVE PROTOCOL -# -# Imported by ../../Justfile via `import? "build/just/groove.just"`. -# Recipes here configure and validate the Groove protocol manifest at -# .machine_readable/integrations/groove.a2ml — port assignment, API surface -# flags (REST/gRPC/GraphQL/WebSocket/SSE), and template-placeholder hygiene. -# The manifest itself is consumed by the Groove bridge / zig-unified-api-adapter. - -# Configure Groove protocol manifest (port assignment, API surfaces) -groove-setup: - #!/usr/bin/env bash - set -euo pipefail - MANIFEST=".machine_readable/integrations/groove.a2ml" - if [ ! -f "$MANIFEST" ]; then - echo "Error: $MANIFEST not found. Run 'just init' first." - exit 1 - fi - - echo "═══════════════════════════════════════════════════" - echo " Groove Protocol Setup" - echo "═══════════════════════════════════════════════════" - echo "" - echo "Check PORT-REGISTRY.md before assigning a port:" - echo " https://github.com/hyperpolymath/standards/blob/main/PORT-REGISTRY.md" - echo "" - - read -rp "Primary port for this service: " PORT - [ -z "$PORT" ] && echo "Error: port required" && exit 1 - - echo "" - echo "Which API surfaces does this project expose?" - read -rp " REST API? [Y/n]: " REST - read -rp " gRPC? [y/N]: " GRPC - read -rp " GraphQL? [y/N]: " GRAPHQL - read -rp " WebSocket? [y/N]: " WS - read -rp " SSE (Server-Sent Events)? [y/N]: " SSE - - # Update port in manifest - sed -i "s/(port 0)/(port ${PORT})/" "$MANIFEST" - - # Update API surface flags - [[ "${GRPC,,}" == "y" ]] && sed -i 's/(grpc.*enabled false)/(grpc (enabled true)/' "$MANIFEST" - [[ "${GRAPHQL,,}" == "y" ]] && sed -i 's/(graphql.*enabled false)/(graphql (enabled true)/' "$MANIFEST" - [[ "${WS,,}" == "y" ]] && sed -i 's/(websocket.*enabled false)/(websocket (enabled true)/' "$MANIFEST" - [[ "${SSE,,}" == "y" ]] && sed -i 's/(sse.*enabled false)/(sse (enabled true)/' "$MANIFEST" - - echo "" - echo "Groove manifest updated: $MANIFEST" - echo "Port ${PORT} assigned. Add to PORT-REGISTRY.md if not already there." - -# Check for template placeholders that haven't been replaced -verify-template: - #!/usr/bin/env bash - set -euo pipefail - echo "Checking for unreplaced template placeholders..." - FOUND=0 - - # Check for double-brace placeholder patterns - HITS=$(grep -rn '{{'{{'}}[A-Z_]*{{'}}'}}' --include="*.adoc" --include="*.md" --include="*.a2ml" \ - --include="*.scm" --include="*.toml" --include="*.yml" --include="*.yaml" \ - . 2>/dev/null | grep -v 'node_modules\|\.git/' | grep -v 'PLACEHOLDERS.adoc' || true) - if [ -n "$HITS" ]; then - echo "" - echo "⚠ Unreplaced placeholders found:" - echo "$HITS" | head -20 - FOUND=1 - fi - - # Check for template defaults still present - if grep -q 'rsr-template-repo' Justfile 2>/dev/null; then - echo "⚠ Justfile still references 'rsr-template-repo' — update project name" - FOUND=1 - fi - - # Check for port 0 in Groove manifest - if grep -q '(port 0)' .machine_readable/integrations/groove.a2ml 2>/dev/null; then - echo "⚠ Groove manifest has port 0 — run 'just groove-setup' to assign a port" - FOUND=1 - fi - - # Check for empty SCM files - for f in .machine_readable/6a2/STATE.a2ml .machine_readable/6a2/META.a2ml .machine_readable/6a2/ECOSYSTEM.a2ml; do - if [ -f "$f" ] && grep -q '{{'{{'}}' "$f" 2>/dev/null; then - echo "⚠ $f still has template placeholders" - FOUND=1 - fi - done - - if [ $FOUND -eq 0 ]; then - echo "✓ No template placeholders found — project is properly customised." - else - echo "" - echo "Run 'just init' to replace placeholders, or edit files manually." - exit 1 - fi diff --git a/build/just/init.just b/build/just/init.just deleted file mode 100644 index 746b4f6..0000000 --- a/build/just/init.just +++ /dev/null @@ -1,214 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -# -# INIT — Bootstrap a new project from this template -# -# Imported by ../../Justfile via `import? "build/just/init.just"`. -# Variables (project, OWNER, REPO, version, tier) and the `set shell` directive -# are inherited from the root Justfile. - -# Interactive project bootstrap — replaces all {{PLACEHOLDER}} tokens -init: - #!/usr/bin/env bash - set -euo pipefail - - echo "═══════════════════════════════════════════════════" - echo " RSR Project Bootstrap" - echo "═══════════════════════════════════════════════════" - echo "" - - # --- Load defaults from config (if exists) --- - # Create yours: ~/.config/rsr/defaults - # Format: OWNER=myorg AUTHOR="My Name" AUTHOR_EMAIL=me@example.org ... - DEFAULTS="${XDG_CONFIG_HOME:-$HOME/.config}/rsr/defaults" - if [ -f "$DEFAULTS" ]; then - echo "Loading defaults from $DEFAULTS" - # shellcheck source=/dev/null - source "$DEFAULTS" - echo "" - fi - - # --- Required values (pre-filled from defaults if available) --- - read -rp "Project name (human-readable, e.g. My Project): " PROJECT_NAME - [ -z "$PROJECT_NAME" ] && echo "Error: project name required" && exit 1 - - read -rp "Repository slug (e.g. my-project): " REPO - [ -z "$REPO" ] && echo "Error: repo slug required" && exit 1 - - read -rp "Owner [${OWNER:-}]: " _OWNER - OWNER="${_OWNER:-${OWNER:-}}" - [ -z "$OWNER" ] && echo "Error: owner required" && exit 1 - - read -rp "Author full name [${AUTHOR:-}]: " _AUTHOR - AUTHOR="${_AUTHOR:-${AUTHOR:-}}" - [ -z "$AUTHOR" ] && echo "Error: author name required" && exit 1 - - read -rp "Author email [${AUTHOR_EMAIL:-}]: " _AUTHOR_EMAIL - AUTHOR_EMAIL="${_AUTHOR_EMAIL:-${AUTHOR_EMAIL:-}}" - [ -z "$AUTHOR_EMAIL" ] && echo "Error: email required" && exit 1 - - # --- Optional values (pre-filled from defaults if available) --- - read -rp "Author organization [${AUTHOR_ORG:-none}]: " _AUTHOR_ORG - AUTHOR_ORG="${_AUTHOR_ORG:-${AUTHOR_ORG:-}}" - - read -rp "Previous/alt email [${AUTHOR_EMAIL_ALT:-none}]: " _AUTHOR_EMAIL_ALT - AUTHOR_EMAIL_ALT="${_AUTHOR_EMAIL_ALT:-${AUTHOR_EMAIL_ALT:-}}" - - read -rp "Project description []: " PROJECT_DESCRIPTION - - read -rp "Forge domain [${FORGE:-github.com}]: " _FORGE - FORGE="${_FORGE:-${FORGE:-github.com}}" - - read -rp "Security contact email [${SECURITY_EMAIL:-$AUTHOR_EMAIL}]: " _SECURITY_EMAIL - SECURITY_EMAIL="${_SECURITY_EMAIL:-${SECURITY_EMAIL:-$AUTHOR_EMAIL}}" - - read -rp "Conduct contact email [${CONDUCT_EMAIL:-$AUTHOR_EMAIL}]: " _CONDUCT_EMAIL - CONDUCT_EMAIL="${_CONDUCT_EMAIL:-${CONDUCT_EMAIL:-$AUTHOR_EMAIL}}" - - read -rp "Project type (library|binary|monorepo|service|website) [library]: " PROJECT_TYPE - PROJECT_TYPE="${PROJECT_TYPE:-library}" - - read -rp "Website URL [https://${FORGE}/${OWNER}/${REPO}]: " WEBSITE - WEBSITE="${WEBSITE:-https://${FORGE}/${OWNER}/${REPO}}" - - # --- Container values (optional — only relevant if container/ exists) --- - if [ -d "container" ]; then - echo "" - echo "── Container configuration (optional) ─────────" - read -rp "Service name [${REPO}]: " _SERVICE_NAME - SERVICE_NAME="${_SERVICE_NAME:-${REPO}}" - read -rp "Primary port [8080]: " _PORT - PORT="${_PORT:-8080}" - read -rp "Container registry [ghcr.io/${OWNER}]: " _REGISTRY - REGISTRY="${_REGISTRY:-ghcr.io/${OWNER}}" - else - SERVICE_NAME="${REPO}" - PORT="8080" - REGISTRY="ghcr.io/${OWNER}" - fi - - # --- Derived values --- - PROJECT_UPPER=$(echo "$REPO" | tr '[:lower:]-' '[:upper:]_') - PROJECT_LOWER=$(echo "$REPO" | tr '[:upper:]-' '[:lower:]_') - CURRENT_YEAR=$(date +%Y) - CURRENT_DATE=$(date +%Y-%m-%d) - VERSION="0.1.0" - - # Derive citation name parts (best-effort split on last space) - AUTHOR_LAST="${AUTHOR##* }" - AUTHOR_FIRST="${AUTHOR% *}" - FIRST_INITIAL="${AUTHOR_FIRST:0:1}." - if [ "$AUTHOR_LAST" = "$AUTHOR_FIRST" ]; then - AUTHOR_FIRST="$AUTHOR" - AUTHOR_LAST="" - FIRST_INITIAL="" - fi - - echo "" - echo "── Summary ──────────────────────────────────────" - echo " Project: $PROJECT_NAME" - echo " Repo: $REPO" - echo " Owner: $OWNER" - echo " Author: $AUTHOR <$AUTHOR_EMAIL>" - [ -n "$AUTHOR_ORG" ] && echo " Organization: $AUTHOR_ORG" - echo " Forge: $FORGE" - echo " Year: $CURRENT_YEAR" - echo "────────────────────────────────────────────────" - echo "" - read -rp "Proceed? [Y/n] " CONFIRM - [[ "${CONFIRM:-Y}" =~ ^[Nn] ]] && echo "Aborted." && exit 0 - - echo "" - echo "Replacing placeholders..." - - # Brace tokens as variables (hex avoids just interpolation) - LB=$(printf '\x7b\x7b') - RB=$(printf '\x7d\x7d') - - # Build the sed expression list - # Note: using | as delimiter since URLs contain / - SED_ARGS=( - -e "s|${LB}PROJECT_NAME${RB}|${PROJECT_NAME}|g" - -e "s|${LB}PROJECT_DESCRIPTION${RB}|${PROJECT_DESCRIPTION}|g" - -e "s|${LB}PROJECT${RB}|${PROJECT_UPPER}|g" - -e "s|${LB}project${RB}|${PROJECT_LOWER}|g" - -e "s|${LB}REPO${RB}|${REPO}|g" - -e "s|${LB}OWNER${RB}|${OWNER}|g" - -e "s|${LB}AUTHOR${RB}|${AUTHOR}|g" - -e "s|${LB}AUTHOR_EMAIL${RB}|${AUTHOR_EMAIL}|g" - -e "s|${LB}AUTHOR_ORG${RB}|${AUTHOR_ORG}|g" - -e "s|${LB}AUTHOR_LAST${RB}|${AUTHOR_LAST}|g" - -e "s|${LB}AUTHOR_FIRST${RB}|${AUTHOR_FIRST}|g" - -e "s|${LB}AUTHOR_INITIALS${RB}|${FIRST_INITIAL}|g" - -e "s|${LB}FORGE${RB}|${FORGE}|g" - -e "s|${LB}CURRENT_YEAR${RB}|${CURRENT_YEAR}|g" - -e "s|${LB}CURRENT_DATE${RB}|${CURRENT_DATE}|g" - -e "s|${LB}DATE${RB}|${CURRENT_DATE}|g" - -e "s|${LB}SECURITY_EMAIL${RB}|${SECURITY_EMAIL}|g" - -e "s|${LB}CONDUCT_EMAIL${RB}|${CONDUCT_EMAIL}|g" - -e "s|${LB}LICENSE${RB}|MPL-2.0|g" - -e "s|${LB}CONDUCT_TEAM${RB}|Code of Conduct Committee|g" - -e "s|${LB}RESPONSE_TIME${RB}|48 hours|g" - -e "s|${LB}MAIN_BRANCH${RB}|main|g" - -e "s|${LB}PROJECT_PURPOSE${RB}|${PROJECT_DESCRIPTION}|g" - -e "s|${LB}PROJECT_ROLE${RB}|${PROJECT_TYPE}|g" - -e "s|${LB}PROJECT_TYPE${RB}|${PROJECT_TYPE}|g" - -e "s|${LB}WEBSITE${RB}|${WEBSITE}|g" - -e "s|${LB}SERVICE_NAME${RB}|${SERVICE_NAME}|g" - -e "s|${LB}PORT${RB}|${PORT}|g" - -e "s|${LB}REGISTRY${RB}|${REGISTRY}|g" - -e "s|${LB}IMAGE${RB}|${REGISTRY}/${SERVICE_NAME}|g" - -e "s|${LB}VERSION${RB}|${VERSION}|g" - -e "s|${LB}EMAIL${RB}|${AUTHOR_EMAIL}|g" - ) - [ -n "$AUTHOR_EMAIL_ALT" ] && SED_ARGS+=(-e "s|${LB}AUTHOR_EMAIL_ALT${RB}|${AUTHOR_EMAIL_ALT}|g") - - # Replace in all text files (skip .git, LICENSE text, and binaries) - find . -type f \ - -not -path './.git/*' \ - -not -name 'MPL-2.0.txt' \ - -not -name '*.png' -not -name '*.jpg' -not -name '*.gif' \ - -not -name '*.woff' -not -name '*.woff2' \ - | while read -r file; do - if file --brief "$file" | grep -qi 'text\|ascii\|utf'; then - sed -i "${SED_ARGS[@]}" "$file" - fi - done - - # Also replace [YOUR-REPO-NAME] and [YOUR-NAME/ORG] in AI manifest - sed -i "s|\[YOUR-REPO-NAME\]|${PROJECT_NAME}|g" 0-AI-MANIFEST.a2ml 2>/dev/null || true - sed -i "s|\[YOUR-NAME/ORG\]|${OWNER}|g" 0-AI-MANIFEST.a2ml 2>/dev/null || true - - echo "" - echo "── Validation ───────────────────────────────────" - - # Check for remaining placeholders - PATTERN="${LB}[A-Z_]*${RB}" - REMAINING=$(grep -rl "$PATTERN" . --include='*.md' --include='*.adoc' --include='*.yml' --include='*.yaml' --include='*.a2ml' --include='*.toml' --include='*.scm' --include='*.ncl' --include='*.nix' --include='*.json' --include='*.sh' 2>/dev/null | grep -v '.git/' | grep -v '.machine_readable/ai/PLACEHOLDERS.adoc' || true) - if [ -n "$REMAINING" ]; then - echo "WARNING: Remaining placeholders in:" - echo "$REMAINING" | sed 's/^/ /' - echo "" - echo "Run: grep -rn '$LB' . --include='*.md' to inspect" - else - echo "All placeholders replaced successfully!" - fi - - # K9-SVC validation (if available) - if command -v k9-svc >/dev/null 2>&1; then - echo "" - echo "Running k9-svc validation..." - k9-svc validate . 2>/dev/null || true - fi - - echo "" - echo "Running OpenSSF compliance verification..." - just verify - - echo "" - echo "Done! Next steps:" - echo " 1. Review changes: git diff" - echo " 2. Remove template cruft: rm .machine_readable/ai/PLACEHOLDERS.adoc" - echo " 3. Customize README.adoc for your project" - echo " 4. Commit: git add -A && git commit -m 'feat: initialize from RSR template'" - echo " 5. Push: git remote add origin git@${FORGE}:${OWNER}/${REPO}.git && git push -u origin main" diff --git a/build/just/proofs.just b/build/just/proofs.just deleted file mode 100644 index b124d7a..0000000 --- a/build/just/proofs.just +++ /dev/null @@ -1,154 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -# -# FORMAL VERIFICATION (PROOFS) -# -# Imported by ../../Justfile via `import? "build/just/proofs.just"`. -# Recipes here check formal proofs across Idris2, Lean4, Agda, and Coq, plus -# scan for dangerous/unsafe constructs and report status. Run via -# `just proof-check-all` for the full sweep. - -# Check all formal proofs (Idris2 + Lean4 + Agda + Coq) -proof-check-all: proof-check-idris2 proof-check-lean4 proof-check-agda proof-check-coq proof-scan-dangerous - @echo "=== All proof checks complete ===" - -# Check Idris2 proofs (ABI, types, dependent type proofs) -proof-check-idris2: - #!/usr/bin/env bash - set -euo pipefail - echo "=== Checking Idris2 proofs ===" - if ! command -v idris2 &>/dev/null; then - echo "SKIP: idris2 not installed" - exit 0 - fi - ERRORS=0 - for f in $(find verification/proofs/idris2 -name '*.idr' 2>/dev/null); do - echo -n " Checking $f ... " - if idris2 --check "$f" 2>/dev/null; then - echo "OK" - else - echo "FAIL" - ERRORS=$((ERRORS + 1)) - fi - done - if [ "$ERRORS" -gt 0 ]; then - echo "FAIL: $ERRORS Idris2 proof(s) failed" - exit 1 - fi - echo "PASS: All Idris2 proofs verified" - -# Check Lean4 proofs -proof-check-lean4: - #!/usr/bin/env bash - set -euo pipefail - echo "=== Checking Lean4 proofs ===" - if ! command -v lean &>/dev/null; then - echo "SKIP: lean not installed" - exit 0 - fi - ERRORS=0 - for f in $(find verification/proofs/lean4 -name '*.lean' 2>/dev/null); do - echo -n " Checking $f ... " - if lean "$f" 2>/dev/null; then - echo "OK" - else - echo "FAIL" - ERRORS=$((ERRORS + 1)) - fi - done - if [ "$ERRORS" -gt 0 ]; then - echo "FAIL: $ERRORS Lean4 proof(s) failed" - exit 1 - fi - echo "PASS: All Lean4 proofs verified" - -# Check Agda proofs -proof-check-agda: - #!/usr/bin/env bash - set -euo pipefail - echo "=== Checking Agda proofs ===" - if ! command -v agda &>/dev/null; then - echo "SKIP: agda not installed" - exit 0 - fi - ERRORS=0 - for f in $(find verification/proofs/agda -name '*.agda' 2>/dev/null); do - echo -n " Checking $f ... " - if agda --safe "$f" 2>/dev/null; then - echo "OK" - else - echo "FAIL" - ERRORS=$((ERRORS + 1)) - fi - done - if [ "$ERRORS" -gt 0 ]; then - echo "FAIL: $ERRORS Agda proof(s) failed" - exit 1 - fi - echo "PASS: All Agda proofs verified" - -# Check Coq proofs -proof-check-coq: - #!/usr/bin/env bash - set -euo pipefail - echo "=== Checking Coq proofs ===" - if ! command -v coqc &>/dev/null; then - echo "SKIP: coqc not installed" - exit 0 - fi - ERRORS=0 - for f in $(find verification/proofs/coq -name '*.v' 2>/dev/null); do - echo -n " Checking $f ... " - if coqc "$f" 2>/dev/null; then - echo "OK" - else - echo "FAIL" - ERRORS=$((ERRORS + 1)) - fi - done - if [ "$ERRORS" -gt 0 ]; then - echo "FAIL: $ERRORS Coq proof(s) failed" - exit 1 - fi - echo "PASS: All Coq proofs verified" - -# Scan for dangerous patterns in proof files (believe_me, sorry, Admitted, etc.) -proof-scan-dangerous: - #!/usr/bin/env bash - set -euo pipefail - echo "=== Scanning for dangerous patterns in proofs ===" - DANGEROUS=0 - PATTERNS="believe_me|assert_total|postulate|sorry|Admitted|unsafeCoerce|Obj\.magic" - for f in $(find verification/proofs -name '*.idr' -o -name '*.lean' -o -name '*.agda' -o -name '*.v' 2>/dev/null); do - MATCHES=$(grep -nE "$PATTERNS" "$f" 2>/dev/null || true) - if [ -n "$MATCHES" ]; then - echo " DANGEROUS: $f" - echo "$MATCHES" | sed 's/^/ /' - DANGEROUS=$((DANGEROUS + 1)) - fi - done - if [ "$DANGEROUS" -gt 0 ]; then - echo "FAIL: $DANGEROUS file(s) contain dangerous patterns" - exit 1 - fi - echo "PASS: No dangerous patterns found in proofs" - -# Show proof status summary -proof-status: - #!/usr/bin/env bash - echo "=== Proof Status ===" - echo "" - echo "Idris2: $(find verification/proofs/idris2 -name '*.idr' 2>/dev/null | wc -l) files" - echo "Lean4: $(find verification/proofs/lean4 -name '*.lean' 2>/dev/null | wc -l) files" - echo "Agda: $(find verification/proofs/agda -name '*.agda' 2>/dev/null | wc -l) files" - echo "Coq: $(find verification/proofs/coq -name '*.v' 2>/dev/null | wc -l) files" - echo "TLA+: $(find verification/proofs/tlaplus -name '*.tla' 2>/dev/null | wc -l) files" - echo "" - # PROOF-STATUS may live at root, docs/status/ (post-#20), .md or .adoc (post-#23) - for candidate in docs/status/PROOF-STATUS.adoc docs/status/PROOF-STATUS.md PROOF-STATUS.adoc PROOF-STATUS.md; do - if [ -f "$candidate" ]; then - grep -E "^\| \*\*Total\*\*|^\| \*Total\*" "$candidate" 2>/dev/null || echo "(No summary row in $candidate)" - exit 0 - fi - done - echo "(No PROOF-STATUS file found at root or docs/status/)" diff --git a/build/just/validate.just b/build/just/validate.just deleted file mode 100644 index 5ef9208..0000000 --- a/build/just/validate.just +++ /dev/null @@ -1,130 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -# -# VALIDATION & COMPLIANCE -# -# Imported by ../../Justfile via `import? "build/just/validate.just"`. -# Recipes here check that this repo conforms to the RSR (Rhodium Standard -# Repository) skeleton: required files, METAdata, AI install guide -# completeness, etc. Run via `just validate`. - -# Validate RSR compliance -validate-rsr: - #!/usr/bin/env bash - echo "=== RSR Compliance Check ===" - MISSING="" - for f in .editorconfig .gitignore Justfile README.adoc LICENSE 0-AI-MANIFEST.a2ml; do - [ -f "$f" ] || MISSING="$MISSING $f" - done - for f in .machine_readable/6a2/STATE.a2ml .machine_readable/6a2/META.a2ml .machine_readable/6a2/ECOSYSTEM.a2ml .machine_readable/6a2/anchors/ANCHOR.a2ml .machine_readable/policies/MAINTENANCE-AXES.a2ml .machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml .machine_readable/policies/SOFTWARE-DEVELOPMENT-APPROACH.a2ml; do - [ -f "$f" ] || MISSING="$MISSING $f" - done - for f in licensing/exhibits/EXHIBIT-A-ETHICAL-USE.txt licensing/exhibits/EXHIBIT-B-QUANTUM-SAFE.txt licensing/texts/MPL-2.0.txt; do - [ -f "$f" ] || MISSING="$MISSING $f" - done - if [ ! -d "src/interface/abi" ] && [ ! -d "src/interface/Abi" ]; then - MISSING="$MISSING src/interface/abi" - fi - for f in src/interface/ffi src/interface/generated; do - [ -d "$f" ] || MISSING="$MISSING $f" - done - for f in docs/governance/MAINTENANCE-CHECKLIST.adoc docs/governance/SOFTWARE-DEVELOPMENT-APPROACH.adoc; do - [ -f "$f" ] || MISSING="$MISSING $f" - done - if [ -f ".machine_readable/6a2/META.a2ml" ]; then - grep -q 'axis-1 = "must > intend > like"' .machine_readable/6a2/META.a2ml || MISSING="$MISSING META.a2ml:axis-1" - grep -q 'axis-2 = "corrective > adaptive > perfective"' .machine_readable/6a2/META.a2ml || MISSING="$MISSING META.a2ml:axis-2" - grep -q 'axis-3 = "systems > compliance > effects"' .machine_readable/6a2/META.a2ml || MISSING="$MISSING META.a2ml:axis-3" - grep -q 'scoping-first = true' .machine_readable/6a2/META.a2ml || MISSING="$MISSING META.a2ml:scoping-first" - grep -q 'idris-unsound-scan = "believe_me/assert_total"' .machine_readable/6a2/META.a2ml || MISSING="$MISSING META.a2ml:idris-unsound-scan" - grep -q 'audit-focus = "systems in place, documentation explains actual state, safety/security accounted for, observed effects reviewed"' .machine_readable/6a2/META.a2ml || MISSING="$MISSING META.a2ml:audit-focus" - grep -q 'compliance-focus = "seams/compromises/exception register, bounded exceptions, anti-drift checks"' .machine_readable/6a2/META.a2ml || MISSING="$MISSING META.a2ml:compliance-focus" - grep -q 'effects-evidence = "benchmark execution/results and maintainer status dialogue/review"' .machine_readable/6a2/META.a2ml || MISSING="$MISSING META.a2ml:effects-evidence" - grep -q 'compliance-tooling = "panic-attack"' .machine_readable/policies/MAINTENANCE-AXES.a2ml || MISSING="$MISSING MAINTENANCE-AXES.a2ml:compliance-tooling" - grep -q 'effects-tooling = "ecological checking with sustainabot guidance"' .machine_readable/policies/MAINTENANCE-AXES.a2ml || MISSING="$MISSING MAINTENANCE-AXES.a2ml:effects-tooling" - grep -q 'source-human = "docs/governance/MAINTENANCE-CHECKLIST.adoc"' .machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml || MISSING="$MISSING MAINTENANCE-CHECKLIST.a2ml:source-human" - grep -q 'source-human = "docs/governance/SOFTWARE-DEVELOPMENT-APPROACH.adoc"' .machine_readable/policies/SOFTWARE-DEVELOPMENT-APPROACH.a2ml || MISSING="$MISSING SOFTWARE-DEVELOPMENT-APPROACH.a2ml:source-human" - fi - if [ -n "$MISSING" ]; then - echo "MISSING:$MISSING" - exit 1 - fi - echo "RSR compliance: PASS" - -# Validate STATE.a2ml syntax -validate-state: - @if [ -f ".machine_readable/6a2/STATE.a2ml" ]; then \ - grep -q '^\[metadata\]' .machine_readable/6a2/STATE.a2ml && \ - grep -q 'project\s*=' .machine_readable/6a2/STATE.a2ml && \ - echo "STATE.a2ml: valid" || echo "STATE.a2ml: INVALID (missing required sections)"; \ - else \ - echo "No .machine_readable/6a2/STATE.a2ml found"; \ - fi - -# Validate AI installation guide completeness (finishbot pre-release check) -validate-ai-install: - #!/usr/bin/env bash - echo "=== AI Installation Guide Check ===" - GUIDE="docs/AI_INSTALLATION_GUIDE.adoc" - README="README.adoc" - ERRORS=0 - - # Check guide exists - if [ ! -f "$GUIDE" ]; then - echo "MISSING: $GUIDE (create from template: docs/AI_INSTALLATION_GUIDE.adoc)" - ERRORS=$((ERRORS + 1)) - else - # Check for unfilled TODO markers - TODOS=$(grep -c '\[TODO-AI-INSTALL' "$GUIDE" 2>/dev/null || true) - if [ "$TODOS" -gt 0 ]; then - echo "INCOMPLETE: $GUIDE has $TODOS unfilled [TODO-AI-INSTALL] markers:" - grep -n '\[TODO-AI-INSTALL' "$GUIDE" | head -10 - ERRORS=$((ERRORS + 1)) - else - echo "$GUIDE: complete (no TODO markers)" - fi - - # Check AI implementation section exists - if ! grep -q 'ai-implementation' "$GUIDE" 2>/dev/null; then - echo "MISSING: [[ai-implementation]] anchor in $GUIDE" - ERRORS=$((ERRORS + 1)) - fi - - # Check privacy notice exists - if ! grep -qi 'privacy' "$GUIDE" 2>/dev/null; then - echo "MISSING: Privacy notice in $GUIDE" - ERRORS=$((ERRORS + 1)) - fi - - # Check install commands exist (not just placeholders) - if ! grep -q 'git clone' "$GUIDE" 2>/dev/null; then - echo "WARNING: No git clone command found in $GUIDE -- install commands may be incomplete" - fi - fi - - # Check README has AI install section - if [ -f "$README" ]; then - if ! grep -qi 'AI-Assisted Installation' "$README" 2>/dev/null; then - echo "MISSING: AI-Assisted Installation section in $README" - echo " Copy from docs/AI-INSTALL-README-SECTION.adoc" - ERRORS=$((ERRORS + 1)) - fi - - # Check README for unfilled TODO markers - README_TODOS=$(grep -c '\[TODO-AI-INSTALL' "$README" 2>/dev/null || true) - if [ "$README_TODOS" -gt 0 ]; then - echo "INCOMPLETE: $README has $README_TODOS unfilled [TODO-AI-INSTALL] markers" - ERRORS=$((ERRORS + 1)) - fi - fi - - if [ "$ERRORS" -gt 0 ]; then - echo "" - echo "AI install guide: FAIL ($ERRORS issues)" - exit 1 - fi - echo "AI install guide: PASS" - -# Full validation suite -validate: validate-rsr validate-state validate-ai-install - @echo "All validations passed!" diff --git a/build/setup.sh b/build/setup.sh deleted file mode 100755 index f652bf4..0000000 --- a/build/setup.sh +++ /dev/null @@ -1,294 +0,0 @@ -#!/bin/sh -# SPDX-License-Identifier: MPL-2.0 -# setup.sh — Universal setup script for rsr-template-repo -# -# Detects your shell, platform, and installs prerequisites. -# Then hands off to `just setup` for project-specific configuration. -# -# hypatia: allow code_safety/shell_download_then_run -- the only remote fetch -# (install_just_upstream) deliberately downloads to a temp file and runs that -# file rather than piping `curl | sh`, so the script can be inspected; the -# upstream just installer is a rolling script that cannot be checksum-pinned. -# -# Usage: -# curl -fsSL https://raw.githubusercontent.com/hyperpolymath/rsr-template-repo/main/setup.sh -o setup.sh && sh setup.sh -# # or after cloning: -# ./setup.sh -# -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) - -set -eu - -# ── Colours (safe — uses symbols too per ADJUST contractile) ── -if [ -t 1 ] && command -v tput >/dev/null 2>&1; then - RED=$(tput setaf 1 2>/dev/null || true) - GREEN=$(tput setaf 2 2>/dev/null || true) - YELLOW=$(tput setaf 3 2>/dev/null || true) - CYAN=$(tput setaf 6 2>/dev/null || true) - BOLD=$(tput bold 2>/dev/null || true) - RESET=$(tput sgr0 2>/dev/null || true) -else - RED="" GREEN="" YELLOW="" CYAN="" BOLD="" RESET="" -fi - -ok() { printf " %s[OK]%s %s\n" "$GREEN" "$RESET" "$1"; } -fail() { printf " %s[FAIL]%s %s\n" "$RED" "$RESET" "$1"; } -warn() { printf " %s[WARN]%s %s\n" "$YELLOW" "$RESET" "$1"; } -info() { printf " %s[INFO]%s %s\n" "$CYAN" "$RESET" "$1"; } - -# ── Shell Detection ── -detect_shell() { - # Check the actual running shell, not just $SHELL - CURRENT_SHELL="unknown" - - if [ -n "${BASH_VERSION:-}" ]; then CURRENT_SHELL="bash" - elif [ -n "${ZSH_VERSION:-}" ]; then CURRENT_SHELL="zsh" - elif [ -n "${FISH_VERSION:-}" ]; then CURRENT_SHELL="fish" - elif [ -n "${KSH_VERSION:-}" ]; then CURRENT_SHELL="ksh" - # Check by process name for shells that don't set version vars - elif command -v ps >/dev/null 2>&1; then - SHELL_PROC=$(ps -p $$ -o comm= 2>/dev/null || echo "unknown") - case "$SHELL_PROC" in - *dash*) CURRENT_SHELL="dash" ;; - *tcsh*) CURRENT_SHELL="tcsh" ;; - *csh*) CURRENT_SHELL="csh" ;; - *elvish*) CURRENT_SHELL="elvish" ;; - *nu*) CURRENT_SHELL="nushell" ;; - *oil*|*osh*) CURRENT_SHELL="oil" ;; - *xonsh*) CURRENT_SHELL="xonsh" ;; - *murex*) CURRENT_SHELL="murex" ;; - *ion*) CURRENT_SHELL="ion" ;; - *hilbish*) CURRENT_SHELL="hilbish" ;; - *oh*) CURRENT_SHELL="oh" ;; - *vsh*) CURRENT_SHELL="vsh" ;; - *pwsh*|*powershell*) CURRENT_SHELL="powershell" ;; - esac - fi - - # Fallback: check $SHELL env var - if [ "$CURRENT_SHELL" = "unknown" ] && [ -n "${SHELL:-}" ]; then - case "$SHELL" in - */bash) CURRENT_SHELL="bash" ;; - */zsh) CURRENT_SHELL="zsh" ;; - */fish) CURRENT_SHELL="fish" ;; - */dash) CURRENT_SHELL="dash" ;; - */ksh*) CURRENT_SHELL="ksh" ;; - */tcsh) CURRENT_SHELL="tcsh" ;; - */csh) CURRENT_SHELL="csh" ;; - */vsh) CURRENT_SHELL="vsh" ;; - esac - fi - - printf "%s" "$CURRENT_SHELL" -} - -# ── Platform Detection ── -detect_platform() { - OS="unknown" - DISTRO="unknown" - PKG_MGR="unknown" - ARCH=$(uname -m 2>/dev/null || echo "unknown") - - case "$(uname -s 2>/dev/null)" in - Linux*) - OS="linux" - if [ -f /etc/os-release ]; then - DISTRO=$(. /etc/os-release && echo "$ID") - elif [ -f /etc/redhat-release ]; then - DISTRO="rhel" - elif [ -f /etc/debian_version ]; then - DISTRO="debian" - fi - # Detect package manager - if command -v dnf >/dev/null 2>&1; then PKG_MGR="dnf" - elif command -v apt-get >/dev/null 2>&1; then PKG_MGR="apt" - elif command -v pacman >/dev/null 2>&1; then PKG_MGR="pacman" - elif command -v apk >/dev/null 2>&1; then PKG_MGR="apk" - elif command -v zypper >/dev/null 2>&1; then PKG_MGR="zypper" - elif command -v rpm-ostree >/dev/null 2>&1; then PKG_MGR="rpm-ostree" - elif command -v guix >/dev/null 2>&1; then PKG_MGR="guix" - fi - ;; - Darwin*) - OS="macos" - DISTRO="macos" - if command -v brew >/dev/null 2>&1; then PKG_MGR="brew" - elif command -v port >/dev/null 2>&1; then PKG_MGR="macports" - fi - ;; - CYGWIN*|MINGW*|MSYS*) - OS="windows" - DISTRO="msys" - if command -v winget >/dev/null 2>&1; then PKG_MGR="winget" - elif command -v scoop >/dev/null 2>&1; then PKG_MGR="scoop" - elif command -v choco >/dev/null 2>&1; then PKG_MGR="choco" - fi - ;; - FreeBSD*) - OS="freebsd" - DISTRO="freebsd" - PKG_MGR="pkg" - ;; - esac -} - -# ── Install just ── -# Fetch-then-run rather than `curl | sh`: piping a remote script straight into a -# shell executes whatever the network returns with no chance to inspect or -# verify it (CWE-494). Download to a temp file first, then run that file. -install_just_upstream() { - _ji_tmp=$(mktemp 2>/dev/null || echo "/tmp/just-install.$$.sh") - if curl -fsSL https://just.systems/install.sh -o "$_ji_tmp"; then - sh "$_ji_tmp" --to /usr/local/bin - _ji_rc=$? - else - fail "Could not download the just installer." - _ji_rc=1 - fi - rm -f "$_ji_tmp" - return $_ji_rc -} - -install_just() { - if command -v just >/dev/null 2>&1; then - ok "just already installed: $(just --version 2>/dev/null | head -1)" - return 0 - fi - - info "Installing just (task runner)..." - - case "$PKG_MGR" in - dnf) sudo dnf install -y just ;; - apt) sudo apt-get install -y just 2>/dev/null || install_just_upstream ;; - pacman) sudo pacman -S --noconfirm just ;; - apk) sudo apk add just ;; - brew) brew install just ;; - scoop) scoop install just ;; - winget) winget install Casey.Just ;; - rpm-ostree) sudo rpm-ostree install just ;; - guix) guix install just ;; - *) - info "Using just installer script..." - install_just_upstream - ;; - esac - - if command -v just >/dev/null 2>&1; then - ok "just installed: $(just --version 2>/dev/null | head -1)" - else - fail "Could not install just. Install manually: https://just.systems/" - return 1 - fi -} - -# ── Main ── -main() { - printf "%s=== rsr-template-repo Setup ===%s\n\n" "$BOLD" "$RESET" - - # Detect environment - SHELL_NAME=$(detect_shell) - detect_platform - - info "Shell: $SHELL_NAME" - info "Platform: $OS ($DISTRO)" - info "Arch: $ARCH" - info "Packages: $PKG_MGR" - printf "\n" - - # Warn about exotic shells - case "$SHELL_NAME" in - vsh) - info "Valence Shell detected — experimental support" - info "Falling back to POSIX sh for setup, vsh for post-setup" - ;; - nushell|elvish|murex|ion|hilbish|oil|xonsh|oh) - info "$SHELL_NAME detected — using POSIX sh for setup" - ;; - esac - - # Step 1: Install just - printf "%sStep 1: Install task runner%s\n" "$BOLD" "$RESET" - install_just || { fail "Cannot proceed without just"; exit 1; } - printf "\n" - - # Step 2: Check if we're in the repo directory - if [ ! -f "Justfile" ] && [ ! -f "justfile" ]; then - warn "Not in a repo directory (no Justfile found)" - info "Clone first: git clone https://github.com/hyperpolymath/rsr-template-repo.git" - info "Then: cd rsr-template-repo && ./setup.sh" - exit 1 - fi - - # Step 3: Run just setup - printf "%sStep 2: Project setup%s\n" "$BOLD" "$RESET" - if just --list 2>/dev/null | grep -q "^setup "; then - just setup - elif just --list 2>/dev/null | grep -q "^setup-dev "; then - just setup-dev - else - warn "No 'setup' recipe in Justfile — running 'just doctor' instead" - just doctor 2>/dev/null || true - fi - printf "\n" - - # Step 4: Post-install security snapshot - printf "%sStep 3: Security snapshot%s\n" "$BOLD" "$RESET" - if command -v firewall-cmd >/dev/null 2>&1; then - if firewall-cmd --state 2>/dev/null | grep -q running; then - ok "Firewall: firewalld active" - else - warn "Firewall: firewalld installed but not running" - info " Enable: sudo systemctl enable --now firewalld" - fi - elif command -v ufw >/dev/null 2>&1; then - if ufw status 2>/dev/null | grep -q "Status: active"; then - ok "Firewall: ufw active" - else - warn "Firewall: ufw installed but not active" - info " Enable: sudo ufw enable" - fi - else - warn "Firewall: none detected" - case "$PKG_MGR" in - dnf|rpm-ostree) info " Install: sudo dnf install firewalld && sudo systemctl enable --now firewalld" ;; - apt) info " Install: sudo apt install ufw && sudo ufw enable" ;; - *) info " Install a firewall for your platform" ;; - esac - fi - - if command -v getenforce >/dev/null 2>&1; then - SE_STATUS=$(getenforce 2>/dev/null || echo "unknown") - case "$SE_STATUS" in - Enforcing) ok "SELinux: Enforcing" ;; - Permissive) warn "SELinux: Permissive (recommend Enforcing: sudo setenforce 1)" ;; - *) warn "SELinux: $SE_STATUS" ;; - esac - fi - - # Write report - REPORT_FILE="INSTALL-SECURITY-REPORT.adoc" - { - printf "// SPDX-License-Identifier: MPL-2.0\n" - printf "= Install Security Report\n" - printf ":date: %s\n\n" "$(date -Iseconds 2>/dev/null || date)" - printf "== Platform\n" - printf "* OS: %s (%s)\n" "$OS" "$DISTRO" - printf "* Arch: %s\n" "$ARCH" - printf "* Package manager: %s\n" "$PKG_MGR" - printf "* Shell: %s\n\n" "$SHELL_NAME" - printf "== Security Status\n" - printf "Run \`just doctor\` for full diagnostic.\n" - } > "$REPORT_FILE" - info "Security report: $REPORT_FILE" - printf "\n" - - # Done - printf "%s=== Setup Complete ===%s\n\n" "${BOLD}${GREEN}" "$RESET" - printf "Next steps:\n" - printf " just doctor — verify everything works\n" - printf " just tour — guided tour of the project\n" - printf " just build — build the project\n" - printf " just help-me — get help if stuck\n" -} - -main "$@" diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index aca702c..f66866d 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -1,94 +1,72 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell -// Template: rsr-template-repo/docs/status/PROOF-STATUS.adoc -// Tracks proof completion. Requirements defined in PROOF-NEEDS.adoc -= Proof Status — {{PROJECT}} += Proof Status — anytype -== Summary +The single source of truth for "does the Idris2 in this repo compile?" is +`scripts/check-idris2-proofs.sh` (run as `just proof-check-idris2`, and in CI +by `.github/workflows/idris2-proof.yml`). Its MANIFEST lists every `.idr` +file as `gated` (must compile) or `quarantine` (known-broken, must keep +failing); an unlisted module is an error. This page summarises; the script +decides. -[cols="2,1,1,1,1,1", options="header"] -|=== -| Category | Total | Done | In Progress | Blocked | Remaining - -| ABI/FFI (ABI) | 5 | 0 | 0 | 0 | 5 -| Typing (TP) | 2 | 0 | 0 | 0 | 2 -| Invariant (INV) | 0 | 0 | 0 | 0 | 0 -| Security (SEC) | 0 | 0 | 0 | 0 | 0 -| Concurrency (CONC) | 0 | 0 | 0 | 0 | 0 -| Algorithm (ALG) | 0 | 0 | 0 | 0 | 0 -| Domain (DOM) | 0 | 0 | 0 | 0 | 0 -| *Total* | *7* | *0* | *0* | *0* | *7* -|=== - -*Overall*: 0% proven +== What is actually proven (gated, `%default total`, no escape hatches) -== Proofs Done - -// Format: -// | ID | Proof | Prover | File | Date | Verified By | -// | ABI-1 | Non-null pointer proofs | Idris2 | verification/proofs/idris2/ABI/Pointers.idr | 2026-XX-XX | idris2 --check | - -[cols="1,3,1,3,1,2", options="header"] +[cols="2,3,3", options="header"] |=== -| ID | Proof | Prover | File | Date | Verified By - -| — | No proofs completed yet | — | — | — | — +| Area | Modules | What the proofs say + +| L2 grade algebras +| `src/kernel/Anytype/Grade/{Algebra,Affine,Exact}.idr` +| `GradeAlgebra` carries its ordered-semiring laws as proof fields, so an +unlawful algebra is unrepresentable. The affine `{0,1,ω}` instance (mirroring +AffineScript `lib/quantity.ml`) and the exact-usage `ℕ` instance discharge +every law — associativity, commutativity, identities, annihilation, +distributivity, order reflexivity/transitivity/antisymmetry, and +monotonicity of both operations. + +| L1 totality +| `src/kernel/Anytype/Core/{Syntax,Normalise,Conversion,Check}.idr` +| The type-index language has no recursion constructor and `normalise` is +machine-checked total, so conversion (normalise-and-compare) is decidable by +construction. This is a syntactic totality gate, not a termination analysis. + +| Seam encodings +| `src/interface/Abi/Types.idr` +| Discipline and verdict wire codes are injective; decoding inverts encoding. + +| Seam layouts +| `src/interface/Abi/Layout.idr` +| `anytype_request_t` / `anytype_response_t` (16 bytes, align 8) are proven +`CABICompliant`; the Zig side comptime-asserts the same numbers, so a layout +drift on either side breaks a gate. |=== -== Proofs In Progress +== Quarantined (RSR template stock, never compiled) -[cols="1,3,1,2,1,2", options="header"] -|=== -| ID | Proof | Prover | Assignee | Started | Blocker +Five modules under `verification/proofs/idris2/` are template inheritance +that predates the kernel and does not compile (missing `Data.Nat` imports; +one erased-field projection). They are quarantined in the MANIFEST with +per-module reasons: the gate requires them to KEEP failing, and flags them +for promotion if one starts passing. `ABI/Foreign.idr` is the one template +module that compiles and is gated. Their fate (fix or delete) is tracked in +`STATE.a2ml` critical-next-actions. -| — | — | — | — | — | — -|=== +== Not proven (open obligations) -== Proofs Blocked +* Type safety (progress/preservation) of the L1 checker — the checker is + executable and golden-tested, not yet accompanied by a soundness proof. +* systemet's theory obligations (L1 soundness/completeness of + conversion-as-equality, trope preservation, TEA erasure) live upstream in + systemet and are all open there. +* The Agda/Coq/Lean4/TLA+ stubs under `verification/proofs/` are untouched + template files with no gate; they claim nothing. -[cols="1,3,2,3", options="header"] -|=== -| ID | Proof | Blocked By | Notes - -| — | — | — | — -|=== +== Verification commands -== Proofs Remaining - -[cols="1,3,1,1,1,1", options="header"] -|=== -| ID | Proof | Category | Prover | Priority | Est. Effort - -| ABI-1 | Non-null pointer proofs | ABI | Idris2 | P1 | 2h -| ABI-2 | Memory layout correctness | ABI | Idris2 | P1 | 4h -| ABI-3 | Platform type size proofs | ABI | Idris2 | P1 | 2h -| ABI-4 | FFI function return type proofs | ABI | Idris2 | P1 | 2h -| ABI-5 | C ABI compliance | ABI | Idris2 | P1 | 4h -| TP-1 | Core data type well-formedness | TP | Idris2 | P1 | 4h -| TP-2 | Public API type safety | TP | Lean4 | P2 | 4h -|=== - -== Verification Commands - -[source,bash] +[source,sh] ---- -# Check all Idris2 proofs -just proof-check-idris2 - -# Check all Lean4 proofs -just proof-check-lean4 - -# Check all Agda proofs -just proof-check-agda - -# Check all Coq proofs -just proof-check-coq - -# Run all proof checks -just proof-check-all - -# Scan for dangerous patterns -panic-attack assail --proofs-only +just proof-check-idris2 # every .idr, manifest-gated, hard-fails without idris2 +just test # kernel build + 19-case golden matrix + seam tests ---- == Changelog @@ -98,4 +76,5 @@ panic-attack assail --proofs-only | Date | Change | By | 2026-04-04 | Initial proof status tracking | Template +| 2026-07-21 | Re-scoped from template to the real kernel: gated/quarantine MANIFEST, law-field proofs, layout proofs | MVP kernel work |=== diff --git a/docs/status/ROADMAP.adoc b/docs/status/ROADMAP.adoc index bafe0ce..fe37b46 100644 --- a/docs/status/ROADMAP.adoc +++ b/docs/status/ROADMAP.adoc @@ -1,23 +1,33 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell -= YOUR Template Repo Roadmap += anytype Roadmap -== Current Status +Mirrors `[route-to-mvp]` in `.machine_readable/6a2/STATE.a2ml` (which is the +machine-readable source of truth). -Initial development phase. +== Done -== Milestones +* [x] Phase 0 — split the kernel out of the EveryType draft; RSR repo +* [x] Phase 2 — L2 grade-algebra interface (laws as proof fields) + affine + `{0,1,ω}` and exact-usage `ℕ` instances +* [x] Phase 3 — L1 conversion checker (normalise-and-compare) + syntactic + totality gate, with the 19-case golden matrix +* [x] Phase 4 — anytype-specific seam: `Abi.{Types,Layout,Foreign}` rewritten + from the template, `anytype-check` CLI, Zig `anytype_check` export with + comptime layout asserts (MVP transport: spawned process) -=== v0.1.0 - Foundation -* [ ] Core functionality -* [ ] Basic documentation -* [ ] CI/CD pipeline +== Next -=== v1.0.0 - Stable Release -* [ ] Full feature set -* [ ] Comprehensive tests -* [ ] Production ready +* [ ] Phase 1 residue — finish the design write-up (currently 80%) +* [ ] Branching in L1 — needs a grade join beyond the stated semiring+order + laws; design against systemet first, then extend `GradeAlgebra` +* [ ] Phase 5 — L3 guarded recursion; L0 lowering target +* [ ] In-process seam — link the kernel via the RefC backend instead of + spawning `anytype-check` +* [ ] Quarantined template proofs — fix or delete the five never-compiling + modules under `verification/proofs/idris2/` (see the MANIFEST) -== Future Directions +== Blocked -_To be determined based on community feedback._ +* Phase 6 — L4 effect handlers + TEA erasure: gated on systemet's open + TEA-erasure result (the headline open problem upstream). diff --git a/mise.toml b/mise.toml index 6dd983f..360c2b5 100644 --- a/mise.toml +++ b/mise.toml @@ -1,57 +1,5 @@ [tools] -# Language runtimes -node = "latest" -python = "latest" -rust = "latest" -go = "latest" -zig = "latest" -java = "latest" -bun = "latest" -denojs = "latest" - -# Package managers -npm = "latest" -yarn = "latest" -pnpm = "latest" -pip = "latest" -cargo = "latest" -go-task = "latest" - -# Formatting & Linting -gofmt = "latest" -black = "latest" -isort = "latest" -ruff = "latest" -prettier = "latest" -shfmt = "latest" -stylua = "latest" - -# Build tools -cmake = "latest" -make = "latest" -ninja = "latest" - -# Shell tools -git = "latest" -gnu-sed = "latest" -gnu-tar = "latest" -gnu-grep = "latest" - -# Testing -vitest = "latest" -pytest = "latest" -jest = "latest" - -[env] -# Common environment variables -NODE_ENV = "development" -PYTHONDONTWRITEBYTECODE = "1" -PYTHONUNBUFFERED = "1" - -# Task runner alias -[alias] -task = "go-task" -build = "cargo build --release || npm run build || go build" -test = "cargo test || npm test || go test ./..." -lint = "ruff check . || prettier --check . || black --check ." -fmt = "ruff format . || prettier --write . || black ." +# Kernel toolchain (see .tool-versions for authoritative pins) +idris2 = "0.7.0" +zig = "0.16.0" +rust = "nightly" diff --git a/scripts/check-cli.sh b/scripts/check-cli.sh new file mode 100755 index 0000000..8c0cdd5 --- /dev/null +++ b/scripts/check-cli.sh @@ -0,0 +1,44 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Golden tests for the anytype-check process-boundary seam: verdict lines +# AND exit codes (which are the wire contract — Abi.Types.verdictCode). +# Build first: idris2 --build anytype-cli.ipkg (just test does this). +set -euo pipefail +cd "$(dirname "${BASH_SOURCE[0]}")/.." + +BIN=./build/exec/anytype-check +[ -x "$BIN" ] || { echo "FAIL: $BIN not built (run: just test)"; exit 1; } + +fails=0 + +case_check() { + local desc="$1" disc="$2" term="$3" want_exit="$4" want_prefix="$5" + local out rc + set +e + out="$(echo "$term" | "$BIN" --discipline "$disc" 2>&1)" + rc=$? + set -e + if [ "$rc" -eq "$want_exit" ] && [[ "$out" == "$want_prefix"* ]]; then + echo " PASS $desc" + else + echo " FAIL $desc (want exit=$want_exit '$want_prefix...', got exit=$rc '$out')" + fails=$((fails + 1)) + fi +} + +echo "=== anytype-check seam golden tests ===" +case_check "affine: use once accepted" affine '(lam 1 bool (var 0))' 0 "ACCEPT" +case_check "affine: drop accepted" affine '(lam 1 bool tt)' 0 "ACCEPT" +case_check "affine: double use rejected" affine '(lam 1 bool (pair (var 0) (var 0)))' 1 "REJECT" +case_check "exact: drop rejected (the split)" exact '(lam 1 bool tt)' 1 "REJECT" +case_check "exact: double use at 2 accepted" exact '(lam 2 bool (pair (var 0) (var 0)))' 0 "ACCEPT" +case_check "conversion: (word (+ 2 3)) is Bits 5" affine '(word (+ 2 3))' 0 "ACCEPT Bits 5" +case_check "ill-formed input is exit 2" affine 'garbage((' 2 "ILLFORMED" +case_check "ill-scoped term is exit 2" affine '(var 0)' 2 "ILLFORMED" + +echo +if [ "$fails" -gt 0 ]; then + echo "RESULT: FAIL ($fails failure(s))" + exit 1 +fi +echo "RESULT: PASS" diff --git a/scripts/check-idris2-proofs.sh b/scripts/check-idris2-proofs.sh new file mode 100755 index 0000000..a086a19 --- /dev/null +++ b/scripts/check-idris2-proofs.sh @@ -0,0 +1,166 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <6759885+hyperpolymath@users.noreply.github.com> +# +# Type-check every Idris2 module in the repository. +# +# This script is the single source of truth for "does the Idris2 in this repo +# compile?". Both CI (.github/workflows/idris2-proof.yml) and the Justfile +# (`just proof-check-idris2`) call it, so a green local run and a green CI run +# mean the same thing. +# +# Adapted from ideas-to-alphas scripts/check-idris2-proofs.sh, which documents +# why each rule exists. The estate-wide failure mode it replaces: the old +# build/just/proofs.just recipe did `exit 0` when idris2 was absent, so every +# proof in this repo reported green on machines where nothing could check them. +# If you extend this script, the test to apply is not "does it pass?" but +# "have I watched it fail?". +# +# Three rules: +# * A missing toolchain is a FAILURE, never a skip. +# * Every module is checked from its own source root (module ABI.Foreign +# lives at /ABI/Foreign.idr; a wrong root fails on the name, not on +# the real errors). +# * A module that is not in the MANIFEST is an error. New Idris2 anywhere +# in the tree is gated by default; you cannot add an unchecked proof. +# +# Exit codes: 0 = all gated modules check and all quarantined modules still +# fail as expected; 1 = otherwise. + +set -euo pipefail + +cd "$(dirname "${BASH_SOURCE[0]}")/.." +ROOT="$PWD" + +# --- MANIFEST ----------------------------------------------------------------- +# Format: |||| +# +# gated -- must type-check. A failure fails this script and CI. +# quarantine -- known-broken RSR template stock, kept for reference. Must +# CONTINUE to fail; if one starts passing the script fails and +# tells you to promote it, so the list cannot silently rot. +# Verdicts measured 2026-07-21 under Idris2 0.7.0. +MANIFEST=( + "src/kernel|Anytype/Grade/Algebra.idr|gated||L2 grade-algebra interface: laws are proof fields" + "src/kernel|Anytype/Grade/Affine.idr|gated||{0,1,omega} instance mirroring affinescript lib/quantity.ml" + "src/kernel|Anytype/Grade/Exact.idr|gated||exact-usage Nat instance: the distinct-discipline demo" + "src/kernel|Anytype/Core/Syntax.idr|gated||graded STLC syntax; TNat total by construction" + "src/kernel|Anytype/Core/Normalise.idr|gated||the L1 totality artefact" + "src/kernel|Anytype/Core/Conversion.idr|gated||normalise-and-compare" + "src/kernel|Anytype/Core/Check.idr|gated||usage-counting bidirectional checker" + "src/kernel|Anytype/Kernel.idr|gated||public API" + "src/interface|Abi/Types.idr|gated||ABI seam types" + "src/interface|Abi/Layout.idr|gated||ABI layout proofs" + "src/interface|Abi/Foreign.idr|gated||ABI FFI declarations" + ".machine_readable/coaptation/core|Coaptation.idr|gated||coaptation skeleton; compiles, semantically a placeholder" + "verification/tests/kernel|Tests/Main.idr|gated|-p anytype|golden matrix; needs anytype installed (just test does this)" + "src/cli|Anytype/Sexp.idr|gated|-p anytype|total S-expression reader for the seam wire format" + "src/cli|Anytype/Main.idr|gated|-p anytype -p anytype-abi|anytype-check entry point; exit codes = Abi.Types verdictCode" + "verification/proofs/idris2|ABI/Foreign.idr|gated||the one template verification module that compiles" + "verification/proofs/idris2|Types.idr|quarantine||RSR template stock, never compiled: LTE needs Data.Nat" + "verification/proofs/idris2|ABI/Platform.idr|quarantine||template stock: LTE needs Data.Nat, then undefined lteRefl" + "verification/proofs/idris2|ABI/Layout.idr|quarantine||template stock: NonZero/modNatNZ need Data.Nat" + "verification/proofs/idris2|ABI/Pointers.idr|quarantine||template stock: erased .nonNull projected into a value position" + "verification/proofs/idris2|ABI/Compliance.idr|quarantine||depends on quarantined ABI.Layout" +) + +# --- toolchain: absent means FAIL, never skip --------------------------------- +if ! command -v idris2 >/dev/null 2>&1; then + cat >&2 <<'EOF' +FAIL: idris2 not found on PATH. + +This is deliberately fatal. The recipe this script replaces did `exit 0` here +with "SKIP: idris2 not installed", which meant every proof in this repo +reported green on machines where nothing could check them. An unrunnable gate +that reports success is worse than no gate: it manufactures false confidence. + +Install Idris2 0.7.0, or run this in CI where the workflow installs it. +EOF + exit 1 +fi + +echo "=== Idris2 proof check ===" +idris2 --version +echo + +# --- verdict ------------------------------------------------------------------ +# `idris2 --check` EXITS 0 ON A MISSING IMPORT while printing "Error: Module X +# not found". Testing $? alone is therefore unsound. We require BOTH a zero +# exit AND no "Error:" in the output. +check_module() { + local root="$1" rel="$2" args="$3" out rc + set +e + # shellcheck disable=SC2086 + out="$(cd "$ROOT/$root" && idris2 $args --check "$rel" 2>&1)" + rc=$? + set -e + if [ "$rc" -eq 0 ] && ! grep -q '^Error:' <<<"$out"; then + LAST_OUT="" + return 0 + fi + LAST_OUT="$out" + return 1 +} + +fails=0 +unexpected_pass=0 + +for entry in "${MANIFEST[@]}"; do + IFS='|' read -r root rel status args note <<<"$entry" + printf ' %-34s %-22s ' "$root" "$rel" + + if check_module "$root" "$rel" "$args"; then + if [ "$status" = "gated" ]; then + echo "PASS" + else + echo "PASS -- UNEXPECTED" + echo " This module is marked 'quarantine' but now type-checks." + echo " Promote it to 'gated' in the MANIFEST and update PROOF-STATUS." + unexpected_pass=$((unexpected_pass + 1)) + fi + else + if [ "$status" = "gated" ]; then + echo "FAIL" + printf '%s\n' "${LAST_OUT//$'\n'/$'\n '}" | sed '1s/^/ /' + fails=$((fails + 1)) + else + echo "fail (quarantined, expected)" + echo " reason: $note" + fi + fi +done + +# --- no unlisted Idris2 anywhere in the tree ---------------------------------- +# The anti-recurrence rule: a module absent from the MANIFEST is an error, so +# new Idris2 is gated by default rather than by remembering. +echo +echo "=== manifest coverage ===" +listed="$(for e in "${MANIFEST[@]}"; do IFS='|' read -r r m _ _ _ <<<"$e"; echo "$r/$m"; done | sort)" +found="$(find . -name '*.idr' -not -path './.git/*' -not -path '*/build/*' -not -path './.claude/*' \ + | sed 's|^\./||' | sort)" +unlisted="$(comm -13 <(echo "$listed") <(echo "$found") || true)" +missing="$(comm -23 <(echo "$listed") <(echo "$found") || true)" + +if [ -n "$unlisted" ]; then + echo "FAIL: Idris2 modules present on disk but absent from the MANIFEST:" + printf ' %s\n' "${unlisted//$'\n'/$'\n '}" + echo + echo " Every .idr in this repo must be listed in scripts/check-idris2-proofs.sh," + echo " as 'gated' (it must compile) or 'quarantine' (known-broken, tracked)." + fails=$((fails + 1)) +fi + +if [ -n "$missing" ]; then + echo "FAIL: MANIFEST lists modules that do not exist (stale entries):" + printf ' %s\n' "${missing//$'\n'/$'\n '}" + fails=$((fails + 1)) +fi + +[ -z "$unlisted$missing" ] && echo " all $(echo "$found" | wc -l | tr -d ' ') .idr files accounted for" + +echo +if [ "$fails" -gt 0 ] || [ "$unexpected_pass" -gt 0 ]; then + echo "RESULT: FAIL ($fails failure(s), $unexpected_pass unexpected pass(es))" + exit 1 +fi +echo "RESULT: PASS -- all gated modules type-check; quarantined modules still fail as recorded" diff --git a/src/cli/Anytype/Main.idr b/src/cli/Anytype/Main.idr new file mode 100644 index 0000000..f5acd90 --- /dev/null +++ b/src/cli/Anytype/Main.idr @@ -0,0 +1,56 @@ +||| anytype-check: the kernel's stable process-boundary entry point. +||| +||| Usage: echo '' | anytype-check --discipline affine|exact +||| +||| Output (one line) and exit code follow Abi.Types.verdictCode: +||| ACCEPT exit 0 (VAccepted) +||| REJECT exit 1 (VRejected) +||| ILLFORMED exit 2 (VIllFormed) +||| The Zig side (src/interface/ffi) maps these back to anytype_check's +||| C return value; the codes are proven injective in Abi.Types. +module Anytype.Main + +import System +import Abi.Types +import Anytype.Kernel +import Anytype.Sexp + +%default total + +-- Exit codes are verdictCode values; the literals let ExitFailure's +-- nonzero proof discharge by computation (Abi.Types proves them +-- injective, disciplineRoundTrip ties decode to encode). +exitVerdict : Verdict -> IO () +exitVerdict VAccepted = exitWith ExitSuccess +exitVerdict VRejected = exitWith (ExitFailure 1) +exitVerdict VIllFormed = exitWith (ExitFailure 2) + +run : (pg : String -> Maybe g) -> (GradeAlgebra g) -> (g -> String) -> + String -> IO () +run pg alg sg input = + case parseClosed pg input of + Nothing => do + putStrLn "ILLFORMED unreadable or ill-scoped term" + exitVerdict VIllFormed + Just t => + case checkClosed alg t of + Right ty => do + putStrLn ("ACCEPT " ++ showTy sg ty) + exitVerdict VAccepted + Left err => do + putStrLn ("REJECT " ++ show err) + exitVerdict VRejected + +usage : IO () +usage = do + putStrLn "ILLFORMED usage: anytype-check --discipline affine|exact" + exitVerdict VIllFormed + +main : IO () +main = do + args <- getArgs + input <- getLine + case args of + [_, "--discipline", "affine"] => run affineGrade AffineAlgebra show input + [_, "--discipline", "exact"] => run exactGrade ExactAlgebra show input + _ => usage diff --git a/src/cli/Anytype/Sexp.idr b/src/cli/Anytype/Sexp.idr new file mode 100644 index 0000000..2dcfa36 --- /dev/null +++ b/src/cli/Anytype/Sexp.idr @@ -0,0 +1,127 @@ +||| Total S-expression reader for the anytype seam wire format. +||| +||| Grammar (one term per input): +||| term := (lam ) | (app ) +||| | (pair ) | (letpair ) +||| | (var ) | (word ) | tt | true | false +||| ty := unit | bool | (bits ) +||| | (arr ) | (prod ) +||| tnat := | (+ ) | (* ) +||| Grades are discipline-specific atoms: affine 0|1|w, exact . +||| +||| Everything here is `%default total`: the tokeniser is structural on +||| the character list and the reader burns explicit fuel (the token +||| count), so the seam cannot hang on malformed input. +module Anytype.Sexp + +import Data.String +import Data.Fin +import Anytype.Kernel + +%default total + +data Tok = TOpen | TClose | TAtom String + +flush : List Char -> List Tok -> List Tok +flush [] ts = ts +flush acc ts = TAtom (pack (reverse acc)) :: ts + +tokGo : List Char -> List Char -> List Tok +tokGo acc [] = flush acc [] +tokGo acc (c :: cs) = + if c == '(' then flush acc (TOpen :: tokGo [] cs) + else if c == ')' then flush acc (TClose :: tokGo [] cs) + else if isSpace c then flush acc (tokGo [] cs) + else tokGo (c :: acc) cs + +tokenise : String -> List Tok +tokenise s = tokGo [] (unpack s) + +public export +data SExp = SAtom String | SList (List SExp) + +mutual + readOne : (fuel : Nat) -> List Tok -> Maybe (SExp, List Tok) + readOne Z _ = Nothing + readOne (S _) (TAtom a :: r) = Just (SAtom a, r) + readOne (S f) (TOpen :: r) = do + (xs, r') <- readMany f r + pure (SList xs, r') + readOne _ _ = Nothing + + readMany : (fuel : Nat) -> List Tok -> Maybe (List SExp, List Tok) + readMany Z _ = Nothing + readMany (S _) (TClose :: r) = Just ([], r) + readMany (S f) toks = do + (x, r) <- readOne f toks + (xs, r') <- readMany f r + pure (x :: xs, r') + +||| Read exactly one S-expression covering the whole input. +public export +readSexp : String -> Maybe SExp +readSexp s = + let toks = tokenise s in + case readOne (S (length toks)) toks of + Just (e, []) => Just e + _ => Nothing + +parseTNat : SExp -> Maybe TNat +parseTNat (SAtom s) = map tnatOfNat (parsePositive s) +parseTNat (SList [SAtom "+", a, b]) = + [| NPlus (parseTNat a) (parseTNat b) |] +parseTNat (SList [SAtom "*", a, b]) = + [| NMul (parseTNat a) (parseTNat b) |] +parseTNat _ = Nothing + +parseTy : (pg : String -> Maybe g) -> SExp -> Maybe (Ty g) +parseTy _ (SAtom "unit") = Just TUnit +parseTy _ (SAtom "bool") = Just TBool +parseTy _ (SList [SAtom "bits", w]) = map TBits (parseTNat w) +parseTy pg (SList [SAtom "arr", SAtom q, a, b]) = + [| TArr (pg q) (parseTy pg a) (parseTy pg b) |] +parseTy pg (SList [SAtom "prod", a, b]) = + [| TProd (parseTy pg a) (parseTy pg b) |] +parseTy _ _ = Nothing + +||| Scope-checked term reader: de Bruijn indices are bounds-checked +||| against `n` as they are read, so an ill-scoped input is Nothing, +||| never a crash. +public export +parseTerm : (pg : String -> Maybe g) -> (n : Nat) -> SExp -> + Maybe (Term g n) +parseTerm _ n (SList [SAtom "var", SAtom k]) = do + kn <- parsePositive k + i <- natToFin kn n + pure (Var i) +parseTerm pg n (SList [SAtom "lam", SAtom q, ty, body]) = + [| Lam (pg q) (parseTy pg ty) (parseTerm pg (S n) body) |] +parseTerm pg n (SList [SAtom "app", f, x]) = + [| App (parseTerm pg n f) (parseTerm pg n x) |] +parseTerm pg n (SList [SAtom "pair", s, t]) = + [| Pair (parseTerm pg n s) (parseTerm pg n t) |] +parseTerm pg n (SList [SAtom "letpair", p, body]) = + [| LetPair (parseTerm pg n p) (parseTerm pg (S (S n)) body) |] +parseTerm _ _ (SAtom "tt") = Just TT +parseTerm _ _ (SAtom "true") = Just (BLit True) +parseTerm _ _ (SAtom "false") = Just (BLit False) +parseTerm _ n (SList [SAtom "word", w]) = map WordLit (parseTNat w) +parseTerm _ _ _ = Nothing + +||| Affine grades: 0 | 1 | w. +public export +affineGrade : String -> Maybe Q +affineGrade "0" = Just Q0 +affineGrade "1" = Just Q1 +affineGrade "w" = Just QW +affineGrade _ = Nothing + +||| Exact grades: any natural number. +public export +exactGrade : String -> Maybe Nat +exactGrade = parsePositive + +||| Parse a closed term from wire text. +public export +parseClosed : (pg : String -> Maybe g) -> String -> Maybe (Term g 0) +parseClosed pg s = readSexp s >>= parseTerm pg 0 diff --git a/src/interface/Abi/Foreign.idr b/src/interface/Abi/Foreign.idr index ca66b08..4683452 100644 --- a/src/interface/Abi/Foreign.idr +++ b/src/interface/Abi/Foreign.idr @@ -1,83 +1,33 @@ -- SPDX-License-Identifier: MPL-2.0 -- Copyright (c) Jonathan D.A. Jewell -||| Foreign Function Interface Bridge +||| anytype FFI surface. ||| -||| This module defines the raw FFI calls and their safe wrappers, -||| implemented in the Zig FFI layer. - +||| Replaces the RSR template's generic librsr binding. The C symbol +||| declared here is what the Zig side (src/interface/ffi) exports; the +||| MVP transport behind it is a spawned `anytype-check` process — see +||| src/interface/ffi/README.adoc. In-process linkage of the kernel +||| (RefC backend) is future work; this declaration is the seam contract, +||| stated so both sides agree on one signature. module Abi.Foreign import Abi.Types -import Abi.Layout %default total --------------------------------------------------------------------------------- --- Library Lifecycle --------------------------------------------------------------------------------- - -||| Raw FFI call to initialize the library -%foreign "C:rsr_init,librsr" -prim__init : PrimIO Bits64 - -||| Raw FFI call to free library resources -%foreign "C:rsr_free,librsr" -prim__free : Bits64 -> PrimIO () - -||| Safe wrapper for initialization -export -init : IO (Maybe Handle) -init = do - ptr <- primIO prim__init - pure (createHandle ptr) +||| Raw seam call: check `term` (UTF-8 S-expression, NUL-terminated) +||| under the discipline byte. Returns a verdict code (see +||| Abi.Types.verdictCode). Provided by libanytype (Zig). +%foreign "C:anytype_check,libanytype" +prim__anytypeCheck : Bits8 -> String -> PrimIO Bits8 -||| Safe wrapper for cleanup +||| Safe wrapper: typed discipline in, decoded verdict out. +||| A code outside verdictCode's range is reported as VIllFormed — +||| the seam never invents an acceptance. export -free : Handle -> IO () -free h = primIO (prim__free h.ptr) - --------------------------------------------------------------------------------- --- Core Operations --------------------------------------------------------------------------------- - -||| Raw FFI call for main processing -%foreign "C:rsr_process,librsr" -prim__process : Bits64 -> Bits32 -> PrimIO Bits32 - -||| Safe wrapper with error handling -export -process : Handle -> Bits32 -> IO (Either Result Bits32) -process h input = do - result <- primIO (prim__process h.ptr input) - if result == 0 - then pure (Left Error) - else pure (Right result) - --------------------------------------------------------------------------------- --- Status and Metrics --------------------------------------------------------------------------------- - -||| Get the current error description from the library -%foreign "C:rsr_get_error,librsr" -prim__getError : Bits64 -> PrimIO (Ptr String) - -||| Detailed error string helper -export -errorDescription : Result -> String -errorDescription Ok = "Success" -errorDescription Error = "Generic error" -errorDescription InvalidParam = "Invalid parameter" -errorDescription Busy = "Library is busy" - --------------------------------------------------------------------------------- --- Documentation --------------------------------------------------------------------------------- - -||| Summary of ABI safety properties: -||| 1. All functions are total (total keyword enforced). -||| 2. Pointers are verified non-null before being wrapped in Handle. -||| 3. Memory layouts are proven C-ABI compliant in Abi.Layout. -||| 4. FFI boundary uses explicitly tagged types from Abi.Types. -public export -abiSafetyGuarantees : String -abiSafetyGuarantees = "RSR-Template ABI: 4 proven safety properties for FFI integration" +anytypeCheck : Discipline -> String -> IO Verdict +anytypeCheck d term = do + code <- primIO (prim__anytypeCheck (disciplineCode d) term) + pure (case code of + 0 => VAccepted + 1 => VRejected + _ => VIllFormed) diff --git a/src/interface/Abi/Layout.idr b/src/interface/Abi/Layout.idr index e1f4275..d364adf 100644 --- a/src/interface/Abi/Layout.idr +++ b/src/interface/Abi/Layout.idr @@ -2,8 +2,11 @@ -- Copyright (c) Jonathan D.A. Jewell ||| ABI Layout Verification ||| -||| This module provides formal proofs about memory layout, alignment, -||| and padding for C-compatible structs. +||| Formal proofs about memory layout, alignment, and padding for the +||| C-compatible structs anytype actually passes across its seam. The +||| generic machinery (Divides, StructLayout, FieldsAligned) is inherited +||| from the RSR template; the layouts proven at the bottom are anytype's +||| own request/response structs. module Abi.Layout @@ -101,28 +104,60 @@ data CABICompliant : StructLayout -> Type where CABICompliant l -------------------------------------------------------------------------------- --- Example and Proofs +-- anytype wire structs -------------------------------------------------------------------------------- -||| Example: struct { int32_t x; int64_t y; double z; } -||| On 64-bit Linux, this should have size 24, alignment 8. +div1_0 : Divides 1 0 +div1_0 = MkDivides 0 Refl + +div4_4 : Divides 4 4 +div4_4 = MkDivides 1 Refl + +||| anytype_request_t on 64-bit targets: +||| struct { uint8_t discipline; /* pad 3 */ uint32_t term_len; +||| const uint8_t *term_utf8; } +||| Size 16, alignment 8. The Zig side asserts the same layout with +||| comptime @sizeOf/@offsetOf checks against these numbers. +public export +requestLayout : StructLayout +requestLayout = + MkStructLayout + [ MkField "discipline" 0 1 1 + , MkField "term_len" 4 4 4 + , MkField "term_utf8" 8 8 8 + ] + 16 + 8 + {aligned = div8_16} + +public export +requestLayoutValid : CABICompliant Abi.Layout.requestLayout +requestLayoutValid = CABIOk Abi.Layout.requestLayout ( + ConsField (MkField "discipline" 0 1 1) _ div1_0 ( + ConsField (MkField "term_len" 4 4 4) _ div4_4 ( + ConsField (MkField "term_utf8" 8 8 8) _ div8_8 ( + NoFields)))) + +||| anytype_response_t on 64-bit targets: +||| struct { uint8_t verdict; /* pad 3 */ uint32_t msg_len; +||| const uint8_t *msg_utf8; } +||| Size 16, alignment 8. public export -exampleLayout : StructLayout -exampleLayout = +responseLayout : StructLayout +responseLayout = MkStructLayout - [ MkField "x" 0 4 4 -- Bits32 at offset 0 - , MkField "y" 8 8 8 -- Bits64 at offset 8 (4 bytes padding) - , MkField "z" 16 8 8 -- Double at offset 16 + [ MkField "verdict" 0 1 1 + , MkField "msg_len" 4 4 4 + , MkField "msg_utf8" 8 8 8 ] - 24 -- Total size: 24 bytes - 8 -- Alignment: 8 bytes - {aligned = div8_24} + 16 + 8 + {aligned = div8_16} -||| Proof that example layout is valid public export -exampleLayoutValid : CABICompliant Abi.Layout.exampleLayout -exampleLayoutValid = CABIOk Abi.Layout.exampleLayout ( - ConsField (MkField "x" 0 4 4) _ div4_0 ( - ConsField (MkField "y" 8 8 8) _ div8_8 ( - ConsField (MkField "z" 16 8 8) _ div8_16 ( +responseLayoutValid : CABICompliant Abi.Layout.responseLayout +responseLayoutValid = CABIOk Abi.Layout.responseLayout ( + ConsField (MkField "verdict" 0 1 1) _ div1_0 ( + ConsField (MkField "msg_len" 4 4 4) _ div4_4 ( + ConsField (MkField "msg_utf8" 8 8 8) _ div8_8 ( NoFields)))) diff --git a/src/interface/Abi/Types.idr b/src/interface/Abi/Types.idr index 9d30051..e2c75a3 100644 --- a/src/interface/Abi/Types.idr +++ b/src/interface/Abi/Types.idr @@ -1,112 +1,72 @@ -- SPDX-License-Identifier: MPL-2.0 -- Copyright (c) Jonathan D.A. Jewell -||| ABI Type Definitions Template +||| anytype ABI wire types. ||| -||| This module defines the Application Binary Interface (ABI) for this library. -||| All type definitions include formal proofs of correctness. - +||| This module used to be the RSR template's generic ABI demo; it now +||| defines anytype's actual seam surface: the discipline selector and +||| the verdict a kernel check returns, with machine-checked facts about +||| their byte encodings (codes are injective and decoding inverts +||| encoding, so the Zig side can trust a reverse lookup). module Abi.Types -import Data.Bits -import Data.So -import Data.Vect -import Decidable.Equality - %default total --------------------------------------------------------------------------------- --- Platform Model --------------------------------------------------------------------------------- - -||| Target platforms for the FFI bridge -public export -data Platform = Linux | MacOS | Windows | WASM | RISCV - -||| Pointer size in bits per platform -public export -ptrSize : Platform -> Nat -ptrSize Linux = 64 -ptrSize MacOS = 64 -ptrSize Windows = 64 -ptrSize WASM = 32 -ptrSize RISCV = 64 - -||| Current target platform (detected at compile-time) +||| Which grade algebra the kernel should check under. public export -thisPlatform : Platform -thisPlatform = Linux -- Simplified for template - --------------------------------------------------------------------------------- --- Core Types --------------------------------------------------------------------------------- +data Discipline = DAffine | DExact -||| Return codes for FFI calls +||| Wire encoding of a discipline. public export -data Result = Ok | Error | InvalidParam | Busy +disciplineCode : Discipline -> Bits8 +disciplineCode DAffine = 0 +disciplineCode DExact = 1 -||| Results are decidably equal +||| The result of a kernel check, as seen across the ABI. public export -implementation DecEq Result where - decEq Ok Ok = Yes Refl - decEq Error Error = Yes Refl - decEq InvalidParam InvalidParam = Yes Refl - decEq Busy Busy = Yes Refl - decEq Ok Error = No (\case Refl impossible) - decEq Ok InvalidParam = No (\case Refl impossible) - decEq Ok Busy = No (\case Refl impossible) - decEq Error Ok = No (\case Refl impossible) - decEq Error InvalidParam = No (\case Refl impossible) - decEq Error Busy = No (\case Refl impossible) - decEq InvalidParam Ok = No (\case Refl impossible) - decEq InvalidParam Error = No (\case Refl impossible) - decEq InvalidParam Busy = No (\case Refl impossible) - decEq Busy Ok = No (\case Refl impossible) - decEq Busy Error = No (\case Refl impossible) - decEq Busy InvalidParam = No (\case Refl impossible) +data Verdict = VAccepted | VRejected | VIllFormed -||| Opaque handle for library resources -||| Invariant: Handle pointer must be non-null +||| Wire encoding of a verdict. public export -record Handle where - constructor MkHandle - ptr : Bits64 - 0 prf : So (ptr /= 0) +verdictCode : Verdict -> Bits8 +verdictCode VAccepted = 0 +verdictCode VRejected = 1 +verdictCode VIllFormed = 2 -||| Returns Nothing if pointer is null +||| Decode a discipline byte (total; out-of-range is Nothing). public export -createHandle : Bits64 -> Maybe Handle -createHandle 0 = Nothing -createHandle ptr = case decSo (ptr /= 0) of - Yes p => Just (MkHandle ptr p) - No _ => Nothing - --------------------------------------------------------------------------------- --- C-Types Mapping --------------------------------------------------------------------------------- +disciplineOfCode : Bits8 -> Maybe Discipline +disciplineOfCode 0 = Just DAffine +disciplineOfCode 1 = Just DExact +disciplineOfCode _ = Nothing -||| Tagged types for C-FFI boundary -public export -data CType = CInt | CUInt | CLong | CULong | CPtrType +-- Machine-checked encoding facts ------------------------------------------- -||| Pointer type for platform +||| Discipline codes are injective. public export -CPtr : Platform -> CType -> Type -CPtr p _ = Bits64 -- Simplified for 64-bit template - -||| Size of C types (platform-specific) +disciplineCodeInjective : (d1, d2 : Discipline) -> + disciplineCode d1 = disciplineCode d2 -> d1 = d2 +disciplineCodeInjective DAffine DAffine _ = Refl +disciplineCodeInjective DExact DExact _ = Refl +disciplineCodeInjective DAffine DExact Refl impossible +disciplineCodeInjective DExact DAffine Refl impossible + +||| Verdict codes are injective. public export -cSizeOf : (p : Platform) -> (t : CType) -> Nat -cSizeOf p CInt = 4 -cSizeOf p CUInt = 4 -cSizeOf p CLong = 8 -cSizeOf p CULong = 8 -cSizeOf p CPtrType = 8 - -||| Alignment of C types (platform-specific) +verdictCodeInjective : (v1, v2 : Verdict) -> + verdictCode v1 = verdictCode v2 -> v1 = v2 +verdictCodeInjective VAccepted VAccepted _ = Refl +verdictCodeInjective VRejected VRejected _ = Refl +verdictCodeInjective VIllFormed VIllFormed _ = Refl +verdictCodeInjective VAccepted VRejected Refl impossible +verdictCodeInjective VAccepted VIllFormed Refl impossible +verdictCodeInjective VRejected VAccepted Refl impossible +verdictCodeInjective VRejected VIllFormed Refl impossible +verdictCodeInjective VIllFormed VAccepted Refl impossible +verdictCodeInjective VIllFormed VRejected Refl impossible + +||| Decoding inverts encoding. public export -cAlignOf : (p : Platform) -> (t : CType) -> Nat -cAlignOf p CInt = 4 -cAlignOf p CUInt = 4 -cAlignOf p CLong = 8 -cAlignOf p CULong = 8 -cAlignOf p CPtrType = 8 +disciplineRoundTrip : (d : Discipline) -> + disciplineOfCode (disciplineCode d) = Just d +disciplineRoundTrip DAffine = Refl +disciplineRoundTrip DExact = Refl diff --git a/src/interface/ffi/README.adoc b/src/interface/ffi/README.adoc index ca14320..24df480 100644 --- a/src/interface/ffi/README.adoc +++ b/src/interface/ffi/README.adoc @@ -1,3 +1,28 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell -= ffi Logic += anytype FFI (Zig) + +`libanytype` exports `anytype_check(discipline: u8, term: [*:0]const u8) u8`, +the C symbol declared in `src/interface/Abi/Foreign.idr`. Verdict return +values are `Abi.Types.verdictCode`: 0 accepted, 1 rejected, 2 ill-formed. + +*MVP transport is a spawned process*: the export locates the `anytype-check` +kernel binary (`$ANYTYPE_CHECK_BIN`, else PATH) and speaks the seam protocol +(term on stdin, verdict as exit code). In-process linkage of the Idris2 +kernel (RefC backend) is future work. A missing binary reports ill-formed — +the seam never invents an acceptance. + +Wire structs (`anytype_request_t`, `anytype_response_t`) are comptime-asserted +against the layouts proven `CABICompliant` in `src/interface/Abi/Layout.idr`; +edit a layout on either side and one of the two gates fails. + +Build and test (Zig 0.16, pinned in `.tool-versions`): + +[source,sh] +---- +zig build # static libanytype +zig build test # comptime layout asserts + kernel round-trip tests +---- + +The round-trip tests need `build/exec/anytype-check` at the repo root +(`just test` builds it) and FAIL when it is absent, never skip. diff --git a/src/interface/ffi/build.zig b/src/interface/ffi/build.zig index 2607c11..548d560 100644 --- a/src/interface/ffi/build.zig +++ b/src/interface/ffi/build.zig @@ -1,19 +1,30 @@ // SPDX-License-Identifier: MPL-2.0 // Copyright (c) Jonathan D.A. Jewell // -// Template FFI Build Configuration (Zig 0.15.2+) -// Note: This is a minimal build file that demonstrates Zig integration +// anytype FFI build (Zig 0.16): static libanytype + tests. const std = @import("std"); pub fn build(b: *std.Build) void { - _ = b.standardTargetOptions(.{}); - _ = b.standardOptimizeOption(.{}); + const target = b.standardTargetOptions(.{}); + const optimize = b.standardOptimizeOption(.{}); - // In Zig 0.15+, tests are run directly with: - // zig build-exe -ftest-runner src/main.zig - // zig build-exe -ftest-runner test/integration_test.zig - // - // This minimal build file provides scaffolding for future expansion. - // Tests can be invoked via command line without explicit build.zig configuration. + const mod = b.createModule(.{ + .root_source_file = b.path("src/main.zig"), + .target = target, + .optimize = optimize, + .link_libc = true, // std.c.getenv in the C entry point + }); + + const lib = b.addLibrary(.{ + .name = "anytype", + .root_module = mod, + .linkage = .static, + }); + b.installArtifact(lib); + + const tests = b.addTest(.{ .root_module = mod }); + const run_tests = b.addRunArtifact(tests); + const test_step = b.step("test", "Run seam layout + round-trip tests"); + test_step.dependOn(&run_tests.step); } diff --git a/src/interface/ffi/src/main.zig b/src/interface/ffi/src/main.zig index f1b2633..5733d52 100644 --- a/src/interface/ffi/src/main.zig +++ b/src/interface/ffi/src/main.zig @@ -1,275 +1,140 @@ // SPDX-License-Identifier: MPL-2.0 // Copyright (c) Jonathan D.A. Jewell -// {{PROJECT}} FFI Implementation -// -// This module implements the C-compatible FFI declared in src/abi/Foreign.idr -// All types and layouts must match the Idris2 ABI definitions. +// anytype FFI: the Zig side of the seam. // +// Exports `anytype_check`, the C symbol declared in src/interface/Abi/ +// Foreign.idr. The MVP transport is a spawned `anytype-check` process +// (see README.adoc); in-process linkage of the Idris2 kernel is future +// work. Wire structs are comptime-asserted against the layouts proven +// CABICompliant in src/interface/Abi/Layout.idr — if either side edits +// a layout, one of the two gates fails. const std = @import("std"); -// Version information (keep in sync with project) -const VERSION = "0.1.0"; -const BUILD_INFO = "{{PROJECT}} built with Zig " ++ @import("builtin").zig_version_string; - -/// Thread-local error storage -threadlocal var last_error: ?[]const u8 = null; - -/// Set the last error message -fn setError(msg: []const u8) void { - last_error = msg; -} - -/// Clear the last error -fn clearError() void { - last_error = null; -} - -//============================================================================== -// Core Types (must match src/abi/Types.idr) -//============================================================================== - -/// Result codes (must match Idris2 Result type) -pub const Result = enum(c_int) { - ok = 0, - @"error" = 1, - invalid_param = 2, - out_of_memory = 3, - null_pointer = 4, +/// Verdict codes — must match Abi.Types.verdictCode (proven injective +/// on the Idris side). +pub const VERDICT_ACCEPTED: u8 = 0; +pub const VERDICT_REJECTED: u8 = 1; +pub const VERDICT_ILLFORMED: u8 = 2; + +/// Mirrors Abi.Layout.requestLayout: size 16, align 8, +/// discipline@0, term_len@4, term_utf8@8. +pub const anytype_request_t = extern struct { + discipline: u8, + term_len: u32, + term_utf8: [*:0]const u8, }; -/// Library handle (opaque to prevent direct access) -pub const Handle = opaque { - // Internal state hidden from C - allocator: std.mem.Allocator, - initialized: bool, - // Add your fields here +/// Mirrors Abi.Layout.responseLayout: size 16, align 8, +/// verdict@0, msg_len@4, msg_utf8@8. +pub const anytype_response_t = extern struct { + verdict: u8, + msg_len: u32, + msg_utf8: [*:0]const u8, }; -//============================================================================== -// Library Lifecycle -//============================================================================== - -/// Initialize the library -/// Returns a handle, or null on failure -export fn {{project}}_init() ?*Handle { - const allocator = std.heap.c_allocator; - - const handle = allocator.create(Handle) catch { - setError("Failed to allocate handle"); - return null; - }; - - // Initialize handle - handle.* = .{ - .allocator = allocator, - .initialized = true, - }; - - clearError(); - return handle; -} - -/// Free the library handle -export fn {{project}}_free(handle: ?*Handle) void { - const h = handle orelse return; - const allocator = h.allocator; - - // Clean up resources - h.initialized = false; - - allocator.destroy(h); - clearError(); -} - -//============================================================================== -// Core Operations -//============================================================================== - -/// Process data (example operation) -export fn {{project}}_process(handle: ?*Handle, input: u32) Result { - const h = handle orelse { - setError("Null handle"); - return .null_pointer; +comptime { + // These numbers are the ones proven in Abi.Layout; a drift on either + // side breaks the corresponding gate. + std.debug.assert(@sizeOf(anytype_request_t) == 16); + std.debug.assert(@alignOf(anytype_request_t) == 8); + std.debug.assert(@offsetOf(anytype_request_t, "discipline") == 0); + std.debug.assert(@offsetOf(anytype_request_t, "term_len") == 4); + std.debug.assert(@offsetOf(anytype_request_t, "term_utf8") == 8); + std.debug.assert(@sizeOf(anytype_response_t) == 16); + std.debug.assert(@alignOf(anytype_response_t) == 8); + std.debug.assert(@offsetOf(anytype_response_t, "verdict") == 0); + std.debug.assert(@offsetOf(anytype_response_t, "msg_len") == 4); + std.debug.assert(@offsetOf(anytype_response_t, "msg_utf8") == 8); +} + +fn disciplineName(code: u8) ?[]const u8 { + // Must match Abi.Types.disciplineCode. + return switch (code) { + 0 => "affine", + 1 => "exact", + else => null, }; - - if (!h.initialized) { - setError("Handle not initialized"); - return .@"error"; - } - - // Example processing logic - _ = input; - - clearError(); - return .ok; } -//============================================================================== -// String Operations -//============================================================================== - -/// Get a string result (example) -/// Caller must free the returned string -export fn {{project}}_get_string(handle: ?*Handle) ?[*:0]const u8 { - const h = handle orelse { - setError("Null handle"); - return null; - }; - - if (!h.initialized) { - setError("Handle not initialized"); - return null; +/// Run one kernel check by spawning `bin` and speaking the seam +/// protocol: term on stdin, verdict as exit code (= verdictCode). +pub fn checkWith( + io: std.Io, + bin: []const u8, + discipline: u8, + term: []const u8, +) u8 { + const disc = disciplineName(discipline) orelse return VERDICT_ILLFORMED; + + var child = std.process.spawn(io, .{ + .argv = &.{ bin, "--discipline", disc }, + .stdin = .pipe, + .stdout = .ignore, + .stderr = .ignore, + }) catch return VERDICT_ILLFORMED; + + if (child.stdin) |stdin| { + stdin.writeStreamingAll(io, term) catch {}; + stdin.writeStreamingAll(io, "\n") catch {}; + stdin.close(io); + child.stdin = null; } - - // Example: allocate and return a string - const result = h.allocator.dupeZ(u8, "Example result") catch { - setError("Failed to allocate string"); - return null; - }; - - clearError(); - return result.ptr; -} - -/// Free a string allocated by the library -export fn {{project}}_free_string(str: ?[*:0]const u8) void { - const s = str orelse return; - const allocator = std.heap.c_allocator; - - const slice = std.mem.span(s); - allocator.free(slice); -} - -//============================================================================== -// Array/Buffer Operations -//============================================================================== - -/// Process an array of data -export fn {{project}}_process_array( - handle: ?*Handle, - buffer: ?[*]const u8, - len: u32, -) Result { - const h = handle orelse { - setError("Null handle"); - return .null_pointer; - }; - - const buf = buffer orelse { - setError("Null buffer"); - return .null_pointer; + const result = child.wait(io) catch return VERDICT_ILLFORMED; + return switch (result) { + .exited => |code| switch (code) { + VERDICT_ACCEPTED, VERDICT_REJECTED, VERDICT_ILLFORMED => code, + else => VERDICT_ILLFORMED, + }, + else => VERDICT_ILLFORMED, }; - - if (!h.initialized) { - setError("Handle not initialized"); - return .@"error"; - } - - // Access the buffer - const data = buf[0..len]; - _ = data; - - // Process data here - - clearError(); - return .ok; -} - -//============================================================================== -// Error Handling -//============================================================================== - -/// Get the last error message -/// Returns null if no error -export fn {{project}}_last_error() ?[*:0]const u8 { - const err = last_error orelse return null; - - // Return C string (static storage, no need to free) - const allocator = std.heap.c_allocator; - const c_str = allocator.dupeZ(u8, err) catch return null; - return c_str.ptr; } -//============================================================================== -// Version Information -//============================================================================== - -/// Get the library version -export fn {{project}}_version() [*:0]const u8 { - return VERSION.ptr; -} - -/// Get build information -export fn {{project}}_build_info() [*:0]const u8 { - return BUILD_INFO.ptr; +/// C entry point. The kernel binary is found via $ANYTYPE_CHECK_BIN, +/// falling back to `anytype-check` on PATH. A missing binary reports +/// VERDICT_ILLFORMED — the seam never invents an acceptance. +export fn anytype_check(discipline: u8, term: [*:0]const u8) u8 { + var threaded: std.Io.Threaded = .init(std.heap.page_allocator, .{}); + defer threaded.deinit(); + const bin: []const u8 = if (std.c.getenv("ANYTYPE_CHECK_BIN")) |v| + std.mem.span(@as([*:0]const u8, v)) + else + "anytype-check"; + return checkWith(threaded.io(), bin, discipline, std.mem.span(term)); } -//============================================================================== -// Callback Support -//============================================================================== - -/// Callback function type (C ABI) -pub const Callback = *const fn (u64, u32) callconv(.C) u32; - -/// Register a callback -export fn {{project}}_register_callback( - handle: ?*Handle, - callback: ?Callback, -) Result { - const h = handle orelse { - setError("Null handle"); - return .null_pointer; - }; - - const cb = callback orelse { - setError("Null callback"); - return .null_pointer; - }; - - if (!h.initialized) { - setError("Handle not initialized"); - return .@"error"; - } - - // Store callback for later use - _ = cb; - - clearError(); - return .ok; -} +// --------------------------------------------------------------------------- +// Tests (zig build test). The round-trip tests need the kernel binary at +// ../../../build/exec/anytype-check (built by `just test`); they fail if +// it is absent, because a seam test that cannot run must not pass. +// --------------------------------------------------------------------------- -//============================================================================== -// Utility Functions -//============================================================================== +const KERNEL_BIN = "../../../build/exec/anytype-check"; -/// Check if handle is initialized -export fn {{project}}_is_initialized(handle: ?*Handle) u32 { - const h = handle orelse return 0; - return if (h.initialized) 1 else 0; +test "unknown discipline is ill-formed without spawning" { + try std.testing.expectEqual( + VERDICT_ILLFORMED, + checkWith(std.testing.io, KERNEL_BIN, 9, "tt"), + ); } -//============================================================================== -// Tests -//============================================================================== - -test "lifecycle" { - const handle = {{project}}_init() orelse return error.InitFailed; - defer {{project}}_free(handle); - - try std.testing.expect({{project}}_is_initialized(handle) == 1); +test "round trip: affine accepts drop" { + try std.testing.expectEqual( + VERDICT_ACCEPTED, + checkWith(std.testing.io, KERNEL_BIN, 0, "(lam 1 bool tt)"), + ); } -test "error handling" { - const result = {{project}}_process(null, 0); - try std.testing.expectEqual(Result.null_pointer, result); - - const err = {{project}}_last_error(); - try std.testing.expect(err != null); +test "round trip: exact rejects drop (the discipline split)" { + try std.testing.expectEqual( + VERDICT_REJECTED, + checkWith(std.testing.io, KERNEL_BIN, 1, "(lam 1 bool tt)"), + ); } -test "version" { - const ver = {{project}}_version(); - const ver_str = std.mem.span(ver); - try std.testing.expectEqualStrings(VERSION, ver_str); +test "round trip: ill-formed input" { + try std.testing.expectEqual( + VERDICT_ILLFORMED, + checkWith(std.testing.io, KERNEL_BIN, 0, "garbage(("), + ); } diff --git a/src/kernel/Anytype/Core/Check.idr b/src/kernel/Anytype/Core/Check.idr new file mode 100644 index 0000000..41a3980 --- /dev/null +++ b/src/kernel/Anytype/Core/Check.idr @@ -0,0 +1,97 @@ +||| anytype L1+L2: the usage-counting bidirectional checker. +||| +||| Output-usage formulation (Atkey/QTT style): `infer` returns the type +||| together with a usage vector saying how heavily each free variable +||| was used. Grade accounting: +||| Var i — usage gone at i, gzero elsewhere +||| App f x — Uf `gadd` (q `gmul` Ux), scaling through the arrow +||| Lam q A b — admit iff computed usage of the binder `gleq` q +||| That single inequality is what makes the discipline pluggable: +||| under the affine order dropping a grade-1 binder passes (0 <= 1), +||| under the exact order it fails (0 /= 1). Same rule, distinct +||| disciplines. +||| +||| Conversion is invoked at exactly one place: the check/infer mode +||| switch in `check`. +module Anytype.Core.Check + +import Data.Fin +import Data.Vect +import Anytype.Grade.Algebra +import Anytype.Core.Syntax +import Anytype.Core.Conversion + +%default total + +||| Typing context: declared types of the free variables (grades live +||| on binders; usage is computed, not declared, for the context). +public export +Ctx : Type -> Nat -> Type +Ctx g n = Vect n (Ty g) + +||| Computed usage: one grade per free variable. +public export +Usage : Type -> Nat -> Type +Usage g n = Vect n g + +zeroU : GradeAlgebra g -> (n : Nat) -> Usage g n +zeroU alg n = replicate n alg.gzero + +oneAt : GradeAlgebra g -> {n : Nat} -> Fin n -> Usage g n +oneAt alg FZ = alg.gone :: zeroU alg _ +oneAt alg (FS i) = alg.gzero :: oneAt alg i + +addU : GradeAlgebra g -> Usage g n -> Usage g n -> Usage g n +addU alg = zipWith alg.gadd + +scaleU : GradeAlgebra g -> g -> Usage g n -> Usage g n +scaleU alg q = map (alg.gmul q) + +mutual + ||| Synthesise a type and a usage vector. + public export + infer : GradeAlgebra g -> {n : Nat} -> Ctx g n -> Term g n -> + Either CheckError (Ty g, Usage g n) + infer alg ctx (Var i) = Right (index i ctx, oneAt alg i) + infer alg ctx (Lam q a body) = do + (tb, u) <- infer alg (a :: ctx) body + let (u0 :: rest) = u + if alg.gleq u0 q + then Right (TArr q a tb, rest) + else Left UsageViolation + infer alg ctx (App f x) = do + (tf, uf) <- infer alg ctx f + case tf of + TArr q a b => do + ux <- check alg ctx x a + Right (b, addU alg uf (scaleU alg q ux)) + _ => Left NotAFunction + infer alg ctx (Pair s t) = do + (ts, us) <- infer alg ctx s + (tt, ut) <- infer alg ctx t + Right (TProd ts tt, addU alg us ut) + infer alg ctx (LetPair p body) = do + (tp, up) <- infer alg ctx p + case tp of + TProd a b => do + -- components bound at grade gone: FS FZ = first, FZ = second + (tr, u) <- infer alg (b :: a :: ctx) body + let (u1 :: u0 :: rest) = u + if alg.gleq u0 alg.gone && alg.gleq u1 alg.gone + then Right (tr, addU alg up rest) + else Left UsageViolation + _ => Left NotAPair + infer alg ctx TT = Right (TUnit, zeroU alg n) + infer alg ctx (BLit _) = Right (TBool, zeroU alg n) + infer alg ctx (WordLit w) = Right (TBits w, zeroU alg n) + + ||| Check against an expected type: infer, then normalise-and-compare. + ||| This is the single conversion site. + public export + check : GradeAlgebra g -> {n : Nat} -> Ctx g n -> Term g n -> Ty g -> + Either CheckError (Usage g n) + check alg ctx t ty = do + (ty', u) <- infer alg ctx t + if convertible alg ty' ty + then Right u + else Left TypeMismatch diff --git a/src/kernel/Anytype/Core/Conversion.idr b/src/kernel/Anytype/Core/Conversion.idr new file mode 100644 index 0000000..3444011 --- /dev/null +++ b/src/kernel/Anytype/Core/Conversion.idr @@ -0,0 +1,35 @@ +||| anytype L1: conversion is normalise-and-compare — one primitive +||| relation (equality of normal forms), no coercion machinery. Grades +||| on arrows are compared with the algebra's decidable equality; there +||| is no grade subtyping in conversion. +module Anytype.Core.Conversion + +import Anytype.Grade.Algebra +import Anytype.Core.Syntax +import Anytype.Core.Normalise + +%default total + +||| Structural equality of canonical type-level naturals. +tnatEq : TNat -> TNat -> Bool +tnatEq NZ NZ = True +tnatEq (NS a) (NS b) = tnatEq a b +tnatEq _ _ = False + +||| Structural equality of normalised types. +structEq : GradeAlgebra g -> Ty g -> Ty g -> Bool +structEq _ TUnit TUnit = True +structEq _ TBool TBool = True +structEq _ (TBits v) (TBits w) = tnatEq v w +structEq alg (TArr q a b) (TArr q' a' b') = + case alg.gdec q q' of + Yes _ => structEq alg a a' && structEq alg b b' + No _ => False +structEq alg (TProd a b) (TProd a' b') = + structEq alg a a' && structEq alg b b' +structEq _ _ _ = False + +||| Are two types equal up to type-level computation? +public export +convertible : GradeAlgebra g -> Ty g -> Ty g -> Bool +convertible alg s t = structEq alg (normalise s) (normalise t) diff --git a/src/kernel/Anytype/Core/Normalise.idr b/src/kernel/Anytype/Core/Normalise.idr new file mode 100644 index 0000000..8a17ea5 --- /dev/null +++ b/src/kernel/Anytype/Core/Normalise.idr @@ -0,0 +1,41 @@ +||| anytype L1: normalisation of type-level computation. +||| +||| `TNat` has no recursion constructor, so evaluation is structural and +||| this whole module is `%default total` with no escape hatches — this +||| machine-checked totality IS the MVP totality gate: conversion below +||| is decidable because everything here terminates by construction. +module Anytype.Core.Normalise + +import Anytype.Core.Syntax + +%default total + +||| Evaluate a type-level natural. +public export +nval : TNat -> Nat +nval NZ = 0 +nval (NS t) = S (nval t) +nval (NPlus a b) = nval a + nval b +nval (NMul a b) = nval a * nval b + +||| Canonical (NZ/NS-only) form of a Nat. +public export +tnatOfNat : Nat -> TNat +tnatOfNat Z = NZ +tnatOfNat (S k) = NS (tnatOfNat k) + +||| Canonical form of a type-level natural: normalise-and-compare's +||| "normalise" half at the index level. +public export +nnorm : TNat -> TNat +nnorm = tnatOfNat . nval + +||| Normalise a type: canonicalise every `TBits` index, recurse +||| structurally everywhere else. +public export +normalise : Ty g -> Ty g +normalise TUnit = TUnit +normalise TBool = TBool +normalise (TBits w) = TBits (nnorm w) +normalise (TArr q a b) = TArr q (normalise a) (normalise b) +normalise (TProd a b) = TProd (normalise a) (normalise b) diff --git a/src/kernel/Anytype/Core/Syntax.idr b/src/kernel/Anytype/Core/Syntax.idr new file mode 100644 index 0000000..2a5b624 --- /dev/null +++ b/src/kernel/Anytype/Core/Syntax.idr @@ -0,0 +1,71 @@ +||| anytype L1: syntax of the MVP core — a bidirectional simply-graded +||| lambda calculus. +||| +||| The type-index language `TNat` deliberately has NO fixpoint or +||| recursion constructor: type-level computation is total *by +||| construction*, which is the MVP discharge of systemet's L1 totality +||| gate (a syntactic gate, not a termination analysis — see EXPLAINME). +||| +||| Terms are intrinsically scoped (de Bruijn via `Fin`), parameterised +||| by the grade carrier `g` because binders and arrows carry grades. +module Anytype.Core.Syntax + +import Data.Fin + +%default total + +||| Total type-level naturals: the index language for `TBits`. +public export +data TNat : Type where + NZ : TNat + NS : TNat -> TNat + NPlus : TNat -> TNat -> TNat + NMul : TNat -> TNat -> TNat + +||| Types, parameterised by the grade carrier. +public export +data Ty : Type -> Type where + TUnit : Ty g + TBool : Ty g + ||| An indexed family so conversion has real work to do: + ||| `TBits (NPlus 2 3)` and `TBits 5` are convertible, not equal. + TBits : TNat -> Ty g + ||| Graded function arrow q : A -> B. + TArr : g -> Ty g -> Ty g -> Ty g + ||| Multiplicative pair. + TProd : Ty g -> Ty g -> Ty g + +||| Intrinsically scoped terms. No `if`: branching needs a join on +||| grades beyond systemet's stated semiring+order laws (post-MVP). +public export +data Term : Type -> Nat -> Type where + Var : Fin n -> Term g n + ||| Binder carries its declared grade and domain type. + Lam : g -> Ty g -> Term g (S n) -> Term g n + App : Term g n -> Term g n -> Term g n + Pair : Term g n -> Term g n -> Term g n + ||| Pattern-match consumption of a pair. The body sees the components + ||| at de Bruijn indices FS FZ (first) and FZ (second), each bound at + ||| grade `gone` (multiplicative elimination). + LetPair : Term g n -> Term g (S (S n)) -> Term g n + TT : Term g n + BLit : Bool -> Term g n + ||| Type-indexed word literal: `WordLit w : TBits w`, usage zero. + ||| Exists so closed terms can exercise conversion at `TBits`. + WordLit : TNat -> Term g n + +||| Why the checker rejected a term. +public export +data CheckError : Type where + NotAFunction : CheckError + NotAPair : CheckError + TypeMismatch : CheckError + ||| Computed usage of a binder exceeds its declared grade. + UsageViolation : CheckError + +public export +Show CheckError where + show NotAFunction = "not a function" + show NotAPair = "not a pair" + show TypeMismatch = "type mismatch" + show UsageViolation = "usage violation" diff --git a/src/kernel/Anytype/Grade/Affine.idr b/src/kernel/Anytype/Grade/Affine.idr new file mode 100644 index 0000000..fc7b8a0 --- /dev/null +++ b/src/kernel/Anytype/Grade/Affine.idr @@ -0,0 +1,465 @@ +||| The affine+erasure grade algebra {0, 1, omega} — AffineScript's +||| discipline, mirrored cell-for-cell from affinescript/lib/quantity.ml +||| (q_add / q_mul / q_le): addition saturates (1+1 = omega), omega +||| absorbs, multiplication scales usage through application (the +||| omega*1 = omega rule, AffineScript's BUG-001 fix). `QVar` from the +||| AffineScript elaborator is unification machinery, not part of the +||| algebra, and is deliberately absent here. +||| +||| Law proofs are exhaustive constructor enumerations; the coverage +||| checker forces completeness and `%default total` forbids escape +||| hatches. +module Anytype.Grade.Affine + +import Data.So +import Anytype.Grade.Algebra + +%default total + +public export +data Q = Q0 | Q1 | QW + +public export +Show Q where + show Q0 = "0" + show Q1 = "1" + show QW = "w" + +||| quantity.ml q_add: 0 identity; 1+1 saturates to omega; omega absorbs. +public export +qadd : Q -> Q -> Q +qadd Q0 Q0 = Q0 +qadd Q0 Q1 = Q1 +qadd Q0 QW = QW +qadd Q1 Q0 = Q1 +qadd Q1 Q1 = QW +qadd Q1 QW = QW +qadd QW Q0 = QW +qadd QW Q1 = QW +qadd QW QW = QW + +||| quantity.ml q_mul: 0 annihilates; 1 identity; omega*omega = omega. +public export +qmul : Q -> Q -> Q +qmul Q0 Q0 = Q0 +qmul Q0 Q1 = Q0 +qmul Q0 QW = Q0 +qmul Q1 Q0 = Q0 +qmul Q1 Q1 = Q1 +qmul Q1 QW = QW +qmul QW Q0 = Q0 +qmul QW Q1 = QW +qmul QW QW = QW + +||| quantity.ml q_le: the total order 0 <= 1 <= omega. +public export +qleq : Q -> Q -> Bool +qleq Q0 Q0 = True +qleq Q0 Q1 = True +qleq Q0 QW = True +qleq Q1 Q0 = False +qleq Q1 Q1 = True +qleq Q1 QW = True +qleq QW Q0 = False +qleq QW Q1 = False +qleq QW QW = True + +q0NotQ1 : Q0 = Q1 -> Void +q0NotQ1 Refl impossible + +q0NotQW : Q0 = QW -> Void +q0NotQW Refl impossible + +q1NotQW : Q1 = QW -> Void +q1NotQW Refl impossible + +public export +qdec : (a, b : Q) -> Dec (a = b) +qdec Q0 Q0 = Yes Refl +qdec Q0 Q1 = No q0NotQ1 +qdec Q0 QW = No q0NotQW +qdec Q1 Q0 = No (\p => q0NotQ1 (sym p)) +qdec Q1 Q1 = Yes Refl +qdec Q1 QW = No q1NotQW +qdec QW Q0 = No (\p => q0NotQW (sym p)) +qdec QW Q1 = No (\p => q1NotQW (sym p)) +qdec QW QW = Yes Refl + +-- Exhaustive law proofs (generated; verified by the typechecker). + +qaddAssoc : (a, b, c : Q) -> qadd a (qadd b c) = qadd (qadd a b) c +qmulAssoc : (a, b, c : Q) -> qmul a (qmul b c) = qmul (qmul a b) c +qdistribL : (a, b, c : Q) -> qmul a (qadd b c) = qadd (qmul a b) (qmul a c) +qdistribR : (a, b, c : Q) -> qmul (qadd a b) c = qadd (qmul a c) (qmul b c) +qaddComm : (a, b : Q) -> qadd a b = qadd b a +qaddZeroL : (a : Q) -> qadd Q0 a = a +qmulOneL : (a : Q) -> qmul Q1 a = a +qmulOneR : (a : Q) -> qmul a Q1 = a +qmulZeroL : (a : Q) -> qmul Q0 a = Q0 +qmulZeroR : (a : Q) -> qmul a Q0 = Q0 +qleqRefl : (a : Q) -> So (qleq a a) +qleqTrans : (a, b, c : Q) -> So (qleq a b) -> So (qleq b c) -> So (qleq a c) +qleqAntisym : (a, b : Q) -> So (qleq a b) -> So (qleq b a) -> a = b +qaddMono : (a, b, c, d : Q) -> + So (qleq a b) -> So (qleq c d) -> So (qleq (qadd a c) (qadd b d)) +qmulMono : (a, b, c, d : Q) -> + So (qleq a b) -> So (qleq c d) -> So (qleq (qmul a c) (qmul b d)) + +qaddAssoc Q0 Q0 Q0 = Refl +qaddAssoc Q0 Q0 Q1 = Refl +qaddAssoc Q0 Q0 QW = Refl +qaddAssoc Q0 Q1 Q0 = Refl +qaddAssoc Q0 Q1 Q1 = Refl +qaddAssoc Q0 Q1 QW = Refl +qaddAssoc Q0 QW Q0 = Refl +qaddAssoc Q0 QW Q1 = Refl +qaddAssoc Q0 QW QW = Refl +qaddAssoc Q1 Q0 Q0 = Refl +qaddAssoc Q1 Q0 Q1 = Refl +qaddAssoc Q1 Q0 QW = Refl +qaddAssoc Q1 Q1 Q0 = Refl +qaddAssoc Q1 Q1 Q1 = Refl +qaddAssoc Q1 Q1 QW = Refl +qaddAssoc Q1 QW Q0 = Refl +qaddAssoc Q1 QW Q1 = Refl +qaddAssoc Q1 QW QW = Refl +qaddAssoc QW Q0 Q0 = Refl +qaddAssoc QW Q0 Q1 = Refl +qaddAssoc QW Q0 QW = Refl +qaddAssoc QW Q1 Q0 = Refl +qaddAssoc QW Q1 Q1 = Refl +qaddAssoc QW Q1 QW = Refl +qaddAssoc QW QW Q0 = Refl +qaddAssoc QW QW Q1 = Refl +qaddAssoc QW QW QW = Refl + +qmulAssoc Q0 Q0 Q0 = Refl +qmulAssoc Q0 Q0 Q1 = Refl +qmulAssoc Q0 Q0 QW = Refl +qmulAssoc Q0 Q1 Q0 = Refl +qmulAssoc Q0 Q1 Q1 = Refl +qmulAssoc Q0 Q1 QW = Refl +qmulAssoc Q0 QW Q0 = Refl +qmulAssoc Q0 QW Q1 = Refl +qmulAssoc Q0 QW QW = Refl +qmulAssoc Q1 Q0 Q0 = Refl +qmulAssoc Q1 Q0 Q1 = Refl +qmulAssoc Q1 Q0 QW = Refl +qmulAssoc Q1 Q1 Q0 = Refl +qmulAssoc Q1 Q1 Q1 = Refl +qmulAssoc Q1 Q1 QW = Refl +qmulAssoc Q1 QW Q0 = Refl +qmulAssoc Q1 QW Q1 = Refl +qmulAssoc Q1 QW QW = Refl +qmulAssoc QW Q0 Q0 = Refl +qmulAssoc QW Q0 Q1 = Refl +qmulAssoc QW Q0 QW = Refl +qmulAssoc QW Q1 Q0 = Refl +qmulAssoc QW Q1 Q1 = Refl +qmulAssoc QW Q1 QW = Refl +qmulAssoc QW QW Q0 = Refl +qmulAssoc QW QW Q1 = Refl +qmulAssoc QW QW QW = Refl + +qdistribL Q0 Q0 Q0 = Refl +qdistribL Q0 Q0 Q1 = Refl +qdistribL Q0 Q0 QW = Refl +qdistribL Q0 Q1 Q0 = Refl +qdistribL Q0 Q1 Q1 = Refl +qdistribL Q0 Q1 QW = Refl +qdistribL Q0 QW Q0 = Refl +qdistribL Q0 QW Q1 = Refl +qdistribL Q0 QW QW = Refl +qdistribL Q1 Q0 Q0 = Refl +qdistribL Q1 Q0 Q1 = Refl +qdistribL Q1 Q0 QW = Refl +qdistribL Q1 Q1 Q0 = Refl +qdistribL Q1 Q1 Q1 = Refl +qdistribL Q1 Q1 QW = Refl +qdistribL Q1 QW Q0 = Refl +qdistribL Q1 QW Q1 = Refl +qdistribL Q1 QW QW = Refl +qdistribL QW Q0 Q0 = Refl +qdistribL QW Q0 Q1 = Refl +qdistribL QW Q0 QW = Refl +qdistribL QW Q1 Q0 = Refl +qdistribL QW Q1 Q1 = Refl +qdistribL QW Q1 QW = Refl +qdistribL QW QW Q0 = Refl +qdistribL QW QW Q1 = Refl +qdistribL QW QW QW = Refl + +qdistribR Q0 Q0 Q0 = Refl +qdistribR Q0 Q0 Q1 = Refl +qdistribR Q0 Q0 QW = Refl +qdistribR Q0 Q1 Q0 = Refl +qdistribR Q0 Q1 Q1 = Refl +qdistribR Q0 Q1 QW = Refl +qdistribR Q0 QW Q0 = Refl +qdistribR Q0 QW Q1 = Refl +qdistribR Q0 QW QW = Refl +qdistribR Q1 Q0 Q0 = Refl +qdistribR Q1 Q0 Q1 = Refl +qdistribR Q1 Q0 QW = Refl +qdistribR Q1 Q1 Q0 = Refl +qdistribR Q1 Q1 Q1 = Refl +qdistribR Q1 Q1 QW = Refl +qdistribR Q1 QW Q0 = Refl +qdistribR Q1 QW Q1 = Refl +qdistribR Q1 QW QW = Refl +qdistribR QW Q0 Q0 = Refl +qdistribR QW Q0 Q1 = Refl +qdistribR QW Q0 QW = Refl +qdistribR QW Q1 Q0 = Refl +qdistribR QW Q1 Q1 = Refl +qdistribR QW Q1 QW = Refl +qdistribR QW QW Q0 = Refl +qdistribR QW QW Q1 = Refl +qdistribR QW QW QW = Refl + +qaddComm Q0 Q0 = Refl +qaddComm Q0 Q1 = Refl +qaddComm Q0 QW = Refl +qaddComm Q1 Q0 = Refl +qaddComm Q1 Q1 = Refl +qaddComm Q1 QW = Refl +qaddComm QW Q0 = Refl +qaddComm QW Q1 = Refl +qaddComm QW QW = Refl + +qaddZeroL Q0 = Refl +qaddZeroL Q1 = Refl +qaddZeroL QW = Refl + +qmulOneL Q0 = Refl +qmulOneL Q1 = Refl +qmulOneL QW = Refl + +qmulOneR Q0 = Refl +qmulOneR Q1 = Refl +qmulOneR QW = Refl + +qmulZeroL Q0 = Refl +qmulZeroL Q1 = Refl +qmulZeroL QW = Refl + +qmulZeroR Q0 = Refl +qmulZeroR Q1 = Refl +qmulZeroR QW = Refl + +qleqRefl Q0 = Oh +qleqRefl Q1 = Oh +qleqRefl QW = Oh + +qleqTrans Q0 Q0 Q0 _ _ = Oh +qleqTrans Q0 Q0 Q1 _ _ = Oh +qleqTrans Q0 Q0 QW _ _ = Oh +qleqTrans Q0 Q1 Q0 _ y = absurd y +qleqTrans Q0 Q1 Q1 _ _ = Oh +qleqTrans Q0 Q1 QW _ _ = Oh +qleqTrans Q0 QW Q0 _ y = absurd y +qleqTrans Q0 QW Q1 _ y = absurd y +qleqTrans Q0 QW QW _ _ = Oh +qleqTrans Q1 Q0 Q0 x _ = absurd x +qleqTrans Q1 Q0 Q1 x _ = absurd x +qleqTrans Q1 Q0 QW x _ = absurd x +qleqTrans Q1 Q1 Q0 _ y = absurd y +qleqTrans Q1 Q1 Q1 _ _ = Oh +qleqTrans Q1 Q1 QW _ _ = Oh +qleqTrans Q1 QW Q0 _ y = absurd y +qleqTrans Q1 QW Q1 _ y = absurd y +qleqTrans Q1 QW QW _ _ = Oh +qleqTrans QW Q0 Q0 x _ = absurd x +qleqTrans QW Q0 Q1 x _ = absurd x +qleqTrans QW Q0 QW x _ = absurd x +qleqTrans QW Q1 Q0 x _ = absurd x +qleqTrans QW Q1 Q1 x _ = absurd x +qleqTrans QW Q1 QW x _ = absurd x +qleqTrans QW QW Q0 _ y = absurd y +qleqTrans QW QW Q1 _ y = absurd y +qleqTrans QW QW QW _ _ = Oh + +qleqAntisym Q0 Q0 _ _ = Refl +qleqAntisym Q0 Q1 _ y = absurd y +qleqAntisym Q0 QW _ y = absurd y +qleqAntisym Q1 Q0 x _ = absurd x +qleqAntisym Q1 Q1 _ _ = Refl +qleqAntisym Q1 QW _ y = absurd y +qleqAntisym QW Q0 x _ = absurd x +qleqAntisym QW Q1 x _ = absurd x +qleqAntisym QW QW _ _ = Refl + +qaddMono Q0 Q0 Q0 Q0 _ _ = Oh +qaddMono Q0 Q0 Q0 Q1 _ _ = Oh +qaddMono Q0 Q0 Q0 QW _ _ = Oh +qaddMono Q0 Q0 Q1 Q0 _ y = absurd y +qaddMono Q0 Q0 Q1 Q1 _ _ = Oh +qaddMono Q0 Q0 Q1 QW _ _ = Oh +qaddMono Q0 Q0 QW Q0 _ y = absurd y +qaddMono Q0 Q0 QW Q1 _ y = absurd y +qaddMono Q0 Q0 QW QW _ _ = Oh +qaddMono Q0 Q1 Q0 Q0 _ _ = Oh +qaddMono Q0 Q1 Q0 Q1 _ _ = Oh +qaddMono Q0 Q1 Q0 QW _ _ = Oh +qaddMono Q0 Q1 Q1 Q0 _ y = absurd y +qaddMono Q0 Q1 Q1 Q1 _ _ = Oh +qaddMono Q0 Q1 Q1 QW _ _ = Oh +qaddMono Q0 Q1 QW Q0 _ y = absurd y +qaddMono Q0 Q1 QW Q1 _ y = absurd y +qaddMono Q0 Q1 QW QW _ _ = Oh +qaddMono Q0 QW Q0 Q0 _ _ = Oh +qaddMono Q0 QW Q0 Q1 _ _ = Oh +qaddMono Q0 QW Q0 QW _ _ = Oh +qaddMono Q0 QW Q1 Q0 _ y = absurd y +qaddMono Q0 QW Q1 Q1 _ _ = Oh +qaddMono Q0 QW Q1 QW _ _ = Oh +qaddMono Q0 QW QW Q0 _ y = absurd y +qaddMono Q0 QW QW Q1 _ y = absurd y +qaddMono Q0 QW QW QW _ _ = Oh +qaddMono Q1 Q0 Q0 Q0 x _ = absurd x +qaddMono Q1 Q0 Q0 Q1 x _ = absurd x +qaddMono Q1 Q0 Q0 QW x _ = absurd x +qaddMono Q1 Q0 Q1 Q0 x _ = absurd x +qaddMono Q1 Q0 Q1 Q1 x _ = absurd x +qaddMono Q1 Q0 Q1 QW x _ = absurd x +qaddMono Q1 Q0 QW Q0 x _ = absurd x +qaddMono Q1 Q0 QW Q1 x _ = absurd x +qaddMono Q1 Q0 QW QW x _ = absurd x +qaddMono Q1 Q1 Q0 Q0 _ _ = Oh +qaddMono Q1 Q1 Q0 Q1 _ _ = Oh +qaddMono Q1 Q1 Q0 QW _ _ = Oh +qaddMono Q1 Q1 Q1 Q0 _ y = absurd y +qaddMono Q1 Q1 Q1 Q1 _ _ = Oh +qaddMono Q1 Q1 Q1 QW _ _ = Oh +qaddMono Q1 Q1 QW Q0 _ y = absurd y +qaddMono Q1 Q1 QW Q1 _ y = absurd y +qaddMono Q1 Q1 QW QW _ _ = Oh +qaddMono Q1 QW Q0 Q0 _ _ = Oh +qaddMono Q1 QW Q0 Q1 _ _ = Oh +qaddMono Q1 QW Q0 QW _ _ = Oh +qaddMono Q1 QW Q1 Q0 _ y = absurd y +qaddMono Q1 QW Q1 Q1 _ _ = Oh +qaddMono Q1 QW Q1 QW _ _ = Oh +qaddMono Q1 QW QW Q0 _ y = absurd y +qaddMono Q1 QW QW Q1 _ y = absurd y +qaddMono Q1 QW QW QW _ _ = Oh +qaddMono QW Q0 Q0 Q0 x _ = absurd x +qaddMono QW Q0 Q0 Q1 x _ = absurd x +qaddMono QW Q0 Q0 QW x _ = absurd x +qaddMono QW Q0 Q1 Q0 x _ = absurd x +qaddMono QW Q0 Q1 Q1 x _ = absurd x +qaddMono QW Q0 Q1 QW x _ = absurd x +qaddMono QW Q0 QW Q0 x _ = absurd x +qaddMono QW Q0 QW Q1 x _ = absurd x +qaddMono QW Q0 QW QW x _ = absurd x +qaddMono QW Q1 Q0 Q0 x _ = absurd x +qaddMono QW Q1 Q0 Q1 x _ = absurd x +qaddMono QW Q1 Q0 QW x _ = absurd x +qaddMono QW Q1 Q1 Q0 x _ = absurd x +qaddMono QW Q1 Q1 Q1 x _ = absurd x +qaddMono QW Q1 Q1 QW x _ = absurd x +qaddMono QW Q1 QW Q0 x _ = absurd x +qaddMono QW Q1 QW Q1 x _ = absurd x +qaddMono QW Q1 QW QW x _ = absurd x +qaddMono QW QW Q0 Q0 _ _ = Oh +qaddMono QW QW Q0 Q1 _ _ = Oh +qaddMono QW QW Q0 QW _ _ = Oh +qaddMono QW QW Q1 Q0 _ y = absurd y +qaddMono QW QW Q1 Q1 _ _ = Oh +qaddMono QW QW Q1 QW _ _ = Oh +qaddMono QW QW QW Q0 _ y = absurd y +qaddMono QW QW QW Q1 _ y = absurd y +qaddMono QW QW QW QW _ _ = Oh + +qmulMono Q0 Q0 Q0 Q0 _ _ = Oh +qmulMono Q0 Q0 Q0 Q1 _ _ = Oh +qmulMono Q0 Q0 Q0 QW _ _ = Oh +qmulMono Q0 Q0 Q1 Q0 _ y = absurd y +qmulMono Q0 Q0 Q1 Q1 _ _ = Oh +qmulMono Q0 Q0 Q1 QW _ _ = Oh +qmulMono Q0 Q0 QW Q0 _ y = absurd y +qmulMono Q0 Q0 QW Q1 _ y = absurd y +qmulMono Q0 Q0 QW QW _ _ = Oh +qmulMono Q0 Q1 Q0 Q0 _ _ = Oh +qmulMono Q0 Q1 Q0 Q1 _ _ = Oh +qmulMono Q0 Q1 Q0 QW _ _ = Oh +qmulMono Q0 Q1 Q1 Q0 _ y = absurd y +qmulMono Q0 Q1 Q1 Q1 _ _ = Oh +qmulMono Q0 Q1 Q1 QW _ _ = Oh +qmulMono Q0 Q1 QW Q0 _ y = absurd y +qmulMono Q0 Q1 QW Q1 _ y = absurd y +qmulMono Q0 Q1 QW QW _ _ = Oh +qmulMono Q0 QW Q0 Q0 _ _ = Oh +qmulMono Q0 QW Q0 Q1 _ _ = Oh +qmulMono Q0 QW Q0 QW _ _ = Oh +qmulMono Q0 QW Q1 Q0 _ y = absurd y +qmulMono Q0 QW Q1 Q1 _ _ = Oh +qmulMono Q0 QW Q1 QW _ _ = Oh +qmulMono Q0 QW QW Q0 _ y = absurd y +qmulMono Q0 QW QW Q1 _ y = absurd y +qmulMono Q0 QW QW QW _ _ = Oh +qmulMono Q1 Q0 Q0 Q0 x _ = absurd x +qmulMono Q1 Q0 Q0 Q1 x _ = absurd x +qmulMono Q1 Q0 Q0 QW x _ = absurd x +qmulMono Q1 Q0 Q1 Q0 x _ = absurd x +qmulMono Q1 Q0 Q1 Q1 x _ = absurd x +qmulMono Q1 Q0 Q1 QW x _ = absurd x +qmulMono Q1 Q0 QW Q0 x _ = absurd x +qmulMono Q1 Q0 QW Q1 x _ = absurd x +qmulMono Q1 Q0 QW QW x _ = absurd x +qmulMono Q1 Q1 Q0 Q0 _ _ = Oh +qmulMono Q1 Q1 Q0 Q1 _ _ = Oh +qmulMono Q1 Q1 Q0 QW _ _ = Oh +qmulMono Q1 Q1 Q1 Q0 _ y = absurd y +qmulMono Q1 Q1 Q1 Q1 _ _ = Oh +qmulMono Q1 Q1 Q1 QW _ _ = Oh +qmulMono Q1 Q1 QW Q0 _ y = absurd y +qmulMono Q1 Q1 QW Q1 _ y = absurd y +qmulMono Q1 Q1 QW QW _ _ = Oh +qmulMono Q1 QW Q0 Q0 _ _ = Oh +qmulMono Q1 QW Q0 Q1 _ _ = Oh +qmulMono Q1 QW Q0 QW _ _ = Oh +qmulMono Q1 QW Q1 Q0 _ y = absurd y +qmulMono Q1 QW Q1 Q1 _ _ = Oh +qmulMono Q1 QW Q1 QW _ _ = Oh +qmulMono Q1 QW QW Q0 _ y = absurd y +qmulMono Q1 QW QW Q1 _ y = absurd y +qmulMono Q1 QW QW QW _ _ = Oh +qmulMono QW Q0 Q0 Q0 x _ = absurd x +qmulMono QW Q0 Q0 Q1 x _ = absurd x +qmulMono QW Q0 Q0 QW x _ = absurd x +qmulMono QW Q0 Q1 Q0 x _ = absurd x +qmulMono QW Q0 Q1 Q1 x _ = absurd x +qmulMono QW Q0 Q1 QW x _ = absurd x +qmulMono QW Q0 QW Q0 x _ = absurd x +qmulMono QW Q0 QW Q1 x _ = absurd x +qmulMono QW Q0 QW QW x _ = absurd x +qmulMono QW Q1 Q0 Q0 x _ = absurd x +qmulMono QW Q1 Q0 Q1 x _ = absurd x +qmulMono QW Q1 Q0 QW x _ = absurd x +qmulMono QW Q1 Q1 Q0 x _ = absurd x +qmulMono QW Q1 Q1 Q1 x _ = absurd x +qmulMono QW Q1 Q1 QW x _ = absurd x +qmulMono QW Q1 QW Q0 x _ = absurd x +qmulMono QW Q1 QW Q1 x _ = absurd x +qmulMono QW Q1 QW QW x _ = absurd x +qmulMono QW QW Q0 Q0 _ _ = Oh +qmulMono QW QW Q0 Q1 _ _ = Oh +qmulMono QW QW Q0 QW _ _ = Oh +qmulMono QW QW Q1 Q0 _ y = absurd y +qmulMono QW QW Q1 Q1 _ _ = Oh +qmulMono QW QW Q1 QW _ _ = Oh +qmulMono QW QW QW Q0 _ y = absurd y +qmulMono QW QW QW Q1 _ y = absurd y +qmulMono QW QW QW QW _ _ = Oh + +||| AffineScript's discipline as a lawful algebra: an instance of this +||| record exists, therefore every law above is discharged. +public export +AffineAlgebra : GradeAlgebra Q +AffineAlgebra = MkGradeAlgebra + Q0 Q1 qadd qmul qleq qdec + qaddAssoc qaddComm qaddZeroL + qmulAssoc qmulOneL qmulOneR qmulZeroL qmulZeroR + qdistribL qdistribR + qleqRefl qleqTrans qleqAntisym qaddMono qmulMono diff --git a/src/kernel/Anytype/Grade/Algebra.idr b/src/kernel/Anytype/Grade/Algebra.idr new file mode 100644 index 0000000..71b105c --- /dev/null +++ b/src/kernel/Anytype/Grade/Algebra.idr @@ -0,0 +1,54 @@ +||| anytype L2: the grade-algebra interface. +||| +||| systemet's resource layer (L2) requires an ordered semiring: the +||| discipline of a language is chosen by choosing this algebra. The laws +||| are proof fields, so a `GradeAlgebra` value cannot be constructed +||| without discharging every one of them — an unlawful algebra is +||| unrepresentable, which is how "pins systemet upstream" is enforced +||| mechanically rather than by policy. +||| +||| The carrier is a record *parameter* (not an erased field): erased +||| carrier fields projected into value positions are the documented +||| failure mode of the quarantined template proofs. +module Anytype.Grade.Algebra + +import Data.So + +%default total + +public export +record GradeAlgebra (g : Type) where + constructor MkGradeAlgebra + ||| Additive identity: the grade of an unused variable. + gzero : g + ||| Multiplicative identity: the grade of a single use. + gone : g + ||| Combine usages from independent subterms. + gadd : g -> g -> g + ||| Scale a usage through an application at a graded arrow. + gmul : g -> g -> g + ||| Decidable order: `gleq computed declared` admits a binder. + gleq : g -> g -> Bool + ||| Decidable equality, used by conversion on arrow grades. + gdec : (a, b : g) -> Dec (a = b) + + -- Semiring laws (systemet L2: the stated algebra laws). + addAssoc : (a, b, c : g) -> gadd a (gadd b c) = gadd (gadd a b) c + addComm : (a, b : g) -> gadd a b = gadd b a + addZeroL : (a : g) -> gadd gzero a = a + mulAssoc : (a, b, c : g) -> gmul a (gmul b c) = gmul (gmul a b) c + mulOneL : (a : g) -> gmul gone a = a + mulOneR : (a : g) -> gmul a gone = a + mulZeroL : (a : g) -> gmul gzero a = gzero + mulZeroR : (a : g) -> gmul a gzero = gzero + distribL : (a, b, c : g) -> gmul a (gadd b c) = gadd (gmul a b) (gmul a c) + distribR : (a, b, c : g) -> gmul (gadd a b) c = gadd (gmul a c) (gmul b c) + + -- Order laws, and compatibility of the order with the semiring ops. + leqRefl : (a : g) -> So (gleq a a) + leqTrans : (a, b, c : g) -> So (gleq a b) -> So (gleq b c) -> So (gleq a c) + leqAntisym : (a, b : g) -> So (gleq a b) -> So (gleq b a) -> a = b + addMono : (a, b, c, d : g) -> + So (gleq a b) -> So (gleq c d) -> So (gleq (gadd a c) (gadd b d)) + mulMono : (a, b, c, d : g) -> + So (gleq a b) -> So (gleq c d) -> So (gleq (gmul a c) (gmul b d)) diff --git a/src/kernel/Anytype/Grade/Exact.idr b/src/kernel/Anytype/Grade/Exact.idr new file mode 100644 index 0000000..056d3b2 --- /dev/null +++ b/src/kernel/Anytype/Grade/Exact.idr @@ -0,0 +1,66 @@ +||| The exact-usage grade algebra over Nat: `gleq` is *equality*, so a +||| binder's computed usage must equal its declared grade — dropping a +||| grade-1 value is rejected, unlike the affine order where 0 <= 1. +||| +||| This instance is systemet's required demonstration that the same +||| checking rules instantiate distinct disciplines: the checker code +||| never changes, only the algebra passed to it. +module Anytype.Grade.Exact + +import Data.Nat +import Data.So +import Decidable.Equality +import Anytype.Grade.Algebra + +%default total + +natEqRefl : (n : Nat) -> (n == n) = True +natEqRefl Z = Refl +natEqRefl (S k) = natEqRefl k + +natEqSound : (a, b : Nat) -> (a == b) = True -> a = b +natEqSound Z Z _ = Refl +natEqSound Z (S _) prf = absurd prf +natEqSound (S _) Z prf = absurd prf +natEqSound (S a) (S b) prf = cong S (natEqSound a b prf) + +soSound : (a, b : Nat) -> So (a == b) -> a = b +soSound a b s = natEqSound a b (soToEq s) + +eqRefl : (a : Nat) -> So (a == a) +eqRefl a = rewrite natEqRefl a in Oh + +eqTrans : (a, b, c : Nat) -> So (a == b) -> So (b == c) -> So (a == c) +eqTrans a b c s1 s2 = + rewrite soSound a b s1 in rewrite soSound b c s2 in eqRefl c + +addMono' : (a, b, c, d : Nat) -> + So (a == b) -> So (c == d) -> So ((a + c) == (b + d)) +addMono' a b c d s1 s2 = + rewrite soSound a b s1 in rewrite soSound c d s2 in eqRefl (b + d) + +mulMono' : (a, b, c, d : Nat) -> + So (a == b) -> So (c == d) -> So ((a * c) == (b * d)) +mulMono' a b c d s1 s2 = + rewrite soSound a b s1 in rewrite soSound c d s2 in eqRefl (b * d) + +||| Exact usage: semiring laws come from Data.Nat; the order is equality. +public export +ExactAlgebra : GradeAlgebra Nat +ExactAlgebra = MkGradeAlgebra + 0 1 (+) (*) (==) decEq + (\a, b, c => plusAssociative a b c) + plusCommutative + plusZeroLeftNeutral + (\a, b, c => multAssociative a b c) + multOneLeftNeutral + multOneRightNeutral + multZeroLeftZero + multZeroRightZero + (\a, b, c => multDistributesOverPlusRight a b c) + (\a, b, c => multDistributesOverPlusLeft a b c) + eqRefl + eqTrans + (\a, b, s1, _ => soSound a b s1) + addMono' + mulMono' diff --git a/src/kernel/Anytype/Kernel.idr b/src/kernel/Anytype/Kernel.idr new file mode 100644 index 0000000..9277ff9 --- /dev/null +++ b/src/kernel/Anytype/Kernel.idr @@ -0,0 +1,37 @@ +||| anytype public API: pick the algebra, get the discipline. +||| +||| `checkClosed AffineAlgebra t` and `checkClosed ExactAlgebra t'` +||| run the identical rules under different grade algebras — the +||| discipline is an input, not something hardwired. +module Anytype.Kernel + +import Data.Vect +import public Anytype.Grade.Algebra +import public Anytype.Grade.Affine +import public Anytype.Grade.Exact +import public Anytype.Core.Syntax +import public Anytype.Core.Normalise +import public Anytype.Core.Conversion +import public Anytype.Core.Check + +%default total + +||| Type a closed term under the chosen grade algebra. +public export +checkClosed : GradeAlgebra g -> Term g 0 -> Either CheckError (Ty g) +checkClosed alg t = map (normalise . fst) (infer alg (the (Ctx g 0) []) t) + +||| Check a closed term against an expected type (conversion included). +public export +checkAgainst : GradeAlgebra g -> Term g 0 -> Ty g -> Either CheckError () +checkAgainst alg t ty = map (const ()) (check alg (the (Ctx g 0) []) t ty) + +||| Render a type, given a renderer for grades. +public export +showTy : (g -> String) -> Ty g -> String +showTy _ TUnit = "Unit" +showTy _ TBool = "Bool" +showTy _ (TBits w) = "Bits " ++ show (nval w) +showTy sg (TArr q a b) = + "(" ++ showTy sg a ++ " " ++ sg q ++ "-> " ++ showTy sg b ++ ")" +showTy sg (TProd a b) = "(" ++ showTy sg a ++ " * " ++ showTy sg b ++ ")" diff --git a/verification/tests/kernel/Tests/Main.idr b/verification/tests/kernel/Tests/Main.idr new file mode 100644 index 0000000..28367eb --- /dev/null +++ b/verification/tests/kernel/Tests/Main.idr @@ -0,0 +1,111 @@ +||| Golden matrix for the anytype kernel: the same terms, checked under +||| the affine and the exact grade algebras, must produce the recorded +||| verdicts. The drop row (grade-1 binder, body TT) is the load-bearing +||| demonstration: affine ACCEPTS (0 <= 1), exact REJECTS (0 /= 1) — +||| same rules, distinct disciplines. +module Tests.Main + +import Data.Fin +import System +import Anytype.Kernel + +%default total + +-- Data.Fin.Equality's Pointwise constructors shadow Fin's FZ/FS. +%hide Data.Fin.Equality.FZ +%hide Data.Fin.Equality.FS + +two : TNat +two = NS (NS NZ) + +three : TNat +three = NS two + +four : TNat +four = NS three + +five : TNat +five = NS four + +accepts : Either CheckError a -> Bool +accepts (Right _) = True +accepts (Left _) = False + +||| (name, expected-accept, actual-accept) +Case : Type +Case = (String, Bool, Bool) + +dup : Term g (S n) +dup = Pair (Var FZ) (Var FZ) + +affineCases : List Case +affineCases = + [ ("affine: use once at 1", + True, accepts (checkClosed AffineAlgebra (Lam Q1 TBool (Var FZ)))) + , ("affine: drop at 1 (weakening allowed)", + True, accepts (checkClosed AffineAlgebra (Lam Q1 TBool TT))) + , ("affine: double use at 1", + False, accepts (checkClosed AffineAlgebra (Lam Q1 TBool dup))) + , ("affine: double use at omega", + True, accepts (checkClosed AffineAlgebra (Lam QW TBool dup))) + , ("affine: erased binder unused", + True, accepts (checkClosed AffineAlgebra (Lam Q0 TBool TT))) + , ("affine: erased binder used", + False, accepts (checkClosed AffineAlgebra (Lam Q0 TBool (Var FZ)))) + , ("affine: omega-arrow scales usage past 1 (BUG-001 rule)", + False, accepts (checkClosed AffineAlgebra + (Lam Q1 TBool (App (Lam QW TBool dup) (Var FZ))))) + , ("affine: omega-arrow scaling admitted at omega", + True, accepts (checkClosed AffineAlgebra + (Lam QW TBool (App (Lam QW TBool dup) (Var FZ))))) + , ("affine: let-pair, each component once", + True, accepts (checkClosed AffineAlgebra + (Lam Q1 (TProd TBool TUnit) + (LetPair (Var FZ) (Pair (Var (FS FZ)) (Var FZ)))))) + , ("affine: let-pair, first component twice", + False, accepts (checkClosed AffineAlgebra + (Lam Q1 (TProd TBool TUnit) + (LetPair (Var FZ) (Pair (Var (FS FZ)) (Var (FS FZ))))))) + , ("affine: conversion Bits(2+3) against Bits 5", + True, accepts (checkAgainst AffineAlgebra (WordLit (NPlus two three)) + (TBits five))) + , ("affine: conversion Bits(2+2) against Bits 5", + False, accepts (checkAgainst AffineAlgebra (WordLit (NPlus two two)) + (TBits five))) + , ("affine: application converts Bits(2+3) argument at Bits 5", + True, accepts (checkClosed AffineAlgebra + (App (Lam Q1 (TBits five) (Var FZ)) (WordLit (NPlus two three))))) + ] + +exactCases : List Case +exactCases = + [ ("exact: use once at 1", + True, accepts (checkClosed ExactAlgebra (Lam 1 TBool (Var FZ)))) + , ("exact: drop at 1 REJECTED (the discipline split)", + False, accepts (checkClosed ExactAlgebra (Lam 1 TBool TT))) + , ("exact: double use at 1", + False, accepts (checkClosed ExactAlgebra (Lam 1 TBool dup))) + , ("exact: double use at exactly 2", + True, accepts (checkClosed ExactAlgebra (Lam 2 TBool dup))) + , ("exact: zero binder unused", + True, accepts (checkClosed ExactAlgebra (Lam 0 TBool TT))) + , ("exact: zero binder used", + False, accepts (checkClosed ExactAlgebra (Lam 0 TBool (Var FZ)))) + ] + +report : Case -> IO Bool +report (name, expected, actual) = + if expected == actual + then putStrLn (" PASS " ++ name) $> True + else putStrLn (" FAIL " ++ name + ++ " (expected accept=" ++ show expected + ++ ", got accept=" ++ show actual ++ ")") $> False + +main : IO () +main = do + putStrLn "=== anytype kernel golden matrix ===" + results <- traverse report (affineCases ++ exactCases) + let bad = length (filter not results) + putStrLn ("=== " ++ show (length results) ++ " cases, " + ++ show bad ++ " failure(s) ===") + when (bad > 0) exitFailure