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
20 changes: 20 additions & 0 deletions .github/workflows/guards-nightly.yml
Original file line number Diff line number Diff line change
Expand Up @@ -201,9 +201,19 @@ jobs:
run: setsid --wait bash scripts/check_book_examples_compile.sh
- name: Harness fixture servers die with their harness (LAB, quarantined from the merge path, #5873)
run: setsid --wait bash scripts/check_harness_server_cleanup.sh
- name: Coverage scan files no per-function ticket (LAB, #5879)
id: lab_cov_scan
if: ${{ !cancelled() }}
env:
GH_TOKEN: ${{ github.token }}
run: |
set -euo pipefail
{ setsid --wait bash scripts/check_coverage_single_report.sh --self-test && setsid --wait bash scripts/check_coverage_single_report.sh; } 2>&1 | tee "$RUNNER_TEMP/cov-scan.log"
- name: aprender-profile lib tests (was gated by nothing)
if: ${{ !cancelled() }}
run: cargo test -p aprender-profile --lib
- name: model-tests falsification suites (was gated by nothing, aprender#2522) -- SATD ceiling measured on the comparand (BSE-03)
if: ${{ !cancelled() }}
run: |
set -euo pipefail
# The warm sccache lives under the runner user's data dir on the persistent intel
Expand Down Expand Up @@ -303,6 +313,16 @@ jobs:
set -euo pipefail
bash scripts/lab_ticket.sh --label lab-ladder-gap --title "LAB: the model ladder owes cells to model-cell commands (ladder-gap, #3745)" \
--owner aprender-a7 --log "$RUNNER_TEMP/ladder-gap.log" --event "$GITHUB_EVENT_NAME" --run-url "$RUN_URL"
- name: A red coverage-scan night opens or updates its one LAB ticket (#5879)
if: failure() && steps.lab_cov_scan.outcome == 'failure'
env:
GH_TOKEN: ${{ github.token }}
GH_REPO: ${{ github.repository }}
RUN_URL: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}
run: |
set -euo pipefail
bash scripts/lab_ticket.sh --label lab-cov-scan --title "LAB: an open per-function coverage ticket is not rolled into epic #5875 (#5879)" \
--owner aprender-flow --log "$RUNNER_TEMP/cov-scan.log" --event "$GITHUB_EVENT_NAME" --run-url "$RUN_URL"
# #5182 (GATE/LAB). The two ratchets that left the PR path. On a schedule
# run HEAD *is* origin/main, so merge-base(HEAD, origin/main) is HEAD and a
# shrink-only comparison against it can never fail. The comparand is
Expand Down
4 changes: 2 additions & 2 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -114,7 +114,7 @@ publishing — all backed by YAML provable contracts that fail CI on drift.
| Metric | Count | Source of truth |
|-------:|------:|---|
| Workspace crates | **81** workspace crates | `cargo metadata --no-deps` (NOT `ls crates/` — 4 are `exclude`d, 1 has no Cargo.toml) |
| Provable contracts | **<!-- CONTRACT_COUNT_START -->2001<!-- 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 -->2005<!-- 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 | **113** CLI commands | `contracts/apr-cli-commands-v1.yaml` §`commands` (parse the list; `apr --help` also lists `help` itself, and `grep -c '^ - name:'` gives 119 — other same-indent `name:` keys exist in the file) |
| Book CLI chapters | **114** chapters | `ls book/src/cli/*.md` |
| Book lib chapters | **73** chapters | `ls book/src/lib/*.md` (parity with `pub mod`) |
Expand Down Expand Up @@ -403,7 +403,7 @@ falsification_tests:
prediction: apr validate bad-model.apr exits non-zero
```

The tree carries <!-- CONTRACT_COUNT_START -->2001<!-- CONTRACT_COUNT_END --> contracts across inference, training, quantization, attention, FFN,
The tree carries <!-- CONTRACT_COUNT_START -->2005<!-- 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
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
cargo test -p aprender-cgp --test quant_profile_output
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
cargo test -p aprender-serve --test qwen35_load_failclosed_5678
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
cargo test -p aprender-train --test execute_plan_guards_5674
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
cargo test -p aprender-orchestrate --test repl_slash
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
cargo test -p aprender-contracts-cli --test certify_analyze_config_5622
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
cargo test -p aprender-profile --test run_config_errors_5713
6 changes: 6 additions & 0 deletions contracts/bin-aprender-contracts-cli--pv-v1.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -174,3 +174,9 @@ falsification_tests:
test: 'cargo test -p aprender-contracts-cli --test coverage_report_render'
if_fails: 'the coverage report renderer drifts without a test noticing'
mutation: 'print binding_partial in the Binding implemented line; coverage_with_binding_adds_binding_totals must turn RED (MEASURED 2026-10-19)'
- id: FALSIFY-BIN-PV-007
rule: '`certify` config analysis flags the algebraic constraints a transformer needs'
prediction: 'analyze_config derives head_dim = hidden/heads, defaults kv heads to heads, and names each failing check (positivity, hidden%heads, heads%kv, even head_dim) without dividing by zero'
test: 'cargo test -p aprender-contracts-cli --test certify_analyze_config_5622'
if_fails: 'a malformed config.json is certified, or the report names the wrong constraint'
mutation: 'change `head_dim % 2 == 0` to `head_dim % 2 == 1`; odd_head_dim_fails_only_the_rope_check must turn RED'
6 changes: 6 additions & 0 deletions contracts/bin-aprender-profile--aprender-profile-v1.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -133,3 +133,9 @@ falsification_tests:
test: 'cargo test -p aprender-profile --test cli_surface_gate unusable_input_is_rejected'
if_fails: 'MEASURED 2026-09-27 (aprender-01): each exits 2 ("Baseline not found", the documented code) with no panic, GREEN; an existing FILE is also reported "not found" because a baseline is a directory'
mutation: 'make a rejection path return Ok(()) or unwrap the read; must turn RED on that row'
- id: FALSIFY-BIN-APRENDER-PROFILE-007
rule: 'run rejects bad configuration before tracing, naming the flag'
prediction: '`--ml-clusters 1`, a missing or malformed `--transpiler-map`, an unknown `--chaos` preset and an unparsable `--chaos-memory-limit` each exit 1 with a stderr message naming the offending value'
test: 'cargo test -p aprender-profile --test run_config_errors_5713'
if_fails: 'a bad flag is silently accepted and a trace starts with a default (#5713)'
mutation: 'change the ml_clusters guard from < 2 to < 1; ml_clusters_below_two_is_rejected_with_the_value must turn RED'
6 changes: 6 additions & 0 deletions contracts/bin-aprender-qa-cli--apr-qa-v1.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -135,3 +135,9 @@ falsification_tests:
test: 'cargo test -p aprender-qa-cli --test cli_surface_gate unusable_input_is_rejected'
if_fails: 'MEASURED 2026-09-26 (aprender-01): GREEN on an unmutated tree; no source mutation was run for this binary'
mutation: 'make a rejection path return Ok(()) or unwrap the read; must turn RED on that row'
- id: FALSIFY-BIN-APR-QA-007
rule: 'profile throughput minimums resolve per backend, then legacy, then 5 (cpu) / 50 (gpu)'
prediction: 'check_profiling_assertions records a failed assertion exactly when a measured tok/s is below the resolved minimum, and records nothing when profile_ci is absent'
test: 'cargo test -p aprender-qa-cli --lib profiling_assertion_tests'
if_fails: 'a throughput regression passes certification, or a legacy min_throughput stops applying'
mutation: 'change unwrap_or(5.0) to unwrap_or(6.0) in check_profiling_assertions; defaults_are_5_cpu_and_50_gpu must turn RED (run 2026-10-21T10:15Z on lambda-labs: mutant rc=101, 2 of 5 RED incl. defaults_are_5_cpu_and_50_gpu; restored rc=0, 5 passed)'
6 changes: 5 additions & 1 deletion contracts/classification-finetune-v1.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -151,7 +151,11 @@ falsification_tests:
prediction: 'evaluate_checkpoint on an adapter checkpoint evaluates with the classifier head stored in model.safetensors, so a bias of +50 on class k puts every sample in confusion-matrix column k'
test: 'aprender-train finetune::classify_trainer::tests::test_evaluate_checkpoint_uses_restored_weights'
if_fails: 'The report would describe a randomly initialised model, not the trained checkpoint, and look plausible. MUTANT: skip restore_checkpoint_weights turns 2 rows RED.'

- id: FALSIFY-CLASS-011
rule: Apply preconditions fail loudly, by kind
prediction: 'execute_plan returns ConfigError naming a missing model dir, Io naming missing training data, and ConfigError for an unknown model size (GH-377) after creating the output dir; none fall through to training'
test: 'aprender-train --test execute_plan_guards_5674 (4 tests)'
if_fails: 'A precondition was dropped or its error kind changed; apply would start training against a missing model/data or silently default the model size. MUTANT: execute_plan missing-data guard returning ConfigError instead of Io turns missing_training_data_is_an_io_error RED.'
kani_harnesses:
- id: KANI-FT-001
obligation: FT-INV-001
Expand Down
20 changes: 20 additions & 0 deletions contracts/contracts.nt
Original file line number Diff line number Diff line change
Expand Up @@ -11793,6 +11793,11 @@
<https://ont.paiml.dev/v1alpha1/contract/explain-tui-draw-scrollbar-v1> <https://ont.paiml.dev/v1alpha1/file> "contracts/explain-tui-draw-scrollbar-v1.yaml"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://ont.paiml.dev/v1alpha1/contract/explain-tui-draw-scrollbar-v1> <https://ont.paiml.dev/v1alpha1/id> "explain-tui-draw-scrollbar-v1"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://ont.paiml.dev/v1alpha1/contract/explain-tui-draw-scrollbar-v1> <https://ont.paiml.dev/v1alpha1/kind> "pattern"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://ont.paiml.dev/v1alpha1/contract/explain-tui-register-panel-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/explain-tui-register-panel-v1> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <https://ont.paiml.dev/v1alpha1/Contract> .
<https://ont.paiml.dev/v1alpha1/contract/explain-tui-register-panel-v1> <https://ont.paiml.dev/v1alpha1/file> "contracts/explain-tui-register-panel-v1.yaml"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://ont.paiml.dev/v1alpha1/contract/explain-tui-register-panel-v1> <https://ont.paiml.dev/v1alpha1/id> "explain-tui-register-panel-v1"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://ont.paiml.dev/v1alpha1/contract/explain-tui-register-panel-v1> <https://ont.paiml.dev/v1alpha1/kind> "pattern"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://ont.paiml.dev/v1alpha1/contract/export-user-metadata-roundtrip-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/export-user-metadata-roundtrip-v1> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <https://ont.paiml.dev/v1alpha1/Contract> .
<https://ont.paiml.dev/v1alpha1/contract/export-user-metadata-roundtrip-v1> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <https://ont.paiml.dev/v1alpha1/Kernel> .
Expand Down Expand Up @@ -12555,6 +12560,11 @@
<https://ont.paiml.dev/v1alpha1/contract/model-capability-ladder-v1> <https://ont.paiml.dev/v1alpha1/file> "contracts/model-capability-ladder-v1.yaml"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://ont.paiml.dev/v1alpha1/contract/model-capability-ladder-v1> <https://ont.paiml.dev/v1alpha1/id> "model-capability-ladder-v1"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://ont.paiml.dev/v1alpha1/contract/model-capability-ladder-v1> <https://ont.paiml.dev/v1alpha1/kind> "pattern"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://ont.paiml.dev/v1alpha1/contract/model-card-paint-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/model-card-paint-v1> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <https://ont.paiml.dev/v1alpha1/Contract> .
<https://ont.paiml.dev/v1alpha1/contract/model-card-paint-v1> <https://ont.paiml.dev/v1alpha1/file> "contracts/model-card-paint-v1.yaml"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://ont.paiml.dev/v1alpha1/contract/model-card-paint-v1> <https://ont.paiml.dev/v1alpha1/id> "model-card-paint-v1"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://ont.paiml.dev/v1alpha1/contract/model-card-paint-v1> <https://ont.paiml.dev/v1alpha1/kind> "pattern"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://ont.paiml.dev/v1alpha1/contract/model-config-algebra-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/model-config-algebra-v1> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <https://ont.paiml.dev/v1alpha1/Contract> .
<https://ont.paiml.dev/v1alpha1/contract/model-config-algebra-v1> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <https://ont.paiml.dev/v1alpha1/Kernel> .
Expand Down Expand Up @@ -13990,6 +14000,11 @@
<https://ont.paiml.dev/v1alpha1/contract/tensor-transpose-roundtrip-v1> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <https://ont.paiml.dev/v1alpha1/Kernel> .
<https://ont.paiml.dev/v1alpha1/contract/tensor-transpose-roundtrip-v1> <https://ont.paiml.dev/v1alpha1/file> "contracts/tensor-transpose-roundtrip-v1.yaml"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://ont.paiml.dev/v1alpha1/contract/tensor-transpose-roundtrip-v1> <https://ont.paiml.dev/v1alpha1/id> "tensor-transpose-roundtrip-v1"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://ont.paiml.dev/v1alpha1/contract/test-lib-loadtest-run-phase-max-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/test-lib-loadtest-run-phase-max-v1> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <https://ont.paiml.dev/v1alpha1/Contract> .
<https://ont.paiml.dev/v1alpha1/contract/test-lib-loadtest-run-phase-max-v1> <https://ont.paiml.dev/v1alpha1/file> "contracts/test-lib-loadtest-run-phase-max-v1.yaml"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://ont.paiml.dev/v1alpha1/contract/test-lib-loadtest-run-phase-max-v1> <https://ont.paiml.dev/v1alpha1/id> "test-lib-loadtest-run-phase-max-v1"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://ont.paiml.dev/v1alpha1/contract/test-lib-loadtest-run-phase-max-v1> <https://ont.paiml.dev/v1alpha1/kind> "pattern"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://ont.paiml.dev/v1alpha1/contract/tfidf-l2-norm-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/tfidf-l2-norm-v1> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <https://ont.paiml.dev/v1alpha1/Contract> .
<https://ont.paiml.dev/v1alpha1/contract/tfidf-l2-norm-v1> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <https://ont.paiml.dev/v1alpha1/Kernel> .
Expand Down Expand Up @@ -14107,6 +14122,11 @@
<https://ont.paiml.dev/v1alpha1/contract/tracing-observability-v1> <https://ont.paiml.dev/v1alpha1/id> "tracing-observability-v1"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://ont.paiml.dev/v1alpha1/contract/tracing-observability-v1> <https://ont.paiml.dev/v1alpha1/name> "tracing-observability"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://ont.paiml.dev/v1alpha1/contract/tracing-observability-v1> <https://ont.paiml.dev/v1alpha1/version> "1.0.0"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://ont.paiml.dev/v1alpha1/contract/train-classify-train-loop-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/train-classify-train-loop-v1> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <https://ont.paiml.dev/v1alpha1/Contract> .
<https://ont.paiml.dev/v1alpha1/contract/train-classify-train-loop-v1> <https://ont.paiml.dev/v1alpha1/file> "contracts/train-classify-train-loop-v1.yaml"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://ont.paiml.dev/v1alpha1/contract/train-classify-train-loop-v1> <https://ont.paiml.dev/v1alpha1/id> "train-classify-train-loop-v1"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://ont.paiml.dev/v1alpha1/contract/train-classify-train-loop-v1> <https://ont.paiml.dev/v1alpha1/kind> "pattern"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://ont.paiml.dev/v1alpha1/contract/train-loader-try-load-apr-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/train-loader-try-load-apr-v1> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <https://ont.paiml.dev/v1alpha1/Contract> .
<https://ont.paiml.dev/v1alpha1/contract/train-loader-try-load-apr-v1> <https://ont.paiml.dev/v1alpha1/file> "contracts/train-loader-try-load-apr-v1.yaml"^^<http://www.w3.org/2001/XMLSchema#string> .
Expand Down
5 changes: 5 additions & 0 deletions contracts/distributed-training-v1.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -33,3 +33,8 @@ falsification:
description: "loss(distributed, N) ≈ loss(single, N) within ε"
test: "Related tests in crates/aprender-distribute/src/"
evidence: "cargo test --lib"

- id: FALSIFY-DISTRIBUTED_TRAINING_V1_003
description: "run_worker clamps an out-of-range shard to the training split and fails closed on a bad coordinator (Shutdown mid-AllReduce, non-shard message, refused connect)"
test: "crates/aprender-train/src/finetune/classify_trainer_tests.rs::run_worker_tests"
evidence: "cargo test -p aprender-train --lib run_worker_tests"
47 changes: 47 additions & 0 deletions contracts/explain-tui-register-panel-v1.yaml
Original file line number Diff line number Diff line change
@@ -0,0 +1,47 @@
metadata:
id: C-EXPLAIN-TUI-REGISTER-PANEL
version: 1.0.0
created: '2026-10-19'
author: PAIML Engineering
kind: pattern
status: ACTIVE_ALGORITHM_LEVEL
description: |
Pins the register panel drawn by the aprender-explain TUI sidebar (#5594):
one line per register class with its limit, a total/occupancy line, and a
status colour that is green below 64 registers, yellow from 64 to 127 and
red from 128.
references:
- 'crates/aprender-explain/src/tui/widgets.rs (render_register_panel)'

equations:
register_panel_status_colour:
formula: |
colour(total) = green if total < 64, yellow if total < 128, else red
domain: RegisterUsage totals passed through render_sidebar
invariants:
- 'the thresholds are 64 and 128, lower bound inclusive'

proof_obligations:
- id: ERP-INV-001
type: invariant
property: register panel text and status colour follow the total register count
formal: 'colour ≡ threshold'
applies_to: register_panel_status_colour

falsification_tests:
- id: FALSIFY-EXPLAIN-TUI-REGISTER-PANEL-001
rule: render_register_panel draws exact lines and the threshold colour
prediction: 'totals 63, 64, 127 and 128 give green, yellow, yellow and red borders; the lines show the .f32/.b32/.b64/.pred counts and the Total/occ text'
test: cargo test -p aprender-explain --lib register_panel
if_fails: the TUI misreports register pressure on a kernel
ship_blocking: false
mutation: 'change either < to <=, or print the wrong register field; each must turn RED'

qa_gate:
id: QA-EXPLAIN-TUI-REGISTER-PANEL-001
name: Explain TUI register panel gate
description: register panel text and colour thresholds are exact
checks:
- register_panel_status_colour
pass_criteria: FALSIFY-EXPLAIN-TUI-REGISTER-PANEL-001 passes
falsification: Any failure fails the gate
Loading
Loading