Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ publishing — all backed by YAML provable contracts that fail CI on drift.
| Metric | Count | Source of truth |
|-------:|------:|---|
| Workspace crates | **79** workspace crates | `cargo metadata --no-deps` (NOT `ls crates/` — 4 are `exclude`d, 1 has no Cargo.toml) |
| Provable contracts | **<!-- CONTRACT_COUNT_START -->1800<!-- CONTRACT_COUNT_END -->** provable contracts | `contracts/census.json` `.n_files` — the set `pv lint` walks (`pv census`, ONT-001 ONT-1; regenerated by `make contracts`, written by `make readme-sync`, guarded by `scripts/check_readme_claims.sh`) |
| Provable contracts | **<!-- CONTRACT_COUNT_START -->1801<!-- CONTRACT_COUNT_END -->** provable contracts | `contracts/census.json` `.n_files` — the set `pv lint` walks (`pv census`, ONT-001 ONT-1; regenerated by `make contracts`, written by `make readme-sync`, guarded by `scripts/check_readme_claims.sh`) |
| CLI commands | **110** CLI commands | `apr --help` |
| Book CLI chapters | **112** chapters | `ls book/src/cli/*.md` |
| Book lib chapters | **71** chapters | `ls book/src/lib/*.md` (parity with `pub mod`) |
Expand Down Expand Up @@ -262,7 +262,7 @@ falsification_tests:
prediction: apr validate bad-model.apr exits non-zero
```

The tree carries <!-- CONTRACT_COUNT_START -->1800<!-- CONTRACT_COUNT_END --> contracts across inference, training, quantization, attention, FFN,
The tree carries <!-- CONTRACT_COUNT_START -->1801<!-- CONTRACT_COUNT_END --> contracts across inference, training, quantization, attention, FFN,
tokenization, model formats, CLI safety — and this README itself.

## Migration from old crates
Expand Down
10 changes: 5 additions & 5 deletions contracts/census.json
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
{
"schema": "ont.paiml.dev/census/v1alpha1",
"git_sha": null,
"n_files": 1800,
"n_parsed": 1800,
"n_files": 1801,
"n_parsed": 1801,
"n_parse_errors": 0,
"parse_errors": [],
"quarantined_n": 0,
Expand All @@ -12,7 +12,7 @@
"kernel": 363,
"model-family": 28,
"model-family-variant": 1,
"pattern": 86,
"pattern": 87,
"pretraining-corpus": 2,
"registry": 519,
"schema": 766,
Expand All @@ -25,11 +25,11 @@
"pv-contract": 1
},
"by_anchoring": {
"unanchored": 1797,
"unanchored": 1798,
"class": 2,
"instance": 1
},
"id_set_sha256": "51cfc1e6cf27aa5cb6d9345e918a19863f13aa4728b4eba15bfa69bc6002bfb1",
"id_set_sha256": "e624814d2c82e8a53ab24faac0b5281c0dad15618d9f14e970c740c8391cb712",
"declared_external": [
{
"name": "provable-contracts",
Expand Down
5 changes: 5 additions & 0 deletions contracts/contracts.nt
Original file line number Diff line number Diff line change
Expand Up @@ -9009,6 +9009,11 @@
<https://ont.paiml.dev/v1alpha1/contract/swiglu-kernel-v1> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <https://ont.paiml.dev/v1alpha1/Contract> .
<https://ont.paiml.dev/v1alpha1/contract/swiglu-kernel-v1> <https://ont.paiml.dev/v1alpha1/file> "contracts/swiglu-kernel-v1.yaml"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://ont.paiml.dev/v1alpha1/contract/swiglu-kernel-v1> <https://ont.paiml.dev/v1alpha1/id> "swiglu-kernel-v1"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://ont.paiml.dev/v1alpha1/contract/tag-step-milestone-gate-v1> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://www.w3.org/ns/prov#Entity> .
<https://ont.paiml.dev/v1alpha1/contract/tag-step-milestone-gate-v1> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <https://ont.paiml.dev/v1alpha1/Contract> .
<https://ont.paiml.dev/v1alpha1/contract/tag-step-milestone-gate-v1> <https://ont.paiml.dev/v1alpha1/file> "contracts/tag-step-milestone-gate-v1.yaml"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://ont.paiml.dev/v1alpha1/contract/tag-step-milestone-gate-v1> <https://ont.paiml.dev/v1alpha1/id> "tag-step-milestone-gate-v1"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://ont.paiml.dev/v1alpha1/contract/tag-step-milestone-gate-v1> <https://ont.paiml.dev/v1alpha1/kind> "pattern"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://ont.paiml.dev/v1alpha1/contract/task-pipeline-v1> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://www.w3.org/ns/prov#Entity> .
<https://ont.paiml.dev/v1alpha1/contract/task-pipeline-v1> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <https://ont.paiml.dev/v1alpha1/Contract> .
<https://ont.paiml.dev/v1alpha1/contract/task-pipeline-v1> <https://ont.paiml.dev/v1alpha1/file> "contracts/forjar/task-pipeline-v1.yaml"^^<http://www.w3.org/2001/XMLSchema#string> .
Expand Down
104 changes: 104 additions & 0 deletions contracts/tag-step-milestone-gate-v1.yaml
Original file line number Diff line number Diff line change
@@ -0,0 +1,104 @@
metadata:
version: 1.0.0
created: '2026-09-20'
author: PAIML Engineering
description: "The release train's tag step cannot be reached without a clean milestone. v0.68.1 was tagged 2026-09-17T15:06:29Z by an autopilot copy living outside the repository, six minutes after #3455 merged the milestone gate; `grep -c check_milestone_cut autopilot.sh` was 0. The spec required the read and no code path that cuts a tag made it. This contract is the property that the requirement and the mechanism are the same object: the gate call lives INSIDE cut_tag(), ahead of `git tag`, and a guard runs that function against each gate outcome and asserts on whether a tag was cut."
kind: pattern
references:
- "scripts/release/autopilot.sh — cut_tag(); the gate call precedes `git tag` inside it"
- "scripts/check_milestone_cut.sh — the gate (#3445, #3455); exit 0 clean, 1 open items, 2 cannot judge"
- "scripts/check_tag_step_gated.sh — the behavioural guard and its mutants"
- "docs/specifications/APR-RELEASE-001-train-and-build-kaizen.md — §4 T-0/T-3"
- "docs/specifications/06x-release-schedule.md — §4 steps 1 and 4"
- "contracts/release-schedule-06x-v1.yaml — milestone_settled_at_cut, the schedule-level statement of the same rule"

five_whys:
symptom: "v0.68.1 was tagged while nothing had read its milestone, six minutes after the gate that would have read it merged."
why_1: "The script that cuts the tag was not in the repository — it was a per-train copy under /mnt/nvme-raid0/agent-wt/, so merging a gate into the repo could not reach it."
why_2: "The gate was wired into specifications and into CI, and the tag is cut by neither: the one caller that matters was the one surface nobody enumerated."
why_3: "A rule landed without its enforcer in the same change, so the enforcer's absence was invisible from the rule's side."
why_4: "The only evidence that the gate ran would have been a log line, and a missing log line reads as 'nothing to report' rather than as 'the gate did not run'."
why_5: "Nothing could refuse the tag: `git tag` was reachable from a code path that made no claim about the milestone at all."
root_cause: "The requirement lived in prose and the tag lived in an unversioned script, so there was no object in which both could be false together. The remedy is that the gate call is structurally inside the function that tags, and a guard proves by execution — not by grep — that no gate outcome other than 0 reaches `git tag`."

equations:
tag_requires_clean_milestone:
formula: "cut_tag(v, t, mc) reaches `git tag` iff check_milestone_cut.sh(v) exited 0; rc 1 and rc 2 both die before it"
domain: "the gate's exit codes {0, 1, 2+}"
codomain: "a tag is cut, or the train stops with a STOP line naming which code refused it"
invariants:
- "rc 1 (the milestone holds open items) cuts no tag and publishes nothing"
- "rc 2 (the gate could not judge) cuts no tag — Unknown is not a pass"
- "the gate call precedes `git tag` inside one function, so removing it is a diff to that function and not to a distant caller"

guard_is_behavioural_not_textual:
formula: "check_tag_step_gated.sh extracts cut_tag() from the autopilot, runs it against a stubbed gate once per outcome, and asserts on the presence of a GIT-TAG in the transcript"
domain: "scripts/release/autopilot.sh and three mutants of it"
codomain: "PASS only when rc 0 tags and rc 1 and rc 2 do not"
invariants:
- "a guard that greps for the gate's NAME is satisfied by a comment; this one is not"
- "a mutant with the gate call deleted is RED"
- "a mutant whose gate verdict is discarded with `|| true` is RED"
- "a subject with no cut_tag() is ENV (rc 2), never a pass"

proof_obligations:
- id: TSMG-INV-001
type: invariant
property: "No gate outcome other than 0 reaches `git tag`"
formal: "∀ rc ∈ {1, 2}: cut_tag(v, t, mc) with gate(v) = rc ⇒ ¬ tagged(t) ∧ gate(v) = 0 ⇒ tagged(t)"
applies_to: tag_requires_clean_milestone
- id: TSMG-INV-002
type: invariant
property: "The guard still fails on the defect it names"
formal: "∀ m ∈ {gate_call_deleted, verdict_discarded, cut_tag_removed}: guard(m) ≠ 0 ∧ guard(subject) = 0"
applies_to: guard_is_behavioural_not_textual
- id: TSMG-INV-003
type: invariant
property: "The autopilot that cuts the tag is in the repository and reviewed"
formal: "scripts/release/autopilot.sh ∈ tracked(main) ∧ cut_tag ∈ autopilot.sh"
applies_to: tag_requires_clean_milestone

falsification_tests:
- id: FALSIFY-TSMG-001
rule: "The tag path is in the repository"
prediction: "scripts/release/autopilot.sh is a regular file"
test: "test -f scripts/release/autopilot.sh"
if_fails: "The tag is cut by a script no pull request has ever reviewed — the v0.68.1 condition, restored"

- id: FALSIFY-TSMG-002
rule: "The tag step names the milestone gate"
prediction: "cut_tag() in the autopilot calls scripts/check_milestone_cut.sh"
test: "awk '/^cut_tag\\(\\) \\{/,/^\\}/' scripts/release/autopilot.sh | grep -q 'check_milestone_cut\\.sh'"
if_fails: "`grep -c check_milestone_cut autopilot.sh` is 0 again, which is exactly what was true when v0.68.1 was tagged"

- id: FALSIFY-TSMG-003
rule: "The gate call precedes `git tag` inside cut_tag()"
prediction: "In cut_tag(), the check_milestone_cut.sh line is at a lower line number than the `git tag` line"
test: "b=$(awk '/^cut_tag\\(\\) \\{/,/^\\}/' scripts/release/autopilot.sh); g=$(printf '%s\\n' \"$b\" | grep -n 'check_milestone_cut\\.sh' | head -1 | cut -d: -f1); t=$(printf '%s\\n' \"$b\" | grep -n 'git tag -a' | head -1 | cut -d: -f1); [ -n \"$g\" ] && [ -n \"$t\" ] && [ \"$g\" -lt \"$t\" ]"
if_fails: "A gate that runs after the tag is a receipt, not a gate"

- id: FALSIFY-TSMG-004
rule: "No gate outcome other than 0 reaches `git tag`"
prediction: "The guard runs cut_tag() against a stubbed gate at rc 0, 1 and 2 and exits 0"
test: "bash scripts/check_tag_step_gated.sh"
if_fails: "A tag can be cut while the milestone holds open items, or while the gate could not judge at all"

- id: FALSIFY-TSMG-005
rule: "The guard can still fail on the defect it names"
prediction: "Three mutants — gate call deleted, gate verdict discarded, cut_tag() removed — are each RED, and the real subject is GREEN"
test: "bash scripts/check_tag_step_gated.sh --self-test"
if_fails: "The guard is theater: it would have passed the tree that tagged v0.68.1"

- id: FALSIFY-TSMG-006
rule: "The gate it calls is itself present and self-testing"
prediction: "scripts/check_milestone_cut.sh is a regular file — the repo invokes guards as `bash scripts/...`, so the executable bit is not the property (guard_tree.sh says so of its whole universe)"
test: "test -f scripts/check_milestone_cut.sh"
if_fails: "cut_tag() calls a script that is not there; every cut becomes rc 2 and the train stops — fail-closed, but the gate is gone"

qa_gate:
id: F-TSMG-001
name: "The release train's tag step cannot be reached without a clean milestone"
description: "The gate call lives inside cut_tag() ahead of `git tag`, and check_tag_step_gated.sh proves by execution that rc 1 and rc 2 both refuse the tag. guard_tree.sh's universe is `git ls-files 'scripts/check_*.sh'`, so the guard runs in the guard-tree job, which `ci / gate` reads through needs.guard-tree.result."
checks:
- "tag_requires_clean_milestone"
- "guard_is_behavioural_not_textual"
Loading
Loading