diff --git a/AFFIRMATION.adoc b/AFFIRMATION.adoc new file mode 100644 index 0000000..e7f7159 --- /dev/null +++ b/AFFIRMATION.adoc @@ -0,0 +1,235 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += AFFIRMATION — git-reticulator, as of 2026-10-07 +Jonathan D.A. Jewell +:status: DRAFT — agent-authored, NOT affirmed by the owner +:toc: +:icons: font + +[WARNING] +==== +*DRAFT.* An AI agent wrote this file and did not commit it. It becomes an +affirmation only when the owner lands it with a signed commit whose parent is +the anchor SHA below +(`19f568189c465ba6666b6c26ece059d5871f58e1`). Until then, read it as a draft. +==== + +== What this is, and how it works + +git-reticulator is a Rust crate with one binary, `reticulate`. `reticulate +build` walks a repository and writes a graph of its directories, files and +definitions to `.git-reticulator/lattice.json`. `reticulate query` returns a +token-budgeted context pack from that graph. Optional Cargo features +(`git-integration`, `verisim`, `db`, `embeddings`) add git history, a +VeriSimDB sink, Postgres and embeddings. A separate Idris2 corpus in +`verification/proofs/` proves elementary order theory. The AffineScript files +under `src/lattice/affine/` are not compiled by anything. + +== The epistemic contract + +You may conclude that, at the anchor commit and at the stated time, each +command below produced the stated exit code and count on the stated toolchain. + +You may *not* conclude that the structure the Rust code builds is a lattice or +a partial order. The Idris2 proofs are about an abstract `PartialOrder` +record and natural numbers; nothing connects them to the Rust graph. You may +also not conclude anything about the `verisim`, `db` or `embeddings` +features: none was built or tested. + +== Verifiable anchor + +[cols="1,3", options="header"] +|=== +| Field | Value + +| Repo +| `hyperpolymath/git-reticulator` + +| Branch +| `main` (worktree branch `docs/affirmation-2026-10-07` at `origin/main`) + +| Commit (HEAD) +| `19f568189c465ba6666b6c26ece059d5871f58e1` + +| Permalink +| https://github.com/hyperpolymath/git-reticulator/tree/19f568189c465ba6666b6c26ece059d5871f58e1 + +| Verified (UTC) +| 2026-10-07T10:51:23Z (first run) to 2026-10-07T10:55:01Z (last run) + +| Working-tree delta at verification +| `clean`. `git status --porcelain` was empty. The dogfood run wrote + `.git-reticulator/` and the Idris2 build wrote `verification/proofs/build/`; + both are gitignored and were removed afterwards. Cargo output went to a + target directory outside the tree. + +| Toolchain +| rustc 1.99.0 (b940084d7 2026-09-28), cargo 1.99.0 (5f94df478 2026-08-27), + Idris 2 0.8.0, GNU grep, git 2.47.3. Debian 13 on WSL2. +|=== + +[IMPORTANT] +==== +If you are reading this at a later commit, the claims may have drifted. Re-run +the reproduction steps and write a fresh affirmation; do not trust a stale one. +==== + +== Companion documents and repo metadata (cross-check) + +* `README.adoc` calls the project *experimental* and says the proofs cover + abstract order theory only. Both statements agree with the runs below. +* `PROOF-NEEDS.adoc` says the built structure is "a typed, weighted digraph + ... not (yet) a lattice, not even a partial order", and asks prose to say + "typed graph" until that is proved. This file follows that rule. The dogfood + run below reports `acyclic=true` for this repository, which is a property of + one input, not a proof. +* `docs/DOGFOOD.adoc` describes the build-then-query loop. It says token + savings are not yet measured. This file does not measure them either. +* `README.adoc` sends readers to `.machine_readable/6a2/STATE.a2ml` for the + honest status (lines 23 and 97). That directory and its six `.a2ml` files + still exist at the anchor, last changed 2026-08-28. A2ML is a retired + format in this estate; see *Outstanding* below. + +== The honest state (one breath) + +The Rust test suites pass in the default and `git-integration` builds, the +code is `rustfmt`-clean, and the binary builds a graph of its own repository +and answers a budgeted query. The Idris2 order-theory module type-checks with +no proof escapes. The proofs do not yet touch the Rust code. + +=== What is solid (and how we checked) + +[cols="2,3,1", options="header"] +|=== +| Claim | Command | Result + +| Default-feature tests pass +| `cargo test --locked` +| exit 0; 38 passed, 0 failed (17 lib, 2 api, 13 integration, + 6 property; 0 doc-tests) + +| `git-integration` tests pass (the feature CI uses) +| `cargo test --locked --features git-integration` +| exit 0; 39 passed, 0 failed (18 lib, 2 api, 13 integration, + 6 property) + +| Formatting is clean +| `cargo fmt --all --check` +| exit 0 + +| The binary builds +| `cargo build --locked --features git-integration` +| exit 0, 0 warnings in the log + +| Dogfood build works on this repository +| `reticulate build --repo .` +| exit 0; 262 nodes, 196 edges, 262 components, `acyclic=true` + +| Dogfood query honours the token budget +| `reticulate query --repo . --zoom lattice --level file + --budget-tokens 800`; then the same with `--budget-tokens 100` +| exit 0 both; 2804 bytes at 800; 504 bytes at 100, with 2 "omitted + (budget)" lines + +| The Idris2 corpus type-checks +| `idris2 --build git-reticulator-proofs.ipkg` in `verification/proofs` +| exit 0; 1 of 1 module built (`Lattice.Order`, `%default total`) + +| No proof escapes in the corpus +| `grep -rnE '\b(believe_me|really_believe_me|assert_total|assert_smaller| + idris_crash|postulate|sorry)\b' verification/proofs --include='*.idr'` +| exit 1 (0 matches) + +| That grep can find an escape +| Same grep on a scratch copy of the corpus with `bad = believe_me ()` + appended to `Lattice/Order.idr` +| 1 match (planted control) +|=== + +=== The honest nuance you must not lose + +* "Lattice" is the project's name for its output, not a proved property. + `Lattice/Order.idr` proves reflexivity, transitivity and antisymmetry for an + abstract record and gives one instance, `Leq` on `Nat`. It does not mention + the Rust types. +* The crate is small: `src/` holds 1777 lines of Rust (`wc -l`) and 128 lines + of AffineScript that nothing compiles. +* `reticulate build --db postgresql://x` exits 0 in the default build. It + prints a warning that `--db` is ignored without `--features verisim`, then + writes the local file. That is a loud fallback, but the exit code alone + would not tell a script that the database write did not happen. +* The two test runs share 38 tests. The 39th, + `ingest::git_history_tests::ingests_self_repo_with_structure_and_remains_a_dag`, + exists only with `git-integration`; it checks that this repository's own + graph is a DAG, which again is one input, not a proof. + +=== Known-incomplete but honestly fenced + +* The `verisim`, `db` and `embeddings` features were not built or tested here. + `embeddings` pulls in `tch` (libtorch), which this machine was not set up + for. The README says these are feature-gated off. +* `README.adoc` and `docs/DOGFOOD.adoc` both say token savings are not yet + measured. That is still true. + +=== Outstanding / weak / refuted (no spin) + +* The README points readers to `.machine_readable/6a2/STATE.a2ml`, + `NEUROSYM.a2ml` and `PLAYBOOK.a2ml` as the canonical state. The estate has + retired A2ML and the `6a2/` directory. Six `.a2ml` files remain there, and a + seventh, `0-AI-MANIFEST.a2ml`, sits at the root. This file does not cite any + of them as evidence. +* There is no link between the Idris2 proofs and the Rust graph, as + `PROOF-NEEDS.adoc` itself says. +* On this machine the repo's `mise.toml` is not trusted, and the cargo shim + that `mise` provides refuses to run in the tree. The runs above used the + cargo binaries directly. This is a machine setting, not a repo defect, but + `just test` fails out of the box here for that reason. + +== Reproduce it yourself + +Run from the repository root at the anchor commit. + +[source,bash] +---- +cargo test --locked # 38 passed, 0 failed +cargo test --locked --features git-integration # 39 passed, 0 failed +cargo fmt --all --check # exit 0 +cargo build --locked --features git-integration # exit 0 +./target/debug/reticulate build --repo . # 262 nodes, 196 edges +./target/debug/reticulate query --repo . --zoom lattice --level file \ + --budget-tokens 800 # exit 0 +ESC='believe_me|really_believe_me|assert_total|assert_smaller' +ESC="$ESC|idris_crash|postulate|sorry" +grep -rnE "\b($ESC)\b" verification/proofs --include='*.idr' + # no output, exit 1 +(cd verification/proofs && idris2 --build git-reticulator-proofs.ipkg) + # 1/1 Lattice.Order +rm -rf .git-reticulator verification/proofs/build # tidy up +---- + +The node and edge counts describe this commit's own tree. They change +whenever a file is added or removed. + +== One-line characterisation (quote this) + +At `19f56818`, git-reticulator passes 39 of 39 Rust tests with +`git-integration`, builds and queries a 262-node graph of itself, and +type-checks one escape-free Idris2 order-theory module that does not yet +speak about the Rust code. + +== Joint attestation + +*Engineering party (AI).* `claude-opus-5-5` ran every command in this file +between 2026-10-07T10:51:23Z and 2026-10-07T10:55:01Z, in a git worktree +checked out at the anchor commit. The wording above is a faithful report of +those runs. No claim was copied from an earlier document. + +*Owner / maintainer.* Jonathan D.A. Jewell signs by landing this file: + +[source,bash] +---- +git commit -S -s -m "docs: affirm state at 19f56818" +git log --show-signature -1 +---- + +The affirmation is anchored only if the parent of that commit is +`19f568189c465ba6666b6c26ece059d5871f58e1` and the signature verifies.