Skip to content

AFFIRMATION.adoc

Latest commit

 

History

History
235 lines (187 loc) · 9.37 KB

AFFIRMATION.adoc

File metadata and controls

235 lines (187 loc) · 9.37 KB
Raw

AFFIRMATION — git-reticulator, as of 2026-10-07

Table of Contents
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

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

    1. 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)

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.

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:

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.