diff --git a/.claude/skills/apr-dogfood/SKILL.md b/.claude/skills/apr-dogfood/SKILL.md index 39f6ed15a2..327d53f2fa 100644 --- a/.claude/skills/apr-dogfood/SKILL.md +++ b/.claude/skills/apr-dogfood/SKILL.md @@ -1594,7 +1594,7 @@ The nine clusters at zero, largest first: `http-orchestrate-banco` (95), `test-harness` (49), `rag-eval` (44), `qa-cgp` (37), `simulation` (18), `orchestrate-pacha-secrets` (17). -**Report both numbers or neither (T2).** "5 of 14 clusters gated (35.7%)" without "144 of 907 features gated (15.9%)" beside it is a proxy masquerading as coverage, and the gate refuses to emit it — *on this line too*. +**Report both numbers or neither (T2).** "5 of 14 clusters gated (35.7%)" without "144 of 911 features gated (15.8%)" beside it is a proxy masquerading as coverage, and the gate refuses to emit it — *on this line too*. The rule is about the NUMBER, not about a phrasing, and it is enforced on every surface that can emit one: the gate's own report, the receipt, the output of diff --git a/README.md b/README.md index 066292a350..a2c2305d2e 100644 --- a/README.md +++ b/README.md @@ -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 | **1989** 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 | **1993** 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`) | @@ -403,7 +403,7 @@ falsification_tests: prediction: apr validate bad-model.apr exits non-zero ``` -The tree carries 1989 contracts across inference, training, quantization, attention, FFN, +The tree carries 1993 contracts across inference, training, quantization, attention, FFN, tokenization, model formats, CLI safety — and this README itself. ## Migration from old crates diff --git a/contracts/apr-cli-operations-v1.yaml b/contracts/apr-cli-operations-v1.yaml index 71260f0d76..439c3aa6ea 100644 --- a/contracts/apr-cli-operations-v1.yaml +++ b/contracts/apr-cli-operations-v1.yaml @@ -270,6 +270,11 @@ falsification_tests: prediction: print_json and print_reverse_lookup complete on every table and report launches/layer x layers test: commands::ptx_map::tests::print_json_and_reverse_lookup_cover_every_branch if_fails: ptx-map JSON or reverse-lookup output panics or miscounts launches +- id: FALSIFY-OPS-012 + rule: apr run prints every output mode and derives tok/s as documented + prediction: print_run_output succeeds for stream, json, benchmark and text; effective_tok_per_sec prefers the reported rate, else tokens/duration, else 0.0 + test: commands::run::tests::print_run_output_serves_every_mode_and_derives_the_rate + if_fails: apr run output errors on a finished run or reports a wrong rate kani_harnesses: - id: KANI-OPS-001 obligation: ReadOnly commands have no side effects @@ -324,7 +329,7 @@ qa_gate: - progress_reporting - concurrent_model_access - tokenizer_consistency - pass_criteria: All 11 falsification tests pass + pass_criteria: All 12 falsification tests pass falsification: > Run read-only command with filesystem watcher to detect mutations. Force inference error and measure GPU memory leak. diff --git a/contracts/apr-dogfood-coverage-v1.yaml b/contracts/apr-dogfood-coverage-v1.yaml index 9dc6136bb5..afc082013b 100644 --- a/contracts/apr-dogfood-coverage-v1.yaml +++ b/contracts/apr-dogfood-coverage-v1.yaml @@ -3,7 +3,7 @@ metadata: created: '2026-08-22' author: PAIML Engineering references: - - 'docs/audits/surface_audit.csv — 142 of 830 features gated, across 28 binaries and 14 clusters, measured 2026-08-22 @ 4bbfeb07f; 142 of 832 features gated after the PERF-046 partial re-audit (PR #2742); 143 of 833 features gated after the PP-LLAMA-001 re-audit (GET /v1/effective-config added and swept by the dogfood route enumeration, router.rs rows re-pointed); 144 of 837 features gated after PP-066 L0-1b added the three `apr parity` flag rows (--per-op, --out, --threshold), which the dogfood sweep does not reach -- the denominator grew and the numerator did not; 144 of 838 features gated after #3726 added `apr tokenize encode` (the tokenizer-parity gate''s id source), which the dogfood sweep does not reach either; 144 of 839 features gated after ONT-10 S19 ledgered the bare `aprender-cbtop` root surface (interactive TUI / --headless), which the dogfood sweep does not reach; 144 of 851 features gated after ONT-4g (#4476) added the twelve pv/apr command rows the binary snapshot found unledgered, none of them gated; 144 of 853 features gated after the ONT-4g bin gate (surface_audit_bins_gate.sh) found `pv-sat` shipping with no row and its two surfaces were ledgered, neither gated; 144 of 857 features gated after ONT-10 S4 ledgered the 4 hf_* tools `aprender-orchestrate mcp` lists, none of them gated; 144 of 868 features gated after ONT-10 S9/S7 mirrored the eleven ONT-4g pv rows as `apr pv` rows (the apr node joins binary=apr), none of them gated; 144 of 894 features gated once main (with #4219''s 26 ` --version` rows, each run and observed printing its SHA, which the dogfood sweep does not reach) merged into ONT-10''s 868; 144 of 904 features gated after the bin gate found `aprender-ci-tools` (the C301 port of the CI helpers) shipping with no row and its ten surfaces (nine subcommands and --version) were ledgered, none of them gated (#5170); 144 of 906 features gated after #5382 added the `pv ontology readme` and `apr pv ontology readme` rows, ungated; 144 of 907 features gated after #5225 added the `aprender-ci-tools ladder-cells-produce` row, ungated' + - 'docs/audits/surface_audit.csv — 142 of 830 features gated, across 28 binaries and 14 clusters, measured 2026-08-22 @ 4bbfeb07f; 142 of 832 features gated after the PERF-046 partial re-audit (PR #2742); 143 of 833 features gated after the PP-LLAMA-001 re-audit (GET /v1/effective-config added and swept by the dogfood route enumeration, router.rs rows re-pointed); 144 of 837 features gated after PP-066 L0-1b added the three `apr parity` flag rows (--per-op, --out, --threshold), which the dogfood sweep does not reach -- the denominator grew and the numerator did not; 144 of 838 features gated after #3726 added `apr tokenize encode` (the tokenizer-parity gate''s id source), which the dogfood sweep does not reach either; 144 of 839 features gated after ONT-10 S19 ledgered the bare `aprender-cbtop` root surface (interactive TUI / --headless), which the dogfood sweep does not reach; 144 of 851 features gated after ONT-4g (#4476) added the twelve pv/apr command rows the binary snapshot found unledgered, none of them gated; 144 of 853 features gated after the ONT-4g bin gate (surface_audit_bins_gate.sh) found `pv-sat` shipping with no row and its two surfaces were ledgered, neither gated; 144 of 857 features gated after ONT-10 S4 ledgered the 4 hf_* tools `aprender-orchestrate mcp` lists, none of them gated; 144 of 868 features gated after ONT-10 S9/S7 mirrored the eleven ONT-4g pv rows as `apr pv` rows (the apr node joins binary=apr), none of them gated; 144 of 894 features gated once main (with #4219''s 26 ` --version` rows, each run and observed printing its SHA, which the dogfood sweep does not reach) merged into ONT-10''s 868; 144 of 904 features gated after the bin gate found `aprender-ci-tools` (the C301 port of the CI helpers) shipping with no row and its ten surfaces (nine subcommands and --version) were ledgered, none of them gated (#5170); 144 of 906 features gated after #5382 added the `pv ontology readme` and `apr pv ontology readme` rows, ungated; 144 of 907 features gated after #5225 added the `aprender-ci-tools ladder-cells-produce` row, ungated; 144 of 911 features gated after the `sim repo-flow` and `sim course-flow` rows (apr and aprender-simulate, four rows) were ledgered, each run on x86_64, ungated' - 'docs/audits/surface_audit_elbow.png — k-selection evidence: inertia knee and silhouette over k in [2,45]' - 'scripts/dogfood_cluster.py — the k-sweep that produced the elbow plot (k-selection ONLY; it does not write the columns)' - 'scripts/check_no_cluster_id_keys.sh — T1 enforcement: nothing may key on `cluster_id`' @@ -87,9 +87,9 @@ metadata: overall: command: "python3 scripts/dogfood_baseline.py # section: totals" - rows: 907 + rows: 911 covered: 144 - ratio: 0.1588 # 144/907 -- 15.9%, NOT "about 16%" + ratio: 0.1581 # 144/911 -- 15.8%, NOT "about 16%" binaries: 30 binaries_at_zero_coverage: 29 clusters: 14 @@ -104,7 +104,7 @@ metadata: note: > covered may never DECREASE for any binary; total may never decrease without a reconciliation finding recording which direction moved. - apr: {total: 388, covered: 144} + apr: {total: 390, covered: 144} aprender-orchestrate: {total: 189, covered: 0} aprender-test-cli: {total: 40, covered: 0} pv: {total: 50, covered: 0} @@ -114,7 +114,7 @@ metadata: apr-qa: {total: 16, covered: 0} aprender-rag: {total: 14, covered: 0} aprender-train-shell: {total: 14, covered: 0} - aprender-simulate: {total: 13, covered: 0} + aprender-simulate: {total: 15, covered: 0} aprender-verify: {total: 12, covered: 0} aprender-explain: {total: 8, covered: 0} aprender-present: {total: 8, covered: 0} @@ -182,7 +182,7 @@ metadata: profiling: {total: 46, covered: 1} # 2.2% of cluster, 0.7% of gate effort rag-eval: {total: 46, covered: 0} # ZERO qa-cgp: {total: 38, covered: 0} # ZERO - simulation: {total: 19, covered: 0} # ZERO + simulation: {total: 23, covered: 0} # ZERO orchestrate-pacha-secrets: {total: 17, covered: 0} # ZERO per_band: @@ -195,7 +195,7 @@ metadata: the 4.3% coverage of that band is why. q1_2: {total: 80, covered: 58} # 72.5% q3_4: {total: 49, covered: 27} # 55.1% - q5_6: {total: 719, covered: 29} # 4.1% + q5_6: {total: 723, covered: 29} # 4.1% q7_8: {total: 38, covered: 10} # 26.3% q9_10: {total: 21, covered: 20} # 95.2% @@ -306,7 +306,7 @@ equations: codomain: bool invariants: - "T2. Cluster coverage is a PROXY: one gate in a 95-member cluster is 1%, not covered" - - "5/14 clusters (35.7%) and 144/907 features (15.9%) are reported together, always" + - "5/14 clusters (35.7%) and 144/911 features (15.8%) are reported together, always" - "Enforced mechanically by enforce_pairing(); deleting the feature fraction from the emitter turns the gate RED" - "This is the single most important trap: reporting the proxy alone is how a coverage gate becomes theatre while looking stricter" @@ -695,7 +695,7 @@ falsification_tests: Every emitted line stating a CLUSTER-level ratio also states the underlying FEATURE-level ratio, on EVERY channel one can be emitted through: this gate's report, the receipt, scripts/dogfood_baseline.py and - .claude/skills/apr-dogfood/SKILL.md. 5 of 14 clusters (35.7%) is a proxy and 144 of 907 features (15.9%) is the thing. + .claude/skills/apr-dogfood/SKILL.md. 5 of 14 clusters (35.7%) is a proxy and 144 of 911 features (15.8%) is the thing. One gate in a 95-member cluster is 1%. The rule keys on the NUMBER -- a denominator equal to the cluster count -- not on a phrase, because a phrase can be reworded and a denominator cannot; diff --git a/contracts/aprender-registry-download-progress-v1.yaml b/contracts/aprender-registry-download-progress-v1.yaml new file mode 100644 index 0000000000..eed1fe371a --- /dev/null +++ b/contracts/aprender-registry-download-progress-v1.yaml @@ -0,0 +1,47 @@ +metadata: + id: C-REGISTRY-DOWNLOAD-PROGRESS + version: 1.0.0 + created: '2026-10-18' + author: PAIML Engineering + kind: pattern + status: ACTIVE_ALGORITHM_LEVEL + description: | + Pins the human-readable accessors of aprender-registry's DownloadProgress: + eta_human formats seconds, minutes and hours; downloaded_human reads the + downloaded byte count and total_human reads the total, never each other's. + references: + - 'crates/aprender-registry/src/cache.rs (DownloadProgress::eta_human, downloaded_human, total_human)' + +equations: + progress_human_accessors: + formula: | + eta_human = format_duration(eta_secs); downloaded_human = format_bytes(downloaded_bytes); + total_human = format_bytes(total_bytes) + domain: DownloadProgress values + invariants: + - 'downloaded_human depends only on downloaded_bytes; total_human only on total_bytes' + +proof_obligations: +- id: RDP-INV-001 + type: invariant + property: each human accessor reads its own field + formal: "∀ t ∈ {progress_human_tests}: exit(t) = 0" + applies_to: progress_human_accessors + +falsification_tests: +- id: FALSIFY-REGISTRY-DOWNLOAD-PROGRESS-001 + rule: eta_human, downloaded_human and total_human render their own fields + prediction: 'eta 42.9/125/3725 s -> "42s"/"2m 5s"/"1h 2m"; 1536 B downloaded -> "1.50 KB"; 5 MiB total -> "5.00 MB"' + test: cargo test -p aprender-registry --lib cache::progress_human_tests + if_fails: progress lines show the wrong size or ETA to users during model pulls + ship_blocking: false + mutation: 'make downloaded_human format total_bytes; must turn RED' + +qa_gate: + id: QA-REGISTRY-DOWNLOAD-PROGRESS-001 + name: Registry download progress accessors gate + description: human-readable accessors read their own fields + checks: + - progress_human_accessors + pass_criteria: FALSIFY-REGISTRY-DOWNLOAD-PROGRESS-001 passes + falsification: Any failure fails the gate diff --git a/contracts/contracts.nt b/contracts/contracts.nt index aef57b58ef..70db0aa4b0 100644 --- a/contracts/contracts.nt +++ b/contracts/contracts.nt @@ -334,11 +334,13 @@ "apr shard"^^ . "apr shared-cache-lint"^^ . "apr showcase"^^ . + "apr sim course-flow"^^ . "apr sim emc-check"^^ . "apr sim emc-validate"^^ . "apr sim help"^^ . "apr sim list-emc"^^ . "apr sim render"^^ . + "apr sim repo-flow"^^ . "apr sim run"^^ . "apr sim validate"^^ . "apr sim verify"^^ . @@ -675,6 +677,8 @@ "rag eval metrics"^^ . "rag eval retrieve"^^ . "rag eval sample"^^ . + "sim course-flow"^^ . + "sim repo-flow"^^ . "POST /v1/logprobs"^^ . "POST /v1/perplexity"^^ . "apr.bench"^^ . @@ -1734,11 +1738,13 @@ . . "aprender-simulate --version"^^ . + "aprender-simulate course-flow"^^ . "aprender-simulate emc-check"^^ . "aprender-simulate emc-validate"^^ . "aprender-simulate help"^^ . "aprender-simulate list-emc"^^ . "aprender-simulate render"^^ . + "aprender-simulate repo-flow"^^ . "aprender-simulate run"^^ . "aprender-simulate validate"^^ . "aprender-simulate verify"^^ . @@ -1757,6 +1763,8 @@ "version"^^ . "47d198202ff793c91cb790beba358f531505cb51"^^ . "adaaa5979da2b555e584a1ca8e918e8c4859c1bab12c89c3924044a1a002f0ee"^^ . + "course-flow"^^ . + "repo-flow"^^ . "aprender-simulate"^^ . "aprender-simulate"^^ . "1d57fceab026705fbcb61e62721b0cbdc4299277f2e4cfd76340981781ccb241"^^ . @@ -2385,11 +2393,13 @@ "apr shard"^^ . "apr shared-cache-lint"^^ . "apr showcase"^^ . + "apr sim course-flow"^^ . "apr sim emc-check"^^ . "apr sim emc-validate"^^ . "apr sim help"^^ . "apr sim list-emc"^^ . "apr sim render"^^ . + "apr sim repo-flow"^^ . "apr sim run"^^ . "apr sim validate"^^ . "apr sim verify"^^ . @@ -2726,6 +2736,8 @@ "rag eval metrics"^^ . "rag eval retrieve"^^ . "rag eval sample"^^ . + "sim course-flow"^^ . + "sim repo-flow"^^ . "POST /v1/logprobs"^^ . "POST /v1/perplexity"^^ . "apr.bench"^^ . @@ -8691,6 +8703,11 @@ . "contracts/apr-zero-feature-gate-v1.yaml"^^ . "apr-zero-feature-gate-v1"^^ . + . + . + "contracts/aprender-registry-download-progress-v1.yaml"^^ . + "aprender-registry-download-progress-v1"^^ . + "pattern"^^ . . . . @@ -13029,6 +13046,11 @@ . "contracts/preprocessing-normalization-v1.yaml"^^ . "preprocessing-normalization-v1"^^ . + . + . + "contracts/present-widgets-data-card-paint-v1.yaml"^^ . + "present-widgets-data-card-paint-v1"^^ . + "pattern"^^ . . . "contracts/present-yaml-expression-executor-v1.yaml"^^ . @@ -13746,6 +13768,11 @@ "simd-scalar-parity-v1"^^ . "simd-scalar-parity"^^ . "1.0.0"^^ . + . + . + "contracts/simulate-edd-verification-tests-v1.yaml"^^ . + "simulate-edd-verification-tests-v1"^^ . + "pattern"^^ . . . . @@ -14018,6 +14045,11 @@ "tracing-observability-v1"^^ . "tracing-observability"^^ . "1.0.0"^^ . + . + . + "contracts/train-loader-try-load-apr-v1.yaml"^^ . + "train-loader-try-load-apr-v1"^^ . + "pattern"^^ . . . . diff --git a/contracts/present-widgets-data-card-paint-v1.yaml b/contracts/present-widgets-data-card-paint-v1.yaml new file mode 100644 index 0000000000..9fdb3803f1 --- /dev/null +++ b/contracts/present-widgets-data-card-paint-v1.yaml @@ -0,0 +1,43 @@ +metadata: + version: 1.0.0 + created: '2026-10-18' + author: PAIML Engineering + description: "DataCard paint — the widget draws chrome, title, version line, optional description and stats, a schema preview capped at four columns and at most five tag chips, in a fixed order." + kind: pattern + references: + - "aprender#5538 — coverage-gap ticket for DataCard::paint" + - "crates/aprender-present-widgets/src/data_card.rs — paint and the paint_* tests" + +equations: + data_card_paint_caps_and_order: + formula: "paint emits texts [quality, name, version-line] first; schema rows <= 4 then '... +N more'; tag chips <= 5" + domain: "a DataCard painted onto a recording Canvas" + codomain: "the ordered list of draw_text strings and the fill_rect count" + invariants: + - "A set format is joined into the version line; an unset one leaves the bare version" + - "An unset stat (rows, columns, size) draws neither its label nor its value" + - "Schema is hidden when show_schema is false or the schema is empty" + +proof_obligations: + - id: PWDC-INV-001 + type: invariant + property: "Schema preview shows at most 4 columns plus a '+N more' marker" + formal: "∀ t ∈ {paint_schema_truncates_to_four_columns_with_more_marker}: exit(t) = 0" + applies_to: data_card_paint_caps_and_order + - id: PWDC-INV-002 + type: invariant + property: "At most 5 tag chips are drawn" + formal: "∀ t ∈ {paint_draws_at_most_five_tag_chips}: exit(t) = 0" + applies_to: data_card_paint_caps_and_order + +falsification_tests: + - id: FALSIFY-PWDC-001 + rule: "schema cap raised" + prediction: "changing take(4) to take(5) turns the schema truncation test RED" + test: "cargo test -p aprender-present-widgets --lib paint_schema_truncates_to_four_columns_with_more_marker" + if_fails: "the schema preview cap is not enforced by any test" + - id: FALSIFY-PWDC-002 + rule: "tag cap raised" + prediction: "changing take(5) to take(6) turns the tag chip test RED" + test: "cargo test -p aprender-present-widgets --lib paint_draws_at_most_five_tag_chips" + if_fails: "the tag chip cap is not enforced by any test" diff --git a/contracts/simulate-edd-verification-tests-v1.yaml b/contracts/simulate-edd-verification-tests-v1.yaml new file mode 100644 index 0000000000..a264bc7cf7 --- /dev/null +++ b/contracts/simulate-edd-verification-tests-v1.yaml @@ -0,0 +1,38 @@ +metadata: + version: 1.0.0 + created: '2026-10-18' + author: PAIML Engineering + description: "EDD-07 — EddValidator::validate_verification_tests reports each failing EMC verification test as a critical EDD-07 violation, passes silently when all hold, and records failures in the validator." + kind: pattern + references: + - "crates/aprender-simulate/src/edd/validation.rs — validate_verification_tests and its tests" + - "docs/findings/aprender-w5032.jsonl — coverage-gaps ranking that selected this function" + +equations: + edd07_reports_exactly_the_failing_tests: + formula: "errors == { t in emc.tests : |eval(t.inputs) - t.expected| > t.tolerance }, each code EDD-07 and severity Critical; validator.violations grows by |errors|" + domain: "an EquationModelCard with >= 1 verification test and an evaluator closure" + codomain: "Result<(), Vec>" + invariants: + - "A passing run leaves the validator's violations untouched" + - "A failing run appends to, never replaces, earlier violations" + - "The violation context carries the FAIL line with expected, actual and tolerance" + +proof_obligations: + - id: SEV-INV-001 + type: invariant + property: "Only failing tests are reported, as EDD-07 Critical with FAIL context" + formal: "∀ t ∈ {test_validate_verification_tests_failure_is_edd07_critical_with_context}: exit(t) = 0" + applies_to: edd07_reports_exactly_the_failing_tests + - id: SEV-INV-002 + type: invariant + property: "Failures accumulate in the validator across runs" + formal: "∀ t ∈ {test_validate_verification_tests_failures_accumulate_in_validator}: exit(t) = 0" + applies_to: edd07_reports_exactly_the_failing_tests + +falsification_tests: + - id: FALSIFY-SEV-001 + rule: "failures not recorded" + prediction: "deleting the self.violations.extend call turns the accumulate test RED" + test: "cargo test -p aprender-simulate --lib test_validate_verification_tests_failures_accumulate_in_validator" + if_fails: "a failed verification leaves no trace in the validator" diff --git a/contracts/train-loader-try-load-apr-v1.yaml b/contracts/train-loader-try-load-apr-v1.yaml new file mode 100644 index 0000000000..5d2025f91c --- /dev/null +++ b/contracts/train-loader-try-load-apr-v1.yaml @@ -0,0 +1,36 @@ +metadata: + version: 1.0.0 + created: '2026-10-18' + author: PAIML Engineering + description: "config::train::loader try_load_apr — loading a transformer from an APR file or checkpoint directory: unreadable or absent input is None, the checkpoint step comes from the checkpoint_step metadata and otherwise from the model-step-N file name, a directory resolves to its newest step, and the weights round-trip." + kind: pattern + references: + - "crates/aprender-train/src/config/train/loader/data.rs — try_load_apr, try_load_apr_for_inference, find_latest_apr_checkpoint" + +equations: + try_load_apr_step_and_weights: + formula: "step == metadata.checkpoint_step if present else parse(file name model-step-N.apr) else 0; a directory picks max N; absent, corrupt or empty-dir input yields None" + domain: "a path (APR file or directory) and a TransformerConfig" + codomain: "Option<(Option, usize)>" + invariants: + - "Metadata step takes precedence over the file-name step" + - "Loaded embedding weights equal the saved ones" + +proof_obligations: + - id: TLA-INV-001 + type: invariant + property: "Metadata checkpoint_step wins over the file-name step" + formal: "∀ t ∈ {test_try_load_apr_reads_step_from_metadata_over_filename}: exit(t) = 0" + applies_to: try_load_apr_step_and_weights + - id: TLA-INV-002 + type: invariant + property: "A directory resolves to its newest model-step-N.apr" + formal: "∀ t ∈ {test_try_load_apr_directory_picks_latest_step_from_filename}: exit(t) = 0" + applies_to: try_load_apr_step_and_weights + +falsification_tests: + - id: FALSIFY-TLA-001 + rule: "metadata key ignored" + prediction: "reading a different metadata key makes the step fall back to the file name and turns the metadata test RED" + test: "cargo test -p aprender-train --lib test_try_load_apr_reads_step_from_metadata_over_filename" + if_fails: "the checkpoint_step metadata path is unguarded" diff --git a/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json b/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json index cd19ad1c52..b6e4620fa7 100644 --- a/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json +++ b/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json @@ -1,5 +1,5 @@ { - "census_id_set_sha256": "d3dfda18ea6caa1dfb2920d1803d8ddea6534bb557f22bed7db5e2a8c0bc2619", + "census_id_set_sha256": "c9013292ce5d9aa45045302bf73eb8bb217b4fb272cd819d55c36157b94fa942", "relations_sha256": "811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850", "checkable_n": 87, "result": { diff --git a/crates/apr-cli/src/commands/run_tests_accel_reconcile.rs b/crates/apr-cli/src/commands/run_tests_accel_reconcile.rs index 2ccb78c6d0..c600a482eb 100644 --- a/crates/apr-cli/src/commands/run_tests_accel_reconcile.rs +++ b/crates/apr-cli/src/commands/run_tests_accel_reconcile.rs @@ -423,3 +423,31 @@ mod pmat3826_fell_back_names_a_real_fallback { ); } } + +/// FALSIFY-OPS-012: every output mode of `print_run_output` completes on a +/// finished run, and the rate it reports is derived exactly as documented. +#[test] +fn print_run_output_serves_every_mode_and_derives_the_rate() { + let mut r = gpu_result(Some(true)); + // stream, json, benchmark (text and json), plain text (cached, then downloaded) + for (fmt, bench, stream) in [ + ("text", false, true), + ("json", false, false), + ("text", true, false), + ("json", true, false), + ("text", false, false), + ] { + assert!(print_run_output(&r, "model.gguf", fmt, 8, bench, stream, false).is_ok()); + } + r.cached = false; + assert!(print_run_output(&r, "model.gguf", "text", 8, false, false, true).is_ok()); + + // reported rate wins; otherwise tokens / duration; zero duration gives 0.0 + r.tok_per_sec = Some(7.5); + assert!((effective_tok_per_sec(&r, 4) - 7.5).abs() < f64::EPSILON); + r.tok_per_sec = None; + r.duration_secs = 2.0; + assert!((effective_tok_per_sec(&r, 4) - 2.0).abs() < f64::EPSILON); + r.duration_secs = 0.0; + assert!(effective_tok_per_sec(&r, 4).abs() < f64::EPSILON); +} diff --git a/crates/aprender-present-widgets/src/data_card.rs b/crates/aprender-present-widgets/src/data_card.rs index 9942bef57d..0140192f5c 100644 --- a/crates/aprender-present-widgets/src/data_card.rs +++ b/crates/aprender-present-widgets/src/data_card.rs @@ -1501,4 +1501,110 @@ mod tests { let card = DataCard::default(); assert_eq!(card.background, Color::WHITE); } + + // ===== paint (Refs #5538) ===== + + #[derive(Default)] + struct Rec { + texts: Vec, + fills: usize, + strokes: usize, + } + + impl Canvas for Rec { + fn fill_rect(&mut self, _r: Rect, _c: Color) { + self.fills += 1; + } + fn stroke_rect(&mut self, _r: Rect, _c: Color, _w: f32) { + self.strokes += 1; + } + fn draw_text(&mut self, t: &str, _p: Point, _s: &TextStyle) { + self.texts.push(t.to_string()); + } + fn draw_line(&mut self, _a: Point, _b: Point, _c: Color, _w: f32) {} + fn fill_circle(&mut self, _c: Point, _r: f32, _col: Color) {} + fn stroke_circle(&mut self, _c: Point, _r: f32, _col: Color, _w: f32) {} + fn fill_arc(&mut self, _c: Point, _r: f32, _a: f32, _b: f32, _col: Color) {} + fn draw_path(&mut self, _p: &[Point], _c: Color, _w: f32) {} + fn fill_polygon(&mut self, _p: &[Point], _c: Color) {} + fn push_clip(&mut self, _r: Rect) {} + fn pop_clip(&mut self) {} + fn push_transform(&mut self, _t: presentar_core::Transform2D) {} + fn pop_transform(&mut self) {} + } + + fn painted(card: &DataCard) -> Rec { + let mut rec = Rec::default(); + card.paint(&mut rec); + rec + } + + #[test] + fn paint_minimal_card_draws_chrome_title_and_bare_version() { + let rec = painted(&DataCard::new("plain")); + assert_eq!(rec.fills, 1 + 1, "background + quality badge"); + assert_eq!(rec.strokes, 1); + assert_eq!(rec.texts, ["Unknown", "plain", "v1.0.0"]); + } + + #[test] + fn paint_version_line_includes_format_when_set() { + let rec = painted(&DataCard::new("d").format("Parquet")); + assert!(rec.texts.contains(&"v1.0.0 • Parquet".to_string())); + } + + #[test] + fn paint_draws_description_stats_labels_and_values_in_order() { + let card = DataCard::new("d").description("about").stats( + DataStats::new() + .rows(2_500) + .columns(7) + .size_bytes(3_000_000), + ); + let t = painted(&card).texts; + assert_eq!( + t[3..], + [ + "about", + "Rows", + "2.5K rows", + "Columns", + "7", + "Size", + "3.0 MB" + ] + ); + } + + #[test] + fn paint_skips_stat_blocks_that_are_unset() { + let t = painted(&DataCard::new("d").stats(DataStats::new().columns(3))).texts; + assert_eq!(t[3..], ["Columns", "3"]); + } + + #[test] + fn paint_schema_truncates_to_four_columns_with_more_marker() { + let cols = (0..6).map(|i| DataColumn::new(format!("c{i}"), "int")); + let t = painted(&DataCard::new("d").columns(cols)).texts; + assert_eq!(t[3], "Schema:"); + assert_eq!(t[4..8], ["c0: int", "c1: int", "c2: int", "c3: int"]); + assert_eq!(t[8], "... +2 more"); + assert_eq!(t.len(), 9); + } + + #[test] + fn paint_schema_hidden_when_show_schema_false_or_empty() { + let col = DataColumn::new("id", "int"); + let hidden = painted(&DataCard::new("d").column(col).show_schema(false)); + assert!(!hidden.texts.iter().any(|t| t == "Schema:")); + let empty = painted(&DataCard::new("d")); + assert!(!empty.texts.iter().any(|t| t == "Schema:")); + } + + #[test] + fn paint_draws_at_most_five_tag_chips() { + let rec = painted(&DataCard::new("d").tags(["a", "b", "c", "d", "e", "f", "g"])); + assert_eq!(rec.fills, 2 + 5, "chrome fills + one chip per shown tag"); + assert_eq!(rec.texts[3..], ["a", "b", "c", "d", "e"]); + } } diff --git a/crates/aprender-registry/src/cache.rs b/crates/aprender-registry/src/cache.rs index e48a1cdb0c..f8c13a812f 100644 --- a/crates/aprender-registry/src/cache.rs +++ b/crates/aprender-registry/src/cache.rs @@ -1081,3 +1081,34 @@ mod tests { assert_eq!(parsed, EvictionPolicy::LRU); } } + +#[cfg(test)] +mod progress_human_tests { + use super::*; + + fn progress(total: u64, downloaded: u64, eta_secs: f64) -> DownloadProgress { + let mut p = DownloadProgress::new(total); + p.downloaded_bytes = downloaded; + p.eta_secs = eta_secs; + p + } + + #[test] + fn eta_human_formats_seconds_minutes_and_hours() { + assert_eq!(progress(1, 0, 42.9).eta_human(), "42s"); + assert_eq!(progress(1, 0, 125.0).eta_human(), "2m 5s"); + assert_eq!(progress(1, 0, 3725.0).eta_human(), "1h 2m"); + } + + #[test] + fn downloaded_human_reads_downloaded_not_total() { + let p = progress(5 * 1024 * 1024, 1536, 0.0); + assert_eq!(p.downloaded_human(), "1.50 KB"); + } + + #[test] + fn total_human_reads_total_not_downloaded() { + let p = progress(5 * 1024 * 1024, 1536, 0.0); + assert_eq!(p.total_human(), "5.00 MB"); + } +} diff --git a/crates/aprender-simulate/src/cli/args.rs b/crates/aprender-simulate/src/cli/args.rs index 014e33985a..42165e85dd 100644 --- a/crates/aprender-simulate/src/cli/args.rs +++ b/crates/aprender-simulate/src/cli/args.rs @@ -165,7 +165,7 @@ pub enum Commands { #[arg(long, default_value = "unknown")] sha: String, }, - /// Run a FLOW-006 repo case (conflict step, optional merge queue); --json prints the sim block + /// Run a FLOW-006 repo case (conflict step, optional merge queue) RepoFlow { /// Case name, for example rmedia-design or infra-rule. #[arg(long)] @@ -177,7 +177,7 @@ pub enum Commands { #[arg(long)] json: bool, }, - /// Run a FLOW-006 course-factory case; --json prints the sim block + /// Run a FLOW-006 course-factory case CourseFlow { /// Case: cal-today, design, nine-builders, coursera-24h or render-300. #[arg(long)] diff --git a/crates/aprender-simulate/src/edd/validation.rs b/crates/aprender-simulate/src/edd/validation.rs index b07d563e75..75ccb103d5 100644 --- a/crates/aprender-simulate/src/edd/validation.rs +++ b/crates/aprender-simulate/src/edd/validation.rs @@ -1559,4 +1559,54 @@ mod tests { let result_loose = richardson_extrapolation(&values, 2.0, 2.5, 1.0); assert!(result_loose.order_matches); } + + fn emc_with_tests(tests: &[(&str, f64, f64)]) -> EquationModelCard { + let mut b = EmcBuilder::new() + .name("Test") + .equation("x = y") + .citation(Citation::new(&["Test"], "Test", 2024)); + for (d, e, t) in tests { + b = b.add_verification_test(*d, *e, *t); + } + b.build().ok().unwrap() + } + + #[test] + fn test_validate_verification_tests_all_pass_records_nothing() { + let mut v = EddValidator::new(); + let emc = emc_with_tests(&[("a", 1.0, 0.1), ("b", 1.0, 0.5)]); + assert!(v.validate_verification_tests(&emc, |_| 1.05).is_ok()); + assert!(v.violations().is_empty()); + } + + #[test] + fn test_validate_verification_tests_failure_is_edd07_critical_with_context() { + let mut v = EddValidator::new(); + let emc = emc_with_tests(&[("good", 1.0, 0.1), ("bad", 5.0, 0.1)]); + let errs = v.validate_verification_tests(&emc, |_| 1.0).err().unwrap(); + assert_eq!(errs.len(), 1, "only the failing test is reported"); + assert_eq!(errs[0].code, "EDD-07"); + assert_eq!(errs[0].severity, ViolationSeverity::Critical); + assert!(errs[0].message.contains("Verification test failed: bad")); + assert!(errs[0] + .context + .as_deref() + .unwrap_or("") + .contains("FAIL: bad")); + } + + #[test] + fn test_validate_verification_tests_failures_accumulate_in_validator() { + let mut v = EddValidator::new(); + let emc = emc_with_tests(&[("x", 9.0, 0.1), ("y", 8.0, 0.1)]); + let errs = v.validate_verification_tests(&emc, |_| 0.0).err().unwrap(); + assert_eq!(errs.len(), 2); + assert_eq!(v.violations().len(), 2); + let _ = v.validate_verification_tests(&emc, |_| 0.0); + assert_eq!( + v.violations().len(), + 4, + "a second run appends, not replaces" + ); + } } diff --git a/crates/aprender-train/src/config/train/loader/tests.rs b/crates/aprender-train/src/config/train/loader/tests.rs index f67d7eea2b..16bb6d52a1 100644 --- a/crates/aprender-train/src/config/train/loader/tests.rs +++ b/crates/aprender-train/src/config/train/loader/tests.rs @@ -2096,3 +2096,78 @@ fn test_tabular_shapes_name_the_offending_batch_index() { let err = validate_tabular_batch_shapes(&batches, 8).expect_err("batch 2 must be rejected"); assert!(err.to_string().contains("batch 2"), "error must name the batch: {err}"); } + +// ── try_load_apr (via try_load_apr_for_inference) ──────────────────────── + +/// Write `model` as an APR file at `path` with the given extra metadata. +fn write_tiny_apr(path: &std::path::Path, model: &Transformer, meta: &[(&str, &str)]) { + use aprender::serialization::apr::AprWriter; + let mut w = AprWriter::new(); + for (k, v) in meta { + w.set_metadata(k.to_string(), serde_json::json!(v)); + } + for (name, t) in model.named_parameters() { + let data = t.data(); + w.add_tensor_f32(name, vec![data.len()], data.as_slice().expect("contiguous")); + } + w.write(path).expect("write apr"); +} + +#[test] +fn test_try_load_apr_rejects_missing_path_and_corrupt_file() { + let cfg = TransformerConfig::tiny(); + let dir = tempfile::tempdir().expect("tempdir"); + assert!(try_load_apr_for_inference(&dir.path().join("absent.apr"), &cfg).is_none()); + let bad = dir.path().join("bad.apr"); + std::fs::write(&bad, b"not an apr file").expect("write"); + assert!(try_load_apr_for_inference(&bad, &cfg).is_none()); + // Empty directory: no checkpoint to pick. + assert!(try_load_apr_for_inference(dir.path(), &cfg).is_none()); +} + +#[test] +fn test_try_load_apr_reads_step_from_metadata_over_filename() { + let cfg = TransformerConfig::tiny(); + let model = Transformer::new(&cfg); + let dir = tempfile::tempdir().expect("tempdir"); + let p = dir.path().join("model-step-5.apr"); + write_tiny_apr(&p, &model, &[("checkpoint_step", "42")]); + let (loaded, step) = try_load_apr_for_inference(&p, &cfg).expect("loads"); + assert_eq!(step, 42, "metadata step wins over filename step"); + assert_eq!(loaded.expect("model").named_parameters().len(), model.named_parameters().len()); +} + +#[test] +fn test_try_load_apr_directory_picks_latest_step_from_filename() { + let cfg = TransformerConfig::tiny(); + let model = Transformer::new(&cfg); + let dir = tempfile::tempdir().expect("tempdir"); + write_tiny_apr(&dir.path().join("model-step-3.apr"), &model, &[]); + write_tiny_apr(&dir.path().join("model-step-12.apr"), &model, &[]); + let (_, step) = try_load_apr_for_inference(dir.path(), &cfg).expect("loads"); + assert_eq!(step, 12, "no metadata: step parsed from the newest file name"); +} + +#[test] +fn test_try_load_apr_round_trips_weights_with_training_tensor_present() { + let cfg = TransformerConfig::tiny(); + let model = Transformer::new(&cfg); + let dir = tempfile::tempdir().expect("tempdir"); + let p = dir.path().join("model.apr"); + { + use aprender::serialization::apr::AprWriter; + let mut w = AprWriter::new(); + for (name, t) in model.named_parameters() { + let d = t.data(); + w.add_tensor_f32(name, vec![d.len()], d.as_slice().expect("contiguous")); + } + w.add_tensor_f32("__training__.opt_state", vec![2], &[1.0, 2.0]); + w.write(&p).expect("write"); + } + let (loaded, step) = try_load_apr_for_inference(&p, &cfg).expect("loads"); + assert_eq!(step, 0, "model.apr carries no step"); + let loaded = loaded.expect("model"); + let a = model.embed_tokens.weight.data(); + let b = loaded.embed_tokens.weight.data(); + assert_eq!(a.as_slice(), b.as_slice(), "embedding weights round-trip"); +} diff --git a/docs/audits/surface_audit.csv b/docs/audits/surface_audit.csv index 122777439b..0a25cff4e4 100644 --- a/docs/audits/surface_audit.csv +++ b/docs/audits/surface_audit.csv @@ -416,11 +416,13 @@ apr,apr serve run --no-metrics,4,x86_64-linux;nvidia-cuda,llama.cpp,no,10,apr-co apr,apr shard,6,x86_64-linux,llama.cpp,yes,1,apr-lint-diag,crates/apr-cli/src/extended_commands.rs:1239,high apr,apr shared-cache-lint,1,x86_64-linux,NONE,yes,1,apr-lint-diag,crates/apr-cli/src/extended_commands.rs:1217,high apr,apr showcase,6,x86_64-linux,NONE,yes,10,apr-core-commands,crates/apr-cli/src/tool_commands.rs:5,high +apr,apr sim course-flow,6,x86_64-linux,NONE,no,11,simulation,crates/aprender-simulate/src/cli/args.rs:181,high apr,apr sim emc-check,6,x86_64-linux,NONE,no,11,simulation,crates/aprender-simulate/src/cli/args.rs:206,low apr,apr sim emc-validate,6,x86_64-linux,NONE,no,11,simulation,crates/aprender-simulate/src/cli/args.rs:211,low apr,apr sim help,6,x86_64-linux,NONE,no,11,simulation,crates/aprender-simulate/src/cli/args.rs:218,low apr,apr sim list-emc,6,x86_64-linux,NONE,no,11,simulation,crates/aprender-simulate/src/cli/args.rs:216,low apr,apr sim render,6,x86_64-linux,NONE,no,11,simulation,crates/aprender-simulate/src/cli/args.rs:79,low +apr,apr sim repo-flow,6,x86_64-linux,NONE,no,11,simulation,crates/aprender-simulate/src/cli/args.rs:169,high apr,apr sim run,6,x86_64-linux,NONE,no,11,simulation,crates/aprender-simulate/src/cli/args.rs:68,low apr,apr sim validate,6,x86_64-linux,NONE,no,11,simulation,crates/aprender-simulate/src/cli/args.rs:193,low apr,apr sim verify,6,x86_64-linux,NONE,no,11,simulation,crates/aprender-simulate/src/cli/args.rs:198,low @@ -832,11 +834,13 @@ aprender-score,aprender-score [PATH] (TUI-crate quality scoring),6,UNKNOWN,NONE, aprender-simulate,unserved: GET / (visualization UI; library feature web; no aprender-simulate command starts the server),6,UNKNOWN,NONE,no,0,entrypoint-and-mcp,crates/aprender-simulate/src/visualization/web.rs:88,medium aprender-simulate,unserved: GET /health (visualization; library feature web; no aprender-simulate command starts the server),6,UNKNOWN,NONE,no,0,entrypoint-and-mcp,crates/aprender-simulate/src/visualization/web.rs:89,medium aprender-simulate,unserved: GET /ws (visualization WebSocket; library feature web; no aprender-simulate command starts the server),6,UNKNOWN,NONE,no,0,entrypoint-and-mcp,crates/aprender-simulate/src/visualization/web.rs:82,medium +aprender-simulate,aprender-simulate course-flow,6,x86_64-linux,NONE,no,11,simulation,crates/aprender-simulate/src/cli/args.rs:181,high aprender-simulate,aprender-simulate emc-check,6,UNKNOWN,NONE,no,11,simulation,crates/aprender-simulate/src/cli/args.rs:206,high aprender-simulate,aprender-simulate emc-validate,6,UNKNOWN,NONE,no,11,simulation,crates/aprender-simulate/src/cli/args.rs:211,high aprender-simulate,aprender-simulate help,6,UNKNOWN,NONE,no,11,simulation,crates/aprender-simulate/src/cli/args.rs:218,high aprender-simulate,aprender-simulate list-emc,6,UNKNOWN,NONE,no,11,simulation,crates/aprender-simulate/src/cli/args.rs:216,high aprender-simulate,aprender-simulate render,6,UNKNOWN,NONE,no,11,simulation,crates/aprender-simulate/src/cli/args.rs:79,high +aprender-simulate,aprender-simulate repo-flow,6,x86_64-linux,NONE,no,11,simulation,crates/aprender-simulate/src/cli/args.rs:169,high aprender-simulate,aprender-simulate run,6,UNKNOWN,NONE,no,11,simulation,crates/aprender-simulate/src/cli/args.rs:68,high aprender-simulate,aprender-simulate validate,6,UNKNOWN,NONE,no,11,simulation,crates/aprender-simulate/src/cli/args.rs:193,high aprender-simulate,aprender-simulate verify,6,UNKNOWN,NONE,no,11,simulation,crates/aprender-simulate/src/cli/args.rs:198,high diff --git a/docs/findings/aprender-w5404.jsonl b/docs/findings/aprender-w5404.jsonl index a8f210dfab..4f836d98a3 100644 --- a/docs/findings/aprender-w5404.jsonl +++ b/docs/findings/aprender-w5404.jsonl @@ -1 +1,2 @@ +{"session":"aprender-w5404","ref":"cov-run-output","note":"pmat ticket not minted (needs GH issue); tests for run print_run_output/effective_tok_per_sec, FALSIFY-OPS-013"} {"session":"aprender-w5404","ref":"cov-ptx-map","note":"pmat ticket not minted: pmat work add requires a GitHub issue and new issues are barred; tests for ptx_map print_json/print_reverse_lookup, FALSIFY-OPS-011"} diff --git a/docs/findings/w5382.jsonl b/docs/findings/w5382.jsonl index 5a5a93f9fd..e9c4ba6ab5 100644 --- a/docs/findings/w5382.jsonl +++ b/docs/findings/w5382.jsonl @@ -1,3 +1,4 @@ {"id":"FND-20261018-compute-inplace-unreferenced","title":"aprender-compute pub fns with a single reference (their definition): blocking_8x48, packed_a/b_size_v2, with_reserve, get_checksums","evidence":"grep -rw over crates/aprender-compute/{src,tests,benches,examples} finds exactly one hit each; pmat --coverage-gaps timed out without cached llvm-cov","repro":"grep -rwn packed_a_size_v2 crates/aprender-compute","suspected_epic":"unknown","severity":"P3","found_at_sha":"e00034704047bc22f843f7b512f34d3524a0a403"} {"id":"FND-20261018-ruchy-sessions-dark","title":"ecosystem::ruchy tests only run with feature ruchy-sessions, which default CI does not enable","evidence":"cargo test -p aprender-train --lib test_session_metrics runs 0 tests by default (7654 filtered); 7 with --features ruchy-sessions; mod gated at crates/aprender-train/src/ecosystem/mod.rs:16","repro":"cargo test -p aprender-train --lib test_session_metrics","suspected_epic":"unknown","severity":"P3","found_at_sha":"e00034704047bc22f843f7b512f34d3524a0a403"} +{"id":"FND-20261018-registry-progress-human-untested","session":"w5382","kind":"coverage-gap","where":"crates/aprender-registry/src/cache.rs:DownloadProgress::{eta_human,downloaded_human,total_human}","note":"human-readable accessors had no tests; 3 tests + new contract C-REGISTRY-DOWNLOAD-PROGRESS; mutation (downloaded_human reads total) RED->restored."} {"id":"FND-20261018-apr-cli-from-pairs-untested","session":"w5382","kind":"coverage-gap","where":"crates/apr-cli/src/commands/hang_trace_classifier.rs:TraceDirListing::from_pairs","note":"public constructor had no direct test; the module tests build listings by hand, so from_pairs pairing was unexercised. Covered by 3 tests + FALSIFY-CRUX-F-14-004; mutation (reverse sizes) RED."} diff --git a/docs/proposals/contracts-nt-regen-at-merge.md b/docs/proposals/contracts-nt-regen-at-merge.md new file mode 100644 index 0000000000..ce7162971e --- /dev/null +++ b/docs/proposals/contracts-nt-regen-at-merge.md @@ -0,0 +1,39 @@ +# #5762 revised: contracts.nt / shapes.ttl / witness / README count are generated shared files + +Owner: flow (aprender-flow). Supersedes the 14:30Z text after the 3-lane Opus quorum (receipt: +aprender-pace q5762/receipt.md): "regen-at-merge, untrack the files" was NO as written. Four blockers, answered below. + +## What is generated (corrected: four things, not two) +`contracts/contracts.nt`, `contracts/shapes.ttl` (`contracts_gate.sh` GENERATED=), `contracts/witness/.json` +(pv-sat; the name is the hash of the graph), and the contract count inside README.md (`scripts/readme_sync.sh`). +Two PRs that each add a contract conflict on them because each commits its own regenerated copy. + +## Blockers from the quorum and the answer +1. step_diff / ont-consistency starve if the files are untracked: **agreed. Nothing is untracked.** The gate is unchanged. +2. shapes.ttl omitted: **added** (and README.md). +3. No workflow can push to protected main, so "a job writes the committed copy" is impossible: **dropped.** No bot, no admin skip. +4. The verify step stays a blocking GATE with a RED mutant row: **unchanged**; `contracts_gate.sh` is not edited, so its + existing row "a contract added WITHOUT regenerating is RED on diff" (`contracts_gate.sh` --self-test) keeps covering it. + +## Proposal: option "merge-main + regen helper" (quorum's lower-risk alternative 7) +`scripts/contracts_resolve.sh` (new, 40 lines, a developer tool, NOT on any CI path, not gate content): +after `git merge origin/main` stops, it refuses unless every conflict is a generated path, drops those paths, regenerates +them with the gate's own `regen` step + `pv-sat` + `readme_sync.sh --write`, and stages them. The gate stays the judge. + +Measured (throwaway merge of #5710 head with origin/main 14:50Z, never pushed): +- before: conflict on `contracts/witness/811c7818...json`; README count stale. +- `bash scripts/contracts_resolve.sh`: 54 s wall (pv build cached), pv-sat 2 ms. +- then commit, `bash scripts/contracts_gate.sh`: `8 of 8 step(s) RAN, 0 FAILED` (diff + consistency + readme green). +- first attempt without the README step: `2 FAILED: census readme` -> that is why README.md is in the set. +Not measured: #5672 (same shape, not run), a merge where a non-generated file also conflicts (the helper refuses by design). + +## What this does not fix +The conflict still happens; it becomes a 1-minute mechanical step per PR instead of a hand job. Removing it needs +option B (fragment: one `.nt` per contract, witness out of tree), a bigger, one-way change that I am not proposing +until the consumers listed by the quorum (`lint_passes_on_real_contracts`, `ont4d_subsumption`, `ont5_consistency_gate`, +`tests/oracle/jena`, `batch_fold.sh`) are costed. Falsifier for this proposal: a DIRTY contract PR that +`contracts_resolve.sh` leaves red on `contracts_gate.sh`. + +## Ask +No quorum needed for the script alone (no workflow, no gate content). Please confirm that reading; if you want it quorumed +anyway, the receipt can be on this head. diff --git a/scripts/contracts_resolve.sh b/scripts/contracts_resolve.sh new file mode 100644 index 0000000000..f6f3d6e738 --- /dev/null +++ b/scripts/contracts_resolve.sh @@ -0,0 +1,42 @@ +#!/usr/bin/env bash +# contracts_resolve.sh -- finish a `git merge origin/main` that stopped on the GENERATED contract files. +# +# contracts/contracts.nt, contracts/shapes.ttl and contracts/witness/*.json are derived from contracts/*.yaml +# (scripts/contracts_gate.sh GENERATED=, pv-sat); README.md carries a derived count (scripts/readme_sync.sh). Two PRs that each add a contract conflict on them, and +# neither side's copy is right: the merged tree needs a fresh one. This takes no side. It drops the +# generated paths from the conflict, regenerates them from the merged sources with the gate's own regen +# step and pv-sat, and stages the result. It never touches a source file, and it refuses to run if any +# conflict is outside the generated set, so a real conflict is never resolved by regeneration. +# +# git merge origin/main # stops on contracts.nt / witness +# bash scripts/contracts_resolve.sh +# bash scripts/contracts_gate.sh # the gate stays the judge +# +# Pmat-Ticket: #5762 +set -euo pipefail + +GENERATED_RE='^contracts/(contracts\.nt|shapes\.ttl|witness/.*\.json)$' + +conflicted=$(git diff --name-only --diff-filter=U) +[ -n "$conflicted" ] || echo "contracts_resolve: no conflict; regenerating the generated files from the merged sources" +other=$(printf '%s\n' "$conflicted" | grep -vE "$GENERATED_RE" || true) +if [ -n "$other" ]; then + printf 'contracts_resolve: REFUSED, conflicts outside the generated set:\n%s\n' "$other" >&2 + exit 1 +fi + +# Drop both sides of every generated path; the regeneration below recreates what the merged sources produce. +printf '%s\n' "$conflicted" | while IFS= read -r f; do + [ -n "$f" ] || continue + git rm -q --cached --ignore-unmatch -- "$f" + rm -f -- "${f:?}" +done + +. scripts/pv_bin.sh || exit 1 +bash scripts/contracts_gate.sh regen +"${PV_SAT:-$(dirname "$PV")/pv-sat}" contracts +bash scripts/readme_sync.sh --write # README.md carries a derived contract count: also stale after a merge +git add -A -- contracts/contracts.nt contracts/shapes.ttl contracts/witness README.md +left=$(git diff --name-only --diff-filter=U) +[ -z "$left" ] || { printf 'contracts_resolve: still conflicted:\n%s\n' "$left" >&2; exit 1; } +echo "contracts_resolve: regenerated and staged; run scripts/contracts_gate.sh, then commit the merge"