diff --git a/README.md b/README.md index a2c2305d2e..5c4169aff2 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 | **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`) | +| Provable contracts | **1994** 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 1993 contracts across inference, training, quantization, attention, FFN, +The tree carries 1994 contracts across inference, training, quantization, attention, FFN, tokenization, model formats, CLI safety — and this README itself. ## Migration from old crates diff --git a/contracts/contracts.nt b/contracts/contracts.nt index 70db0aa4b0..c32ab0c975 100644 --- a/contracts/contracts.nt +++ b/contracts/contracts.nt @@ -13021,6 +13021,13 @@ "contracts/pp-llama-001-spec-conformance-v1.yaml"^^ . "pp-llama-001-spec-conformance-v1"^^ . "pattern"^^ . + . + . + . + "contracts/pr-flow-sim4-bounds-v1.yaml"^^ . + "pr-flow-sim4-bounds-v1"^^ . + "pr-flow-sim4-bounds"^^ . + "1.0.0"^^ . . . . diff --git a/contracts/pr-flow-sim4-bounds-v1.yaml b/contracts/pr-flow-sim4-bounds-v1.yaml new file mode 100644 index 0000000000..07ae9b9f4b --- /dev/null +++ b/contracts/pr-flow-sim4-bounds-v1.yaml @@ -0,0 +1,51 @@ +metadata: + version: "1.0.0" + created: "2026-10-19" + author: PAIML Engineering + registry: true + references: + - "FLOW-005 SIM-4 (cop-inbox handoff), issue #5511" + - "Little, J.D.C. (1961), A Proof for the Queuing Formula L = lambda W." + description: "pr_flow prediction must satisfy the three SIM-4 capacity inequalities, and name the breached one" + +name: pr-flow-sim4-bounds +version: "1.0.0" +scope: "crates/aprender-simulate/src/scenarios/pr_flow.rs" + +description: | + Every batch's pr_flow prediction is checked against three inequalities: merged/h + <= cap/W, PR runner-min/h <= R_pr * 51, and merge-queue passes/h <= R_mq * 51 / + mq_runner_min (51 = 85% of 60 runner-min per runner-hour). sim4_breaches returns the + names of the breached ones; a non-empty result is the andon. On the reference + designs D, G and E none is breached; design A breaches mq_passes, because its 4 + merge-queue runners run at about 97%. + +equations: + cap_bound: + description: "throughput cannot exceed the WIP cap over the mean time open" + formula: "merged_per_h <= cap / W" + pr_runner_bound: + description: "PR runner-minutes consumed per hour stay under the usable ceiling" + formula: "merged_per_h * pr_runner_min * runs_per_pr <= R_pr * 51" + mq_pass_bound: + description: "merge-queue passes per hour stay under the usable ceiling" + formula: "merged_per_h / prs_per_pass <= R_mq * 51 / mq_runner_min" + +falsification_tests: + - id: FALSIFY-001 + description: "D, G and E breach nothing; A breaches exactly mq_passes" + test: "cargo test -p aprender-simulate --lib sim4_holds_on_the_proposed_designs_and_flags_the_saturated_merge_queue_of_a" + prediction: "the test passes" + if_fails: "a bound is mis-stated or the saturated design is no longer flagged" + + - id: FALSIFY-002 + description: "each inequality is named when, and only when, it is breached" + test: "cargo test -p aprender-simulate --lib sim4_names_each_breached_inequality" + prediction: "the test passes" + if_fails: "a breach is dropped or misattributed, so the andon would stay silent" + + - id: FALSIFY-003 + description: "PR runner load scales with runs per PR, so red-and-fix loops count" + test: "cargo test -p aprender-simulate --lib sim4_pr_runner_load_scales_with_runs_per_pr" + prediction: "the test passes" + if_fails: "rework runs are not counted, so the PR pool bound is understated" diff --git a/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json b/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json index b6e4620fa7..7443b14e11 100644 --- a/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json +++ b/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json @@ -1,5 +1,5 @@ { - "census_id_set_sha256": "c9013292ce5d9aa45045302bf73eb8bb217b4fb272cd819d55c36157b94fa942", + "census_id_set_sha256": "eeb30a611e730d7e82e02815708b6488d97497429cc1fd51a258d6f3bbb2ff0d", "relations_sha256": "811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850", "checkable_n": 87, "result": { diff --git a/crates/aprender-simulate/src/scenarios/pr_flow.rs b/crates/aprender-simulate/src/scenarios/pr_flow.rs index 5aa549e1ca..da71886fbd 100644 --- a/crates/aprender-simulate/src/scenarios/pr_flow.rs +++ b/crates/aprender-simulate/src/scenarios/pr_flow.rs @@ -597,6 +597,33 @@ pub fn bounds(c: &PrFlowConfig, r: &PrFlowResult) -> [(&'static str, f64); 4] { ] } +/// Usable runner-minutes per runner-hour: the 85% ceiling of FLOW-005 SIM-4. +pub const RUNNER_MIN_PER_H: f64 = 51.0; + +/// FLOW-005 SIM-4: the three inequalities every batch's prediction must satisfy. +/// +/// Returns the names of the ones that are breached (empty means all hold): +/// `cap` is merged/h <= cap/W, `pr_runner` is PR runner-min/h <= R_pr * 51, and +/// `mq_passes` is merge-queue passes/h <= R_mq * 51 / mq_runner_min. `cap` carries the +/// 0.5% Little's-law tolerance the SIM-3 contract allows. +#[must_use] +pub fn sim4_breaches(c: &PrFlowConfig, r: &PrFlowResult) -> Vec<&'static str> { + let w_h = (r.w_mean_min / 60.0).max(f64::EPSILON); + let pr_min_h = r.merged_per_h * c.pr_runner_min * r.runs_per_pr.max(1.0); + let passes_h = r.merged_per_h / r.prs_per_pass.max(1.0); + let mut out = Vec::new(); + if r.merged_per_h > c.cap as f64 / w_h * 1.005 { + out.push("cap"); + } + if pr_min_h > c.r_pr as f64 * RUNNER_MIN_PER_H { + out.push("pr_runner"); + } + if passes_h > c.r_mq as f64 * RUNNER_MIN_PER_H / c.mq_runner_min { + out.push("mq_passes"); + } + out +} + /// The binding station: argmin of [`bounds`]. No utilisation thresholds. #[must_use] pub fn binding_station(c: &PrFlowConfig, r: &PrFlowResult) -> &'static str { @@ -741,6 +768,55 @@ mod tests { c } + #[test] + fn sim4_holds_on_the_proposed_designs_and_flags_the_saturated_merge_queue_of_a() { + for (d, _) in WANT { + let c = preset(d).expect("preset"); + let r = run_reference(&c); + let want: Vec<&str> = if d == "A" { vec!["mq_passes"] } else { vec![] }; + assert_eq!(sim4_breaches(&c, &r), want, "{d}"); + } + } + + #[test] + fn sim4_names_each_breached_inequality() { + let c = preset("D").expect("preset"); + let r = run_reference(&c); + let hot = |k: f64| PrFlowResult { + merged_per_h: r.merged_per_h * k, + ..r.clone() + }; + assert_eq!( + sim4_breaches(&c, &hot(1.5)), + vec!["cap", "pr_runner", "mq_passes"] + ); + let mut few = c.clone(); + few.r_pr = 1; + assert_eq!(sim4_breaches(&few, &r), vec!["pr_runner"]); + let mut mq = c.clone(); + mq.r_mq = 1; + assert_eq!(sim4_breaches(&mq, &r), vec!["mq_passes"]); + let mut cap = c.clone(); + cap.cap = 1; + assert_eq!(sim4_breaches(&cap, &r), vec!["cap"]); + } + + #[test] + fn sim4_pr_runner_load_scales_with_runs_per_pr() { + let c = preset("D").expect("preset"); + let r = run_reference(&c); + let one = PrFlowResult { + runs_per_pr: 1.0, + ..r.clone() + }; + let many = PrFlowResult { + runs_per_pr: 1000.0, + ..r + }; + assert!(!sim4_breaches(&c, &one).contains(&"pr_runner")); + assert!(sim4_breaches(&c, &many).contains(&"pr_runner")); + } + #[test] fn six_minutes_of_review_adds_about_two_to_l_at_20_per_hour() { let mut c = roomy();