Stepwise resource-bounding types: deterministic memory first, network resources second. This checkout hosts the Session IR calculus, checker and Idris spike (ULTRAPLAN R0-B) and the stackcert certificate checker (R1) on top of the RSR scaffold.
-
Plan of record (thesis, rung contract, kill criteria, decision log):
ULTRAPLAN.md -
Operational model (what the grade means):
docs/OPERATIONAL-MODEL.md -
Claims-to-files map (with verification status):
docs/EXPLAINME.adoc -
Vocabulary:
docs/glossary.adoc· Retractions & blocked runs:docs/retraction-ledger.adoc -
The gate:
just check(= proofs + tests + expected-rejection controls
checker on fixtures;just check-irruns the toolchain-free slice)
This repo is one node of the hyperpolymath type-theory family. The shared
map — vocabulary, connection obligations, ownership routing — lives in
nextgen-typing:
TYPE-CONNECTIONS.adoc.
-
Question this repo asks — how do live-state footprints compose, and when are they reclaimed? (Occupancy/HWM grades; protocol frontier = reclamation.)
-
Boundary — an occupancy bound is not a cost bound (HWM monoid ≠ max-plus); a measured live-byte count is not an occupancy grade. Cost grades live in tropical-types (the ULTRAPLAN name
tropical-resource-typingresolves there). -
Not this repo — echo indices, warrants, residue measures (shared glossary in TYPE-CONNECTIONS separates all of these from resource grades).
Quick start (Python 3, stdlib only):
PYTHONPATH=src python3 -m session_ir test examples/session_ir/manifest.json
PYTHONPATH=src python3 -m session_ir check examples/session_ir/accept_seq_add.sir|
Important
|
This file still contains RSR template material. You are reading |
A new repository scaffolded from the Rhodium Standard Repository (RSR) template: a batteries-included starting point that ships with CI/CD, machine-readable project metadata, an AI-agent gatekeeper protocol, a formally-typed ABI/FFI seam (Idris2 + Zig), container and reproducible-build scaffolding, and governance infrastructure — all wired and passing the RSR validators on day one.
Replace this section with a description of your project once initialised.
# 1. Create a repo from this template (or clone it), then from the repo root:
just repo-init # interactive bootstrap: fills every {{PLACEHOLDER}}
# 2. See the available tasks:
just # lists all phases (build, test, validate, audit, ...)
# 3. Check the repo still satisfies the RSR shape:
just validate # structure + metadata checksjust repo-init prompts for the project name, owner, author, licence contact, and the
other values listed in .machine_readable/ai/PLACEHOLDERS.adoc, substitutes them
across the tree, validates the result, and (if available) runs the k9-svc checks.
If you are an AI agent installing this project, read the AI installation guide first — it gives the orientation order, the full prompt sequence, and the privacy notice.
The one trap worth stating up front: do not set RSR_NON_INTERACTIVE=1. It
stubs the shell builtin read, which also disables the loops that perform token
substitution — the run never terminates and substitutes nothing. Pipe answers to
stdin instead.
-
Machine-readable metadata (
.machine_readable/descriptiles/) —STATE,META,ECOSYSTEM,PLAYBOOK,AGENTIC,NEUROSYM,CLADE, andanchors/ANCHOR, in deed, so tools and agents can read the project’s state and boundaries. -
AI gatekeeper protocol —
rsr-template-repo_chora.deed(the repo deed) is the universal entry point that tells an AI agent how to work in this repo before it touches anything; it carries the AI allocation policy and the ply directory tree. -
Typed ABI/FFI seam —
src/interface/Abi/(Idris2 type + layout proofs) oversrc/interface/ffi/(Zig implementation), with generated C headers. -
CI/CD — GitHub Actions for quality, security (CodeQL, Scorecard, secret scanning), multi-forge mirroring, and RSR anti-pattern enforcement.
-
Supply-chain & reproducibility — container layering (stapeln), Guix shells, SBOM, and signing hooks.
-
Governance —
GOVERNANCE.adoc,MAINTAINERS.adoc,.github/community health files, and a releaseAUDIT.adocgate.
The authoritative map is generated, so it cannot drift from the tree:
docs/architecture/REPOSITORY-MAP.adoc
(regenerate with just repo-map; CI fails if it is stale).
The short version:
| Path | What lives there |
|---|---|
|
Start here - humans and AI agents respectively. |
|
The code and its tests. |
|
Human documentation, including the full map above. |
|
Manifests, contractiles and policies that tools read. |
|
Every task runs through |
|
CI configuration; GitHub reads |
-
The repository map — generated; what every directory is for.
-
EXPLAINME — the engineering deep-dive: how the pieces actually work.
-
AFFIRMATION — the dated, signed honesty snapshot of the repo’s true state.
-
AUDIT — the release audit gate.
-
AI installation guide — for agents instantiating this template.
-
PLACEHOLDERS — the full placeholder reference.
Code, configuration and scripts are Mozilla Public License 2.0
(MPL-2.0); prose documentation is CC-BY-SA-4.0. Both texts live in
LICENSES/, and per-file SPDX-License-Identifier headers are authoritative.
The GitHub-detected licence is MPL-2.0 (the root LICENSE). Long-term
attribution uses Quantum-Safe Provenance — see
the Quantum-Safe Provenance exhibit.