From 8e7e2fdd927cd3962836e93b7f6f27874ec6e55d Mon Sep 17 00:00:00 2001 From: ImgBotApp Date: Fri, 14 Aug 2026 10:22:17 +0000 Subject: [PATCH] [ImgBot] Optimize images *Total -- 535.94kb -> 507.90kb (5.23%) /docs/img/observers-light.svg -- 3.26kb -> 2.93kb (10.03%) /docs/img/observers-dark.svg -- 3.26kb -> 2.93kb (10.03%) /docs/img/architecture-light.svg -- 5.10kb -> 4.69kb (8.08%) /docs/img/architecture-dark.svg -- 5.10kb -> 4.69kb (8.08%) /readme-assets/coverage-light.svg -- 24.02kb -> 22.15kb (7.78%) /docs/img/coverage-light.svg -- 24.02kb -> 22.15kb (7.78%) /readme-assets/coverage-dark.svg -- 24.02kb -> 22.15kb (7.77%) /docs/img/coverage-dark.svg -- 24.02kb -> 22.15kb (7.77%) /readme-assets/certification-light.svg -- 19.08kb -> 18.12kb (5.06%) /docs/img/certification-light.svg -- 19.08kb -> 18.12kb (5.06%) /readme-assets/certification-dark.svg -- 19.08kb -> 18.12kb (5.06%) /docs/img/certification-dark.svg -- 19.08kb -> 18.12kb (5.06%) /readme-assets/claims-light.svg -- 14.96kb -> 14.21kb (5%) /docs/img/claims-light.svg -- 14.96kb -> 14.21kb (5%) /readme-assets/claims-dark.svg -- 14.96kb -> 14.21kb (4.99%) /docs/img/claims-dark.svg -- 14.96kb -> 14.21kb (4.99%) /readme-assets/throughput-light.svg -- 18.56kb -> 17.69kb (4.66%) /docs/img/throughput-light.svg -- 18.56kb -> 17.69kb (4.66%) /readme-assets/throughput-dark.svg -- 18.56kb -> 17.69kb (4.65%) /docs/img/throughput-dark.svg -- 18.56kb -> 17.69kb (4.65%) /readme-assets/three-numbers-light.svg -- 13.85kb -> 13.21kb (4.61%) /docs/img/three-numbers-light.svg -- 13.85kb -> 13.21kb (4.61%) /readme-assets/three-numbers-dark.svg -- 13.85kb -> 13.21kb (4.6%) /docs/img/three-numbers-dark.svg -- 13.85kb -> 13.21kb (4.6%) /readme-assets/mutation-light.svg -- 18.17kb -> 17.42kb (4.12%) /docs/img/mutation-light.svg -- 18.17kb -> 17.42kb (4.12%) /readme-assets/mutation-dark.svg -- 18.17kb -> 17.42kb (4.11%) /docs/img/mutation-dark.svg -- 18.17kb -> 17.42kb (4.11%) /readme-assets/thesis-light.svg -- 21.17kb -> 20.36kb (3.83%) /docs/img/thesis-light.svg -- 21.17kb -> 20.36kb (3.83%) /readme-assets/thesis-dark.svg -- 21.17kb -> 20.36kb (3.82%) /docs/img/thesis-dark.svg -- 21.17kb -> 20.36kb (3.82%) Signed-off-by: ImgBotApp --- docs/img/architecture-dark.svg | 91 +--------- docs/img/architecture-light.svg | 91 +--------- docs/img/certification-dark.svg | 162 +---------------- docs/img/certification-light.svg | 162 +---------------- docs/img/claims-dark.svg | 132 +------------- docs/img/claims-light.svg | 132 +------------- docs/img/coverage-dark.svg | 243 +------------------------- docs/img/coverage-light.svg | 243 +------------------------- docs/img/mutation-dark.svg | 147 +--------------- docs/img/mutation-light.svg | 147 +--------------- docs/img/observers-dark.svg | 60 +------ docs/img/observers-light.svg | 60 +------ docs/img/thesis-dark.svg | 174 +----------------- docs/img/thesis-light.svg | 174 +----------------- docs/img/three-numbers-dark.svg | 133 +------------- docs/img/three-numbers-light.svg | 133 +------------- docs/img/throughput-dark.svg | 156 +---------------- docs/img/throughput-light.svg | 156 +---------------- readme-assets/certification-dark.svg | 162 +---------------- readme-assets/certification-light.svg | 162 +---------------- readme-assets/claims-dark.svg | 132 +------------- readme-assets/claims-light.svg | 132 +------------- readme-assets/coverage-dark.svg | 243 +------------------------- readme-assets/coverage-light.svg | 243 +------------------------- readme-assets/mutation-dark.svg | 147 +--------------- readme-assets/mutation-light.svg | 147 +--------------- readme-assets/thesis-dark.svg | 174 +----------------- readme-assets/thesis-light.svg | 174 +----------------- readme-assets/three-numbers-dark.svg | 133 +------------- readme-assets/three-numbers-light.svg | 133 +------------- readme-assets/throughput-dark.svg | 156 +---------------- readme-assets/throughput-light.svg | 156 +---------------- 32 files changed, 32 insertions(+), 4858 deletions(-) diff --git a/docs/img/architecture-dark.svg b/docs/img/architecture-dark.svg index 3bf7f96..9f003bb 100644 --- a/docs/img/architecture-dark.svg +++ b/docs/img/architecture-dark.svg @@ -1,90 +1 @@ - - - - - - - - - - - - execution is a pure function of (workload, schedule, seeds) - - - workload - - schedule - - seeds - the schedule is supplied, - not observed - - - - - - - lockstep - engine - - - - - - served run - under the given schedule - - - canonical run - batch 1, uninterrupted - - canonical is the same engine re-run under a - different schedule, not a separate reference - - - - - - oracles compare the two, bitwise - I1 to I4 F1 PATH-EQ golden bytes - - - - - - - internal, white box - external, black box - - - minimizer: ddmin, 1-minimal - - - witness artifact + env.lock - - - report.html - - - certifier - - HTTP - - another engine entirely - vLLM or SGLang, started locally - - it never sees a trajectory; it reads - logprobs, which is strictly weaker - - the two loops share the relations and nothing else - +execution is a pure function of (workload, schedule, seeds)workloadscheduleseedsthe schedule is supplied,not observedlockstepengineserved rununder the given schedulecanonical runbatch 1, uninterruptedcanonical is the same engine re-run under adifferent schedule, not a separate referenceoracles compare the two, bitwiseI1 to I4 F1 PATH-EQ golden bytesinternal, white boxexternal, black boxminimizer: ddmin, 1-minimalwitness artifact + env.lockreport.htmlcertifierHTTPanother engine entirelyvLLM or SGLang, started locallyit never sees a trajectory; it readslogprobs, which is strictly weakerthe two loops share the relations and nothing else \ No newline at end of file diff --git a/docs/img/architecture-light.svg b/docs/img/architecture-light.svg index a9c4c7a..7560e3e 100644 --- a/docs/img/architecture-light.svg +++ b/docs/img/architecture-light.svg @@ -1,90 +1 @@ - - - - - - - - - - - - execution is a pure function of (workload, schedule, seeds) - - - workload - - schedule - - seeds - the schedule is supplied, - not observed - - - - - - - lockstep - engine - - - - - - served run - under the given schedule - - - canonical run - batch 1, uninterrupted - - canonical is the same engine re-run under a - different schedule, not a separate reference - - - - - - oracles compare the two, bitwise - I1 to I4 F1 PATH-EQ golden bytes - - - - - - - internal, white box - external, black box - - - minimizer: ddmin, 1-minimal - - - witness artifact + env.lock - - - report.html - - - certifier - - HTTP - - another engine entirely - vLLM or SGLang, started locally - - it never sees a trajectory; it reads - logprobs, which is strictly weaker - - the two loops share the relations and nothing else - +execution is a pure function of (workload, schedule, seeds)workloadscheduleseedsthe schedule is supplied,not observedlockstepengineserved rununder the given schedulecanonical runbatch 1, uninterruptedcanonical is the same engine re-run under adifferent schedule, not a separate referenceoracles compare the two, bitwiseI1 to I4 F1 PATH-EQ golden bytesinternal, white boxexternal, black boxminimizer: ddmin, 1-minimalwitness artifact + env.lockreport.htmlcertifierHTTPanother engine entirelyvLLM or SGLang, started locallyit never sees a trajectory; it readslogprobs, which is strictly weakerthe two loops share the relations and nothing else \ No newline at end of file diff --git a/docs/img/certification-dark.svg b/docs/img/certification-dark.svg index 99235bd..4c707f8 100644 --- a/docs/img/certification-dark.svg +++ b/docs/img/certification-dark.svg @@ -1,161 +1 @@ - -vLLM certification across seven boundary cases -Seven boundary cases against vLLM batch-invariant mode: five clean, and two diverged at 44 and 45 co-resident with logprob deltas of 4.685e-02 and 3.906e-02 and no token divergence. The max-num-seqs control restores reproducibility at 8. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -CERTIFICATION - - - - -Black-box differential testing of vLLM batch-invariant mode -concurrent submission, co-residency read from the engine's own gauge, every pair of repeats compared - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -SOURCE -evidence/certify-pairs-{a,b,mns8}.json :: vllm-project/vllm#51187 -LOCKSTEP -BOUNDARY CASE -CO-RESIDENT -VERDICT - -prefix_len == block_size - 1 - - -15 - - -clean - -prefix_len == block_size - - -15 - - -clean - -prefix_len == block_size + 1 - - -15 - - -clean - -zero-prefix co-batched with nonzero - - -16 - - -clean - -cache hit covering the full prompt - - -15 - - -clean - -batch 31, shared prefix of one block - - -44 - - -diverged -max delta 4.685e-02 - -batch 32, shared prefix of one block - - -45 - - -diverged -max delta 3.906e-02 - -CONTROL -one knob, and the only controlled single-variable result in this section ---max-num-seqs 8 - -8 co-resident -1 of 5, reproducible ---max-num-seqs 64 - -45 co-resident -not reproducible ---max-num-seqs 128, the default - -45 co-resident -not reproducible, intermittently -intermittent at about one lifetime in three, so which cases trip is not the claim. token ids never move, only logprobs. filed as vllm#51187. - +vLLM certification across seven boundary casesSeven boundary cases against vLLM batch-invariant mode: five clean, and two diverged at 44 and 45 co-resident with logprob deltas of 4.685e-02 and 3.906e-02 and no token divergence. The max-num-seqs control restores reproducibility at 8.CERTIFICATIONBlack-box differential testing of vLLM batch-invariant modeconcurrent submission, co-residency read from the engine's own gauge, every pair of repeats comparedSOURCEevidence/certify-pairs-{a,b,mns8}.json :: vllm-project/vllm#51187LOCKSTEPBOUNDARY CASECO-RESIDENTVERDICTprefix_len == block_size - 115cleanprefix_len == block_size15cleanprefix_len == block_size + 115cleanzero-prefix co-batched with nonzero16cleancache hit covering the full prompt15cleanbatch 31, shared prefix of one block44divergedmax delta 4.685e-02batch 32, shared prefix of one block45divergedmax delta 3.906e-02CONTROLone knob, and the only controlled single-variable result in this section--max-num-seqs 88 co-resident1 of 5, reproducible--max-num-seqs 6445 co-residentnot reproducible--max-num-seqs 128, the default45 co-residentnot reproducible, intermittentlyintermittent at about one lifetime in three, so which cases trip is not the claim. token ids never move, only logprobs. filed as vllm#51187. \ No newline at end of file diff --git a/docs/img/certification-light.svg b/docs/img/certification-light.svg index 7e7ab49..5fc2083 100644 --- a/docs/img/certification-light.svg +++ b/docs/img/certification-light.svg @@ -1,161 +1 @@ - -vLLM certification across seven boundary cases -Seven boundary cases against vLLM batch-invariant mode: five clean, and two diverged at 44 and 45 co-resident with logprob deltas of 4.685e-02 and 3.906e-02 and no token divergence. The max-num-seqs control restores reproducibility at 8. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -CERTIFICATION - - - - -Black-box differential testing of vLLM batch-invariant mode -concurrent submission, co-residency read from the engine's own gauge, every pair of repeats compared - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -SOURCE -evidence/certify-pairs-{a,b,mns8}.json :: vllm-project/vllm#51187 -LOCKSTEP -BOUNDARY CASE -CO-RESIDENT -VERDICT - -prefix_len == block_size - 1 - - -15 - - -clean - -prefix_len == block_size - - -15 - - -clean - -prefix_len == block_size + 1 - - -15 - - -clean - -zero-prefix co-batched with nonzero - - -16 - - -clean - -cache hit covering the full prompt - - -15 - - -clean - -batch 31, shared prefix of one block - - -44 - - -diverged -max delta 4.685e-02 - -batch 32, shared prefix of one block - - -45 - - -diverged -max delta 3.906e-02 - -CONTROL -one knob, and the only controlled single-variable result in this section ---max-num-seqs 8 - -8 co-resident -1 of 5, reproducible ---max-num-seqs 64 - -45 co-resident -not reproducible ---max-num-seqs 128, the default - -45 co-resident -not reproducible, intermittently -intermittent at about one lifetime in three, so which cases trip is not the claim. token ids never move, only logprobs. filed as vllm#51187. - +vLLM certification across seven boundary casesSeven boundary cases against vLLM batch-invariant mode: five clean, and two diverged at 44 and 45 co-resident with logprob deltas of 4.685e-02 and 3.906e-02 and no token divergence. The max-num-seqs control restores reproducibility at 8.CERTIFICATIONBlack-box differential testing of vLLM batch-invariant modeconcurrent submission, co-residency read from the engine's own gauge, every pair of repeats comparedSOURCEevidence/certify-pairs-{a,b,mns8}.json :: vllm-project/vllm#51187LOCKSTEPBOUNDARY CASECO-RESIDENTVERDICTprefix_len == block_size - 115cleanprefix_len == block_size15cleanprefix_len == block_size + 115cleanzero-prefix co-batched with nonzero16cleancache hit covering the full prompt15cleanbatch 31, shared prefix of one block44divergedmax delta 4.685e-02batch 32, shared prefix of one block45divergedmax delta 3.906e-02CONTROLone knob, and the only controlled single-variable result in this section--max-num-seqs 88 co-resident1 of 5, reproducible--max-num-seqs 6445 co-residentnot reproducible--max-num-seqs 128, the default45 co-residentnot reproducible, intermittentlyintermittent at about one lifetime in three, so which cases trip is not the claim. token ids never move, only logprobs. filed as vllm#51187. \ No newline at end of file diff --git a/docs/img/claims-dark.svg b/docs/img/claims-dark.svg index 297b72e..4c70718 100644 --- a/docs/img/claims-dark.svg +++ b/docs/img/claims-dark.svg @@ -1,131 +1 @@ - -Claims I1 to I4 and F1 -Five claims with what verifies each. I1 batch invariance, I2 schedule invariance, I3 replay determinism and I4 RNG isolation all hold. F1 fidelity passes 7 of 7 bounds against an fp64 CPU reference. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -CLAIMS - - - -Five relations, and what measures each one -every claim scoped to one environment tuple, bitwise unless a tolerance is stated - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -SOURCE -evidence/verify-0002.json :: evidence/fidelity-0001.json -LOCKSTEP - - - - - -I1 -Batch invariancebit-identical to canonical, whatever cohabits -MR1, MR5 · fp16 logit bytes · batch 1 to 32 - - -holds - - - - - -I2 -Schedule invarianceany preemption, chunk partition, eviction, cache hit -MR2, MR3, MR4 · per-layer KV equality - - -holds - - - - - -I3 -Replay determinismsame (W, sigma, seeds), same trajectory hash -MR6 · 8 shapes · cross-process, differing PYTHONHASHSEED - - -holds - - - - - -I4 -RNG isolationtokens from (seed, uid, position) and own logits only -MR7 · 11 perturbations of the cohabitant set - - -holds - - - - - -F1 -Fidelitybatch-1 logits against an fp64 CPU reference -exact KL over 151936 tokens at 2756 positions - - -7 of 7 -every claim is scoped to the environment tuple in env.lock. a claim without one is invalid by construction. - +Claims I1 to I4 and F1Five claims with what verifies each. I1 batch invariance, I2 schedule invariance, I3 replay determinism and I4 RNG isolation all hold. F1 fidelity passes 7 of 7 bounds against an fp64 CPU reference.CLAIMSFive relations, and what measures each oneevery claim scoped to one environment tuple, bitwise unless a tolerance is statedSOURCEevidence/verify-0002.json :: evidence/fidelity-0001.jsonLOCKSTEPI1Batch invariancebit-identical to canonical, whatever cohabitsMR1, MR5 · fp16 logit bytes · batch 1 to 32holdsI2Schedule invarianceany preemption, chunk partition, eviction, cache hitMR2, MR3, MR4 · per-layer KV equalityholdsI3Replay determinismsame (W, sigma, seeds), same trajectory hashMR6 · 8 shapes · cross-process, differing PYTHONHASHSEEDholdsI4RNG isolationtokens from (seed, uid, position) and own logits onlyMR7 · 11 perturbations of the cohabitant setholdsF1Fidelitybatch-1 logits against an fp64 CPU referenceexact KL over 151936 tokens at 2756 positions7 of 7every claim is scoped to the environment tuple in env.lock. a claim without one is invalid by construction. \ No newline at end of file diff --git a/docs/img/claims-light.svg b/docs/img/claims-light.svg index d097fbe..9a01bc7 100644 --- a/docs/img/claims-light.svg +++ b/docs/img/claims-light.svg @@ -1,131 +1 @@ - -Claims I1 to I4 and F1 -Five claims with what verifies each. I1 batch invariance, I2 schedule invariance, I3 replay determinism and I4 RNG isolation all hold. F1 fidelity passes 7 of 7 bounds against an fp64 CPU reference. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -CLAIMS - - - -Five relations, and what measures each one -every claim scoped to one environment tuple, bitwise unless a tolerance is stated - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -SOURCE -evidence/verify-0002.json :: evidence/fidelity-0001.json -LOCKSTEP - - - - - -I1 -Batch invariancebit-identical to canonical, whatever cohabits -MR1, MR5 · fp16 logit bytes · batch 1 to 32 - - -holds - - - - - -I2 -Schedule invarianceany preemption, chunk partition, eviction, cache hit -MR2, MR3, MR4 · per-layer KV equality - - -holds - - - - - -I3 -Replay determinismsame (W, sigma, seeds), same trajectory hash -MR6 · 8 shapes · cross-process, differing PYTHONHASHSEED - - -holds - - - - - -I4 -RNG isolationtokens from (seed, uid, position) and own logits only -MR7 · 11 perturbations of the cohabitant set - - -holds - - - - - -F1 -Fidelitybatch-1 logits against an fp64 CPU reference -exact KL over 151936 tokens at 2756 positions - - -7 of 7 -every claim is scoped to the environment tuple in env.lock. a claim without one is invalid by construction. - +Claims I1 to I4 and F1Five claims with what verifies each. I1 batch invariance, I2 schedule invariance, I3 replay determinism and I4 RNG isolation all hold. F1 fidelity passes 7 of 7 bounds against an fp64 CPU reference.CLAIMSFive relations, and what measures each oneevery claim scoped to one environment tuple, bitwise unless a tolerance is statedSOURCEevidence/verify-0002.json :: evidence/fidelity-0001.jsonLOCKSTEPI1Batch invariancebit-identical to canonical, whatever cohabitsMR1, MR5 · fp16 logit bytes · batch 1 to 32holdsI2Schedule invarianceany preemption, chunk partition, eviction, cache hitMR2, MR3, MR4 · per-layer KV equalityholdsI3Replay determinismsame (W, sigma, seeds), same trajectory hashMR6 · 8 shapes · cross-process, differing PYTHONHASHSEEDholdsI4RNG isolationtokens from (seed, uid, position) and own logits onlyMR7 · 11 perturbations of the cohabitant setholdsF1Fidelitybatch-1 logits against an fp64 CPU referenceexact KL over 151936 tokens at 2756 positions7 of 7every claim is scoped to the environment tuple in env.lock. a claim without one is invalid by construction. \ No newline at end of file diff --git a/docs/img/coverage-dark.svg b/docs/img/coverage-dark.svg index ed1d4fd..3edd503 100644 --- a/docs/img/coverage-dark.svg +++ b/docs/img/coverage-dark.svg @@ -1,242 +1 @@ - -Lifecycle n-gram coverage against the corrected denominator -19 of 25 two-grams and 43 of 79 three-grams reached, split between the swarm campaign and the eviction campaign, with probe-only cells outlined and never-reached cells hatched. The denominator was corrected from 27 and 84. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -COVERAGE - - - -Lifecycle n-grams, against the real denominator -reported by population, because a case built to reach a transition is not exploration - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -SOURCE -evidence/fuzz-0002.json :: scripts/verify_no_gpu.py -LOCKSTEP -2-GRAMS -19 of 25 -probes reach 20 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -3-GRAMS -43 of 79 -probes reach 46 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -DENOMINATOR -27 and 84 - --> -25 and 79 -one declared transition was never reachable -every percentage published before the correction was computed against a denominator that was too large. -the correction moves them up, 55.6 to 60.0 percent on 2-grams at identical observed counts, which is exactly why it is stated here. - -swarm campaign, 72 cases - -plus eviction, 132 cases - -targeted probe only - - -never reached - +Lifecycle n-gram coverage against the corrected denominator19 of 25 two-grams and 43 of 79 three-grams reached, split between the swarm campaign and the eviction campaign, with probe-only cells outlined and never-reached cells hatched. The denominator was corrected from 27 and 84.COVERAGELifecycle n-grams, against the real denominatorreported by population, because a case built to reach a transition is not explorationSOURCEevidence/fuzz-0002.json :: scripts/verify_no_gpu.pyLOCKSTEP2-GRAMS19 of 25probes reach 203-GRAMS43 of 79probes reach 46DENOMINATOR27 and 84->25 and 79one declared transition was never reachableevery percentage published before the correction was computed against a denominator that was too large.the correction moves them up, 55.6 to 60.0 percent on 2-grams at identical observed counts, which is exactly why it is stated here.swarm campaign, 72 casesplus eviction, 132 casestargeted probe onlynever reached \ No newline at end of file diff --git a/docs/img/coverage-light.svg b/docs/img/coverage-light.svg index fe1b3f9..f36259f 100644 --- a/docs/img/coverage-light.svg +++ b/docs/img/coverage-light.svg @@ -1,242 +1 @@ - -Lifecycle n-gram coverage against the corrected denominator -19 of 25 two-grams and 43 of 79 three-grams reached, split between the swarm campaign and the eviction campaign, with probe-only cells outlined and never-reached cells hatched. The denominator was corrected from 27 and 84. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -COVERAGE - - - -Lifecycle n-grams, against the real denominator -reported by population, because a case built to reach a transition is not exploration - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -SOURCE -evidence/fuzz-0002.json :: scripts/verify_no_gpu.py -LOCKSTEP -2-GRAMS -19 of 25 -probes reach 20 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -3-GRAMS -43 of 79 -probes reach 46 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -DENOMINATOR -27 and 84 - --> -25 and 79 -one declared transition was never reachable -every percentage published before the correction was computed against a denominator that was too large. -the correction moves them up, 55.6 to 60.0 percent on 2-grams at identical observed counts, which is exactly why it is stated here. - -swarm campaign, 72 cases - -plus eviction, 132 cases - -targeted probe only - - -never reached - +Lifecycle n-gram coverage against the corrected denominator19 of 25 two-grams and 43 of 79 three-grams reached, split between the swarm campaign and the eviction campaign, with probe-only cells outlined and never-reached cells hatched. The denominator was corrected from 27 and 84.COVERAGELifecycle n-grams, against the real denominatorreported by population, because a case built to reach a transition is not explorationSOURCEevidence/fuzz-0002.json :: scripts/verify_no_gpu.pyLOCKSTEP2-GRAMS19 of 25probes reach 203-GRAMS43 of 79probes reach 46DENOMINATOR27 and 84->25 and 79one declared transition was never reachableevery percentage published before the correction was computed against a denominator that was too large.the correction moves them up, 55.6 to 60.0 percent on 2-grams at identical observed counts, which is exactly why it is stated here.swarm campaign, 72 casesplus eviction, 132 casestargeted probe onlynever reached \ No newline at end of file diff --git a/docs/img/mutation-dark.svg b/docs/img/mutation-dark.svg index 787b12d..28db3e6 100644 --- a/docs/img/mutation-dark.svg +++ b/docs/img/mutation-dark.svg @@ -1,146 +1 @@ - -Mutation campaign, with and without golden bytes -Ten mutation operators. Nine killed by the invariance relations and F1 alone, with the reversed split-combine fold surviving. Ten killed once golden bytes are added as an observer outside the process. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -CLAIM 2 HARNESS POWER - - - - -What the harness catches, and what took a third observer -identical operator set, identical campaign, one mutant of difference - - - - - - - - - - - - - - - - - - - - - - - -SOURCE -evidence/fuzz-0002.json -LOCKSTEP - -invariance relations and F1 only -the fold reversal is not a function of the schedule, -so the engine agrees with itself and both pass - -9 of 10 killed - - -O1 - - -O2 - - -O3 - - -O4 - - -O5 - - -O6 - - -O7 - - -O8 - - -O9 - - - -O10 - -with golden bytes -a committed sha256 over raw fp16 logit bytes, -compared exactly, from outside the process - -10 of 10 killed - - -O1 - - -O2 - - -O3 - - -O4 - - -O5 - - -O6 - - -O7 - - -O8 - - -O9 - - -O10 - -the one mutant that separates the two rows: -reversed split-combine fold -every operator fires a sentinel from inside the mutant body, so no trial here is a mutant that never ran. path executed, -patch executed and fault injected are three claims, and the counters can only tell you about the first. - +Mutation campaign, with and without golden bytesTen mutation operators. Nine killed by the invariance relations and F1 alone, with the reversed split-combine fold surviving. Ten killed once golden bytes are added as an observer outside the process.CLAIM 2 HARNESS POWERWhat the harness catches, and what took a third observeridentical operator set, identical campaign, one mutant of differenceSOURCEevidence/fuzz-0002.jsonLOCKSTEPinvariance relations and F1 onlythe fold reversal is not a function of the schedule,so the engine agrees with itself and both pass9 of 10 killedO1O2O3O4O5O6O7O8O9O10with golden bytesa committed sha256 over raw fp16 logit bytes,compared exactly, from outside the process10 of 10 killedO1O2O3O4O5O6O7O8O9O10the one mutant that separates the two rows:reversed split-combine foldevery operator fires a sentinel from inside the mutant body, so no trial here is a mutant that never ran. path executed,patch executed and fault injected are three claims, and the counters can only tell you about the first. \ No newline at end of file diff --git a/docs/img/mutation-light.svg b/docs/img/mutation-light.svg index a9fddba..73b3528 100644 --- a/docs/img/mutation-light.svg +++ b/docs/img/mutation-light.svg @@ -1,146 +1 @@ - -Mutation campaign, with and without golden bytes -Ten mutation operators. Nine killed by the invariance relations and F1 alone, with the reversed split-combine fold surviving. Ten killed once golden bytes are added as an observer outside the process. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -CLAIM 2 HARNESS POWER - - - - -What the harness catches, and what took a third observer -identical operator set, identical campaign, one mutant of difference - - - - - - - - - - - - - - - - - - - - - - - -SOURCE -evidence/fuzz-0002.json -LOCKSTEP - -invariance relations and F1 only -the fold reversal is not a function of the schedule, -so the engine agrees with itself and both pass - -9 of 10 killed - - -O1 - - -O2 - - -O3 - - -O4 - - -O5 - - -O6 - - -O7 - - -O8 - - -O9 - - - -O10 - -with golden bytes -a committed sha256 over raw fp16 logit bytes, -compared exactly, from outside the process - -10 of 10 killed - - -O1 - - -O2 - - -O3 - - -O4 - - -O5 - - -O6 - - -O7 - - -O8 - - -O9 - - -O10 - -the one mutant that separates the two rows: -reversed split-combine fold -every operator fires a sentinel from inside the mutant body, so no trial here is a mutant that never ran. path executed, -patch executed and fault injected are three claims, and the counters can only tell you about the first. - +Mutation campaign, with and without golden bytesTen mutation operators. Nine killed by the invariance relations and F1 alone, with the reversed split-combine fold surviving. Ten killed once golden bytes are added as an observer outside the process.CLAIM 2 HARNESS POWERWhat the harness catches, and what took a third observeridentical operator set, identical campaign, one mutant of differenceSOURCEevidence/fuzz-0002.jsonLOCKSTEPinvariance relations and F1 onlythe fold reversal is not a function of the schedule,so the engine agrees with itself and both pass9 of 10 killedO1O2O3O4O5O6O7O8O9O10with golden bytesa committed sha256 over raw fp16 logit bytes,compared exactly, from outside the process10 of 10 killedO1O2O3O4O5O6O7O8O9O10the one mutant that separates the two rows:reversed split-combine foldevery operator fires a sentinel from inside the mutant body, so no trial here is a mutant that never ran. path executed,patch executed and fault injected are three claims, and the counters can only tell you about the first. \ No newline at end of file diff --git a/docs/img/observers-dark.svg b/docs/img/observers-dark.svg index 5a5599f..7106c6b 100644 --- a/docs/img/observers-dark.svg +++ b/docs/img/observers-dark.svg @@ -1,59 +1 @@ - - - - - - - - - - - - what each observer actually reads - - - I1 to I4 - - F1 - - golden bytes - - - - - - - model.forward - the batch-1 contiguous path - - - three observers, - one shared blind spot: - none of them reads - the path that serves - - - the scheduler - - - model.forward_batch - every served request goes here - - - PATH-EQ - - asserts the two agree, - bitwise, at every position - - - must be identical - +what each observer actually readsI1 to I4F1golden bytesmodel.forwardthe batch-1 contiguous paththree observers,one shared blind spot:none of them readsthe path that servesthe schedulermodel.forward_batchevery served request goes herePATH-EQasserts the two agree,bitwise, at every positionmust be identical \ No newline at end of file diff --git a/docs/img/observers-light.svg b/docs/img/observers-light.svg index 853c054..93e1b53 100644 --- a/docs/img/observers-light.svg +++ b/docs/img/observers-light.svg @@ -1,59 +1 @@ - - - - - - - - - - - - what each observer actually reads - - - I1 to I4 - - F1 - - golden bytes - - - - - - - model.forward - the batch-1 contiguous path - - - three observers, - one shared blind spot: - none of them reads - the path that serves - - - the scheduler - - - model.forward_batch - every served request goes here - - - PATH-EQ - - asserts the two agree, - bitwise, at every position - - - must be identical - +what each observer actually readsI1 to I4F1golden bytesmodel.forwardthe batch-1 contiguous paththree observers,one shared blind spot:none of them readsthe path that servesthe schedulermodel.forward_batchevery served request goes herePATH-EQasserts the two agree,bitwise, at every positionmust be identical \ No newline at end of file diff --git a/docs/img/thesis-dark.svg b/docs/img/thesis-dark.svg index 2e9a21e..61c140d 100644 --- a/docs/img/thesis-dark.svg +++ b/docs/img/thesis-dark.svg @@ -1,173 +1 @@ - -Seventeen findings, laned by who found them -Eighteen tiles for seventeen findings, laned by who found them: eight from this project's own machinery, five from an outside audit, one from an anomaly, two from readers not looking for defects, and two from this project auditing itself later. Findings 9 to 15 came from outside the repository. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -THE THESIS, ON ITS AUTHOR - - - - -Seventeen times this repository declared more surface than it tested -placed by finding index, laned by who found it - - - - - - - - - - - - - - - - - - - - - - - - - -SOURCE -README.md :: tests/test_thesis_table.py -LOCKSTEP - -FOUND FROM OUTSIDE - - -8 -own machinery -a run contradicting a declaration - - -5 -outside audit -commissioned, looking for defects - - -1 -an anomaly -predicted by neither side - - -2 -readers -not looking for defects at all - - -2 -self-audit, later -once it knew where to look - -1 - -2 - -3 - -4 - -5 - -6 - -7 - -8 - -9 - -10 - -11 - -12 - -12b - -13 - -14 - -15 - -16 - -17 - - -1 - -2 - -3 - -4 - -5 - -6 - -7 - -8 - -9 - -10 - -11 - -12 - -12b - -13 - -14 - -15 - -16 - -17 -finding index -eighteen tiles, seventeen findings: 12b is a row and not a count, because the audit named it outright and the witness check only -reproduced it from a different direction. counting it as new would inflate the one table whose only value is that it does not. - +Seventeen findings, laned by who found themEighteen tiles for seventeen findings, laned by who found them: eight from this project's own machinery, five from an outside audit, one from an anomaly, two from readers not looking for defects, and two from this project auditing itself later. Findings 9 to 15 came from outside the repository.THE THESIS, ON ITS AUTHORSeventeen times this repository declared more surface than it testedplaced by finding index, laned by who found itSOURCEREADME.md :: tests/test_thesis_table.pyLOCKSTEPFOUND FROM OUTSIDE8own machinerya run contradicting a declaration5outside auditcommissioned, looking for defects1an anomalypredicted by neither side2readersnot looking for defects at all2self-audit, lateronce it knew where to look12345678910111212b131415161712345678910111212b1314151617finding indexeighteen tiles, seventeen findings: 12b is a row and not a count, because the audit named it outright and the witness check onlyreproduced it from a different direction. counting it as new would inflate the one table whose only value is that it does not. \ No newline at end of file diff --git a/docs/img/thesis-light.svg b/docs/img/thesis-light.svg index 10f671d..3beba8d 100644 --- a/docs/img/thesis-light.svg +++ b/docs/img/thesis-light.svg @@ -1,173 +1 @@ - -Seventeen findings, laned by who found them -Eighteen tiles for seventeen findings, laned by who found them: eight from this project's own machinery, five from an outside audit, one from an anomaly, two from readers not looking for defects, and two from this project auditing itself later. Findings 9 to 15 came from outside the repository. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -THE THESIS, ON ITS AUTHOR - - - - -Seventeen times this repository declared more surface than it tested -placed by finding index, laned by who found it - - - - - - - - - - - - - - - - - - - - - - - - - -SOURCE -README.md :: tests/test_thesis_table.py -LOCKSTEP - -FOUND FROM OUTSIDE - - -8 -own machinery -a run contradicting a declaration - - -5 -outside audit -commissioned, looking for defects - - -1 -an anomaly -predicted by neither side - - -2 -readers -not looking for defects at all - - -2 -self-audit, later -once it knew where to look - -1 - -2 - -3 - -4 - -5 - -6 - -7 - -8 - -9 - -10 - -11 - -12 - -12b - -13 - -14 - -15 - -16 - -17 - - -1 - -2 - -3 - -4 - -5 - -6 - -7 - -8 - -9 - -10 - -11 - -12 - -12b - -13 - -14 - -15 - -16 - -17 -finding index -eighteen tiles, seventeen findings: 12b is a row and not a count, because the audit named it outright and the witness check only -reproduced it from a different direction. counting it as new would inflate the one table whose only value is that it does not. - +Seventeen findings, laned by who found themEighteen tiles for seventeen findings, laned by who found them: eight from this project's own machinery, five from an outside audit, one from an anomaly, two from readers not looking for defects, and two from this project auditing itself later. Findings 9 to 15 came from outside the repository.THE THESIS, ON ITS AUTHORSeventeen times this repository declared more surface than it testedplaced by finding index, laned by who found itSOURCEREADME.md :: tests/test_thesis_table.pyLOCKSTEPFOUND FROM OUTSIDE8own machinerya run contradicting a declaration5outside auditcommissioned, looking for defects1an anomalypredicted by neither side2readersnot looking for defects at all2self-audit, lateronce it knew where to look12345678910111212b131415161712345678910111212b1314151617finding indexeighteen tiles, seventeen findings: 12b is a row and not a count, because the audit named it outright and the witness check onlyreproduced it from a different direction. counting it as new would inflate the one table whose only value is that it does not. \ No newline at end of file diff --git a/docs/img/three-numbers-dark.svg b/docs/img/three-numbers-dark.svg index 6bd6d28..6132d56 100644 --- a/docs/img/three-numbers-dark.svg +++ b/docs/img/three-numbers-dark.svg @@ -1,132 +1 @@ - -The three headline numbers -65 of 65 relation runs bitwise identical, 10 of 10 seeded faults killed with none equivalent, and lockstep invariant running at 5.2 to 5.7 times the wall time of vLLM batch-invariant in eager mode. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -HEADLINE - - - -The three numbers -invariance, harness power, and the price of the constraint - - - - - - - - - - - - - - - - - -SOURCE -evidence/verify-0002.json :: fuzz-0002.json :: throughput-0004.json -LOCKSTEP - - -INVARIANCE -65/65 - - - - - - - - - - - - - - - - - - - - -relation runs, bitwise identical -13 relations across 5 block sizes -MR1 to MR8, PATH-EQ, EOS finish - - -HARNESS POWER -10/10 - - - - - - - - - - - - - - - - - - - - -seeded faults killed -0 equivalent, 0 not-exercised -median time to detection 10.6 s - - -COST -5.2to5.7 - - -0x - -2x - -4x - -6x - -x vLLM batch-invariant, eager -1.05x to 1.10x vs its own fast path -two runs, reported as a range - +The three headline numbers65 of 65 relation runs bitwise identical, 10 of 10 seeded faults killed with none equivalent, and lockstep invariant running at 5.2 to 5.7 times the wall time of vLLM batch-invariant in eager mode.HEADLINEThe three numbersinvariance, harness power, and the price of the constraintSOURCEevidence/verify-0002.json :: fuzz-0002.json :: throughput-0004.jsonLOCKSTEPINVARIANCE65/65relation runs, bitwise identical13 relations across 5 block sizesMR1 to MR8, PATH-EQ, EOS finishHARNESS POWER10/10seeded faults killed0 equivalent, 0 not-exercisedmedian time to detection 10.6 sCOST5.2to5.70x2x4x6xx vLLM batch-invariant, eager1.05x to 1.10x vs its own fast pathtwo runs, reported as a range \ No newline at end of file diff --git a/docs/img/three-numbers-light.svg b/docs/img/three-numbers-light.svg index 8bb1aab..de4b19b 100644 --- a/docs/img/three-numbers-light.svg +++ b/docs/img/three-numbers-light.svg @@ -1,132 +1 @@ - -The three headline numbers -65 of 65 relation runs bitwise identical, 10 of 10 seeded faults killed with none equivalent, and lockstep invariant running at 5.2 to 5.7 times the wall time of vLLM batch-invariant in eager mode. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -HEADLINE - - - -The three numbers -invariance, harness power, and the price of the constraint - - - - - - - - - - - - - - - - - -SOURCE -evidence/verify-0002.json :: fuzz-0002.json :: throughput-0004.json -LOCKSTEP - - -INVARIANCE -65/65 - - - - - - - - - - - - - - - - - - - - -relation runs, bitwise identical -13 relations across 5 block sizes -MR1 to MR8, PATH-EQ, EOS finish - - -HARNESS POWER -10/10 - - - - - - - - - - - - - - - - - - - - -seeded faults killed -0 equivalent, 0 not-exercised -median time to detection 10.6 s - - -COST -5.2to5.7 - - -0x - -2x - -4x - -6x - -x vLLM batch-invariant, eager -1.05x to 1.10x vs its own fast path -two runs, reported as a range - +The three headline numbers65 of 65 relation runs bitwise identical, 10 of 10 seeded faults killed with none equivalent, and lockstep invariant running at 5.2 to 5.7 times the wall time of vLLM batch-invariant in eager mode.HEADLINEThe three numbersinvariance, harness power, and the price of the constraintSOURCEevidence/verify-0002.json :: fuzz-0002.json :: throughput-0004.jsonLOCKSTEPINVARIANCE65/65relation runs, bitwise identical13 relations across 5 block sizesMR1 to MR8, PATH-EQ, EOS finishHARNESS POWER10/10seeded faults killed0 equivalent, 0 not-exercisedmedian time to detection 10.6 sCOST5.2to5.70x2x4x6xx vLLM batch-invariant, eager1.05x to 1.10x vs its own fast pathtwo runs, reported as a range \ No newline at end of file diff --git a/docs/img/throughput-dark.svg b/docs/img/throughput-dark.svg index 5195d40..7638277 100644 --- a/docs/img/throughput-dark.svg +++ b/docs/img/throughput-dark.svg @@ -1,155 +1 @@ - -Wall time across six configurations, and the kill criterion -Wall time for six configurations, run A solid and run B faded: lockstep fast and invariant, and vLLM default and batch-invariant, each eager and graphed. Below, the 15 percent kill criterion, with the eager comparison at 14.6 and 16.6 percent straddling the bar and the graphed comparison at 10.6 and 11.5 percent consistently below it. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -CLAIM 3 THROUGHPUT - - - -Cost of determinism, two runs of the settled design -8 requests, 2972 tokens, median of 5 samples, every measurement in its own process - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -SOURCE -evidence/throughput-0004.json :: docs/kickoff/01-PRD.md s11 -LOCKSTEP - -0s - -1s - -2s - -3s -lockstep, fast mode - - -2.930 -2.823 -spread 1.24x -lockstep, invariant - - -3.226 -2.957 -spread 1.17x -vLLM default, eager - - -0.470 -0.490 -spread 1.27x -vLLM batch-invariant, eager - - -0.563 -0.574 -spread 1.15x -vLLM default, CUDA graphs - - -0.343 -0.341 -spread 1.08x -vLLM batch-invariant, graphs - - -0.484 -0.475 -spread 1.27x - -KILL CRITERION -set in week one, before anything was built: below 15 percent of vLLM default - - -0% - -5% - -10% - -15% - -20% - -A -B - -14.6 - -16.6 - -10.6 - -11.5 -eager -14.6 and 16.6, straddling -graphs -10.6 and 11.5, below it -the bar is finer than this -measurement can resolve -solid bar run A, faded bar run B. two runs do not establish a distribution, which is why both are drawn. - +Wall time across six configurations, and the kill criterionWall time for six configurations, run A solid and run B faded: lockstep fast and invariant, and vLLM default and batch-invariant, each eager and graphed. Below, the 15 percent kill criterion, with the eager comparison at 14.6 and 16.6 percent straddling the bar and the graphed comparison at 10.6 and 11.5 percent consistently below it.CLAIM 3 THROUGHPUTCost of determinism, two runs of the settled design8 requests, 2972 tokens, median of 5 samples, every measurement in its own processSOURCEevidence/throughput-0004.json :: docs/kickoff/01-PRD.md s11LOCKSTEP0s1s2s3slockstep, fast mode2.9302.823spread 1.24xlockstep, invariant3.2262.957spread 1.17xvLLM default, eager0.4700.490spread 1.27xvLLM batch-invariant, eager0.5630.574spread 1.15xvLLM default, CUDA graphs0.3430.341spread 1.08xvLLM batch-invariant, graphs0.4840.475spread 1.27xKILL CRITERIONset in week one, before anything was built: below 15 percent of vLLM default0%5%10%15%20%AB14.616.610.611.5eager14.6 and 16.6, straddlinggraphs10.6 and 11.5, below itthe bar is finer than thismeasurement can resolvesolid bar run A, faded bar run B. two runs do not establish a distribution, which is why both are drawn. \ No newline at end of file diff --git a/docs/img/throughput-light.svg b/docs/img/throughput-light.svg index d0edd50..873d7e3 100644 --- a/docs/img/throughput-light.svg +++ b/docs/img/throughput-light.svg @@ -1,155 +1 @@ - -Wall time across six configurations, and the kill criterion -Wall time for six configurations, run A solid and run B faded: lockstep fast and invariant, and vLLM default and batch-invariant, each eager and graphed. Below, the 15 percent kill criterion, with the eager comparison at 14.6 and 16.6 percent straddling the bar and the graphed comparison at 10.6 and 11.5 percent consistently below it. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -CLAIM 3 THROUGHPUT - - - -Cost of determinism, two runs of the settled design -8 requests, 2972 tokens, median of 5 samples, every measurement in its own process - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -SOURCE -evidence/throughput-0004.json :: docs/kickoff/01-PRD.md s11 -LOCKSTEP - -0s - -1s - -2s - -3s -lockstep, fast mode - - -2.930 -2.823 -spread 1.24x -lockstep, invariant - - -3.226 -2.957 -spread 1.17x -vLLM default, eager - - -0.470 -0.490 -spread 1.27x -vLLM batch-invariant, eager - - -0.563 -0.574 -spread 1.15x -vLLM default, CUDA graphs - - -0.343 -0.341 -spread 1.08x -vLLM batch-invariant, graphs - - -0.484 -0.475 -spread 1.27x - -KILL CRITERION -set in week one, before anything was built: below 15 percent of vLLM default - - -0% - -5% - -10% - -15% - -20% - -A -B - -14.6 - -16.6 - -10.6 - -11.5 -eager -14.6 and 16.6, straddling -graphs -10.6 and 11.5, below it -the bar is finer than this -measurement can resolve -solid bar run A, faded bar run B. two runs do not establish a distribution, which is why both are drawn. - +Wall time across six configurations, and the kill criterionWall time for six configurations, run A solid and run B faded: lockstep fast and invariant, and vLLM default and batch-invariant, each eager and graphed. Below, the 15 percent kill criterion, with the eager comparison at 14.6 and 16.6 percent straddling the bar and the graphed comparison at 10.6 and 11.5 percent consistently below it.CLAIM 3 THROUGHPUTCost of determinism, two runs of the settled design8 requests, 2972 tokens, median of 5 samples, every measurement in its own processSOURCEevidence/throughput-0004.json :: docs/kickoff/01-PRD.md s11LOCKSTEP0s1s2s3slockstep, fast mode2.9302.823spread 1.24xlockstep, invariant3.2262.957spread 1.17xvLLM default, eager0.4700.490spread 1.27xvLLM batch-invariant, eager0.5630.574spread 1.15xvLLM default, CUDA graphs0.3430.341spread 1.08xvLLM batch-invariant, graphs0.4840.475spread 1.27xKILL CRITERIONset in week one, before anything was built: below 15 percent of vLLM default0%5%10%15%20%AB14.616.610.611.5eager14.6 and 16.6, straddlinggraphs10.6 and 11.5, below itthe bar is finer than thismeasurement can resolvesolid bar run A, faded bar run B. two runs do not establish a distribution, which is why both are drawn. \ No newline at end of file diff --git a/readme-assets/certification-dark.svg b/readme-assets/certification-dark.svg index 99235bd..4c707f8 100644 --- a/readme-assets/certification-dark.svg +++ b/readme-assets/certification-dark.svg @@ -1,161 +1 @@ - -vLLM certification across seven boundary cases -Seven boundary cases against vLLM batch-invariant mode: five clean, and two diverged at 44 and 45 co-resident with logprob deltas of 4.685e-02 and 3.906e-02 and no token divergence. The max-num-seqs control restores reproducibility at 8. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -CERTIFICATION - - - - -Black-box differential testing of vLLM batch-invariant mode -concurrent submission, co-residency read from the engine's own gauge, every pair of repeats compared - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -SOURCE -evidence/certify-pairs-{a,b,mns8}.json :: vllm-project/vllm#51187 -LOCKSTEP -BOUNDARY CASE -CO-RESIDENT -VERDICT - -prefix_len == block_size - 1 - - -15 - - -clean - -prefix_len == block_size - - -15 - - -clean - -prefix_len == block_size + 1 - - -15 - - -clean - -zero-prefix co-batched with nonzero - - -16 - - -clean - -cache hit covering the full prompt - - -15 - - -clean - -batch 31, shared prefix of one block - - -44 - - -diverged -max delta 4.685e-02 - -batch 32, shared prefix of one block - - -45 - - -diverged -max delta 3.906e-02 - -CONTROL -one knob, and the only controlled single-variable result in this section ---max-num-seqs 8 - -8 co-resident -1 of 5, reproducible ---max-num-seqs 64 - -45 co-resident -not reproducible ---max-num-seqs 128, the default - -45 co-resident -not reproducible, intermittently -intermittent at about one lifetime in three, so which cases trip is not the claim. token ids never move, only logprobs. filed as vllm#51187. - +vLLM certification across seven boundary casesSeven boundary cases against vLLM batch-invariant mode: five clean, and two diverged at 44 and 45 co-resident with logprob deltas of 4.685e-02 and 3.906e-02 and no token divergence. The max-num-seqs control restores reproducibility at 8.CERTIFICATIONBlack-box differential testing of vLLM batch-invariant modeconcurrent submission, co-residency read from the engine's own gauge, every pair of repeats comparedSOURCEevidence/certify-pairs-{a,b,mns8}.json :: vllm-project/vllm#51187LOCKSTEPBOUNDARY CASECO-RESIDENTVERDICTprefix_len == block_size - 115cleanprefix_len == block_size15cleanprefix_len == block_size + 115cleanzero-prefix co-batched with nonzero16cleancache hit covering the full prompt15cleanbatch 31, shared prefix of one block44divergedmax delta 4.685e-02batch 32, shared prefix of one block45divergedmax delta 3.906e-02CONTROLone knob, and the only controlled single-variable result in this section--max-num-seqs 88 co-resident1 of 5, reproducible--max-num-seqs 6445 co-residentnot reproducible--max-num-seqs 128, the default45 co-residentnot reproducible, intermittentlyintermittent at about one lifetime in three, so which cases trip is not the claim. token ids never move, only logprobs. filed as vllm#51187. \ No newline at end of file diff --git a/readme-assets/certification-light.svg b/readme-assets/certification-light.svg index 7e7ab49..5fc2083 100644 --- a/readme-assets/certification-light.svg +++ b/readme-assets/certification-light.svg @@ -1,161 +1 @@ - -vLLM certification across seven boundary cases -Seven boundary cases against vLLM batch-invariant mode: five clean, and two diverged at 44 and 45 co-resident with logprob deltas of 4.685e-02 and 3.906e-02 and no token divergence. The max-num-seqs control restores reproducibility at 8. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -CERTIFICATION - - - - -Black-box differential testing of vLLM batch-invariant mode -concurrent submission, co-residency read from the engine's own gauge, every pair of repeats compared - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -SOURCE -evidence/certify-pairs-{a,b,mns8}.json :: vllm-project/vllm#51187 -LOCKSTEP -BOUNDARY CASE -CO-RESIDENT -VERDICT - -prefix_len == block_size - 1 - - -15 - - -clean - -prefix_len == block_size - - -15 - - -clean - -prefix_len == block_size + 1 - - -15 - - -clean - -zero-prefix co-batched with nonzero - - -16 - - -clean - -cache hit covering the full prompt - - -15 - - -clean - -batch 31, shared prefix of one block - - -44 - - -diverged -max delta 4.685e-02 - -batch 32, shared prefix of one block - - -45 - - -diverged -max delta 3.906e-02 - -CONTROL -one knob, and the only controlled single-variable result in this section ---max-num-seqs 8 - -8 co-resident -1 of 5, reproducible ---max-num-seqs 64 - -45 co-resident -not reproducible ---max-num-seqs 128, the default - -45 co-resident -not reproducible, intermittently -intermittent at about one lifetime in three, so which cases trip is not the claim. token ids never move, only logprobs. filed as vllm#51187. - +vLLM certification across seven boundary casesSeven boundary cases against vLLM batch-invariant mode: five clean, and two diverged at 44 and 45 co-resident with logprob deltas of 4.685e-02 and 3.906e-02 and no token divergence. The max-num-seqs control restores reproducibility at 8.CERTIFICATIONBlack-box differential testing of vLLM batch-invariant modeconcurrent submission, co-residency read from the engine's own gauge, every pair of repeats comparedSOURCEevidence/certify-pairs-{a,b,mns8}.json :: vllm-project/vllm#51187LOCKSTEPBOUNDARY CASECO-RESIDENTVERDICTprefix_len == block_size - 115cleanprefix_len == block_size15cleanprefix_len == block_size + 115cleanzero-prefix co-batched with nonzero16cleancache hit covering the full prompt15cleanbatch 31, shared prefix of one block44divergedmax delta 4.685e-02batch 32, shared prefix of one block45divergedmax delta 3.906e-02CONTROLone knob, and the only controlled single-variable result in this section--max-num-seqs 88 co-resident1 of 5, reproducible--max-num-seqs 6445 co-residentnot reproducible--max-num-seqs 128, the default45 co-residentnot reproducible, intermittentlyintermittent at about one lifetime in three, so which cases trip is not the claim. token ids never move, only logprobs. filed as vllm#51187. \ No newline at end of file diff --git a/readme-assets/claims-dark.svg b/readme-assets/claims-dark.svg index 297b72e..4c70718 100644 --- a/readme-assets/claims-dark.svg +++ b/readme-assets/claims-dark.svg @@ -1,131 +1 @@ - -Claims I1 to I4 and F1 -Five claims with what verifies each. I1 batch invariance, I2 schedule invariance, I3 replay determinism and I4 RNG isolation all hold. F1 fidelity passes 7 of 7 bounds against an fp64 CPU reference. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -CLAIMS - - - -Five relations, and what measures each one -every claim scoped to one environment tuple, bitwise unless a tolerance is stated - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -SOURCE -evidence/verify-0002.json :: evidence/fidelity-0001.json -LOCKSTEP - - - - - -I1 -Batch invariancebit-identical to canonical, whatever cohabits -MR1, MR5 · fp16 logit bytes · batch 1 to 32 - - -holds - - - - - -I2 -Schedule invarianceany preemption, chunk partition, eviction, cache hit -MR2, MR3, MR4 · per-layer KV equality - - -holds - - - - - -I3 -Replay determinismsame (W, sigma, seeds), same trajectory hash -MR6 · 8 shapes · cross-process, differing PYTHONHASHSEED - - -holds - - - - - -I4 -RNG isolationtokens from (seed, uid, position) and own logits only -MR7 · 11 perturbations of the cohabitant set - - -holds - - - - - -F1 -Fidelitybatch-1 logits against an fp64 CPU reference -exact KL over 151936 tokens at 2756 positions - - -7 of 7 -every claim is scoped to the environment tuple in env.lock. a claim without one is invalid by construction. - +Claims I1 to I4 and F1Five claims with what verifies each. I1 batch invariance, I2 schedule invariance, I3 replay determinism and I4 RNG isolation all hold. F1 fidelity passes 7 of 7 bounds against an fp64 CPU reference.CLAIMSFive relations, and what measures each oneevery claim scoped to one environment tuple, bitwise unless a tolerance is statedSOURCEevidence/verify-0002.json :: evidence/fidelity-0001.jsonLOCKSTEPI1Batch invariancebit-identical to canonical, whatever cohabitsMR1, MR5 · fp16 logit bytes · batch 1 to 32holdsI2Schedule invarianceany preemption, chunk partition, eviction, cache hitMR2, MR3, MR4 · per-layer KV equalityholdsI3Replay determinismsame (W, sigma, seeds), same trajectory hashMR6 · 8 shapes · cross-process, differing PYTHONHASHSEEDholdsI4RNG isolationtokens from (seed, uid, position) and own logits onlyMR7 · 11 perturbations of the cohabitant setholdsF1Fidelitybatch-1 logits against an fp64 CPU referenceexact KL over 151936 tokens at 2756 positions7 of 7every claim is scoped to the environment tuple in env.lock. a claim without one is invalid by construction. \ No newline at end of file diff --git a/readme-assets/claims-light.svg b/readme-assets/claims-light.svg index d097fbe..9a01bc7 100644 --- a/readme-assets/claims-light.svg +++ b/readme-assets/claims-light.svg @@ -1,131 +1 @@ - -Claims I1 to I4 and F1 -Five claims with what verifies each. I1 batch invariance, I2 schedule invariance, I3 replay determinism and I4 RNG isolation all hold. F1 fidelity passes 7 of 7 bounds against an fp64 CPU reference. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -CLAIMS - - - -Five relations, and what measures each one -every claim scoped to one environment tuple, bitwise unless a tolerance is stated - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -SOURCE -evidence/verify-0002.json :: evidence/fidelity-0001.json -LOCKSTEP - - - - - -I1 -Batch invariancebit-identical to canonical, whatever cohabits -MR1, MR5 · fp16 logit bytes · batch 1 to 32 - - -holds - - - - - -I2 -Schedule invarianceany preemption, chunk partition, eviction, cache hit -MR2, MR3, MR4 · per-layer KV equality - - -holds - - - - - -I3 -Replay determinismsame (W, sigma, seeds), same trajectory hash -MR6 · 8 shapes · cross-process, differing PYTHONHASHSEED - - -holds - - - - - -I4 -RNG isolationtokens from (seed, uid, position) and own logits only -MR7 · 11 perturbations of the cohabitant set - - -holds - - - - - -F1 -Fidelitybatch-1 logits against an fp64 CPU reference -exact KL over 151936 tokens at 2756 positions - - -7 of 7 -every claim is scoped to the environment tuple in env.lock. a claim without one is invalid by construction. - +Claims I1 to I4 and F1Five claims with what verifies each. I1 batch invariance, I2 schedule invariance, I3 replay determinism and I4 RNG isolation all hold. F1 fidelity passes 7 of 7 bounds against an fp64 CPU reference.CLAIMSFive relations, and what measures each oneevery claim scoped to one environment tuple, bitwise unless a tolerance is statedSOURCEevidence/verify-0002.json :: evidence/fidelity-0001.jsonLOCKSTEPI1Batch invariancebit-identical to canonical, whatever cohabitsMR1, MR5 · fp16 logit bytes · batch 1 to 32holdsI2Schedule invarianceany preemption, chunk partition, eviction, cache hitMR2, MR3, MR4 · per-layer KV equalityholdsI3Replay determinismsame (W, sigma, seeds), same trajectory hashMR6 · 8 shapes · cross-process, differing PYTHONHASHSEEDholdsI4RNG isolationtokens from (seed, uid, position) and own logits onlyMR7 · 11 perturbations of the cohabitant setholdsF1Fidelitybatch-1 logits against an fp64 CPU referenceexact KL over 151936 tokens at 2756 positions7 of 7every claim is scoped to the environment tuple in env.lock. a claim without one is invalid by construction. \ No newline at end of file diff --git a/readme-assets/coverage-dark.svg b/readme-assets/coverage-dark.svg index ed1d4fd..3edd503 100644 --- a/readme-assets/coverage-dark.svg +++ b/readme-assets/coverage-dark.svg @@ -1,242 +1 @@ - -Lifecycle n-gram coverage against the corrected denominator -19 of 25 two-grams and 43 of 79 three-grams reached, split between the swarm campaign and the eviction campaign, with probe-only cells outlined and never-reached cells hatched. The denominator was corrected from 27 and 84. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -COVERAGE - - - -Lifecycle n-grams, against the real denominator -reported by population, because a case built to reach a transition is not exploration - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -SOURCE -evidence/fuzz-0002.json :: scripts/verify_no_gpu.py -LOCKSTEP -2-GRAMS -19 of 25 -probes reach 20 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -3-GRAMS -43 of 79 -probes reach 46 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -DENOMINATOR -27 and 84 - --> -25 and 79 -one declared transition was never reachable -every percentage published before the correction was computed against a denominator that was too large. -the correction moves them up, 55.6 to 60.0 percent on 2-grams at identical observed counts, which is exactly why it is stated here. - -swarm campaign, 72 cases - -plus eviction, 132 cases - -targeted probe only - - -never reached - +Lifecycle n-gram coverage against the corrected denominator19 of 25 two-grams and 43 of 79 three-grams reached, split between the swarm campaign and the eviction campaign, with probe-only cells outlined and never-reached cells hatched. The denominator was corrected from 27 and 84.COVERAGELifecycle n-grams, against the real denominatorreported by population, because a case built to reach a transition is not explorationSOURCEevidence/fuzz-0002.json :: scripts/verify_no_gpu.pyLOCKSTEP2-GRAMS19 of 25probes reach 203-GRAMS43 of 79probes reach 46DENOMINATOR27 and 84->25 and 79one declared transition was never reachableevery percentage published before the correction was computed against a denominator that was too large.the correction moves them up, 55.6 to 60.0 percent on 2-grams at identical observed counts, which is exactly why it is stated here.swarm campaign, 72 casesplus eviction, 132 casestargeted probe onlynever reached \ No newline at end of file diff --git a/readme-assets/coverage-light.svg b/readme-assets/coverage-light.svg index fe1b3f9..f36259f 100644 --- a/readme-assets/coverage-light.svg +++ b/readme-assets/coverage-light.svg @@ -1,242 +1 @@ - -Lifecycle n-gram coverage against the corrected denominator -19 of 25 two-grams and 43 of 79 three-grams reached, split between the swarm campaign and the eviction campaign, with probe-only cells outlined and never-reached cells hatched. The denominator was corrected from 27 and 84. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -COVERAGE - - - -Lifecycle n-grams, against the real denominator -reported by population, because a case built to reach a transition is not exploration - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -SOURCE -evidence/fuzz-0002.json :: scripts/verify_no_gpu.py -LOCKSTEP -2-GRAMS -19 of 25 -probes reach 20 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -3-GRAMS -43 of 79 -probes reach 46 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -DENOMINATOR -27 and 84 - --> -25 and 79 -one declared transition was never reachable -every percentage published before the correction was computed against a denominator that was too large. -the correction moves them up, 55.6 to 60.0 percent on 2-grams at identical observed counts, which is exactly why it is stated here. - -swarm campaign, 72 cases - -plus eviction, 132 cases - -targeted probe only - - -never reached - +Lifecycle n-gram coverage against the corrected denominator19 of 25 two-grams and 43 of 79 three-grams reached, split between the swarm campaign and the eviction campaign, with probe-only cells outlined and never-reached cells hatched. The denominator was corrected from 27 and 84.COVERAGELifecycle n-grams, against the real denominatorreported by population, because a case built to reach a transition is not explorationSOURCEevidence/fuzz-0002.json :: scripts/verify_no_gpu.pyLOCKSTEP2-GRAMS19 of 25probes reach 203-GRAMS43 of 79probes reach 46DENOMINATOR27 and 84->25 and 79one declared transition was never reachableevery percentage published before the correction was computed against a denominator that was too large.the correction moves them up, 55.6 to 60.0 percent on 2-grams at identical observed counts, which is exactly why it is stated here.swarm campaign, 72 casesplus eviction, 132 casestargeted probe onlynever reached \ No newline at end of file diff --git a/readme-assets/mutation-dark.svg b/readme-assets/mutation-dark.svg index 787b12d..28db3e6 100644 --- a/readme-assets/mutation-dark.svg +++ b/readme-assets/mutation-dark.svg @@ -1,146 +1 @@ - -Mutation campaign, with and without golden bytes -Ten mutation operators. Nine killed by the invariance relations and F1 alone, with the reversed split-combine fold surviving. Ten killed once golden bytes are added as an observer outside the process. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -CLAIM 2 HARNESS POWER - - - - -What the harness catches, and what took a third observer -identical operator set, identical campaign, one mutant of difference - - - - - - - - - - - - - - - - - - - - - - - -SOURCE -evidence/fuzz-0002.json -LOCKSTEP - -invariance relations and F1 only -the fold reversal is not a function of the schedule, -so the engine agrees with itself and both pass - -9 of 10 killed - - -O1 - - -O2 - - -O3 - - -O4 - - -O5 - - -O6 - - -O7 - - -O8 - - -O9 - - - -O10 - -with golden bytes -a committed sha256 over raw fp16 logit bytes, -compared exactly, from outside the process - -10 of 10 killed - - -O1 - - -O2 - - -O3 - - -O4 - - -O5 - - -O6 - - -O7 - - -O8 - - -O9 - - -O10 - -the one mutant that separates the two rows: -reversed split-combine fold -every operator fires a sentinel from inside the mutant body, so no trial here is a mutant that never ran. path executed, -patch executed and fault injected are three claims, and the counters can only tell you about the first. - +Mutation campaign, with and without golden bytesTen mutation operators. Nine killed by the invariance relations and F1 alone, with the reversed split-combine fold surviving. Ten killed once golden bytes are added as an observer outside the process.CLAIM 2 HARNESS POWERWhat the harness catches, and what took a third observeridentical operator set, identical campaign, one mutant of differenceSOURCEevidence/fuzz-0002.jsonLOCKSTEPinvariance relations and F1 onlythe fold reversal is not a function of the schedule,so the engine agrees with itself and both pass9 of 10 killedO1O2O3O4O5O6O7O8O9O10with golden bytesa committed sha256 over raw fp16 logit bytes,compared exactly, from outside the process10 of 10 killedO1O2O3O4O5O6O7O8O9O10the one mutant that separates the two rows:reversed split-combine foldevery operator fires a sentinel from inside the mutant body, so no trial here is a mutant that never ran. path executed,patch executed and fault injected are three claims, and the counters can only tell you about the first. \ No newline at end of file diff --git a/readme-assets/mutation-light.svg b/readme-assets/mutation-light.svg index a9fddba..73b3528 100644 --- a/readme-assets/mutation-light.svg +++ b/readme-assets/mutation-light.svg @@ -1,146 +1 @@ - -Mutation campaign, with and without golden bytes -Ten mutation operators. Nine killed by the invariance relations and F1 alone, with the reversed split-combine fold surviving. Ten killed once golden bytes are added as an observer outside the process. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -CLAIM 2 HARNESS POWER - - - - -What the harness catches, and what took a third observer -identical operator set, identical campaign, one mutant of difference - - - - - - - - - - - - - - - - - - - - - - - -SOURCE -evidence/fuzz-0002.json -LOCKSTEP - -invariance relations and F1 only -the fold reversal is not a function of the schedule, -so the engine agrees with itself and both pass - -9 of 10 killed - - -O1 - - -O2 - - -O3 - - -O4 - - -O5 - - -O6 - - -O7 - - -O8 - - -O9 - - - -O10 - -with golden bytes -a committed sha256 over raw fp16 logit bytes, -compared exactly, from outside the process - -10 of 10 killed - - -O1 - - -O2 - - -O3 - - -O4 - - -O5 - - -O6 - - -O7 - - -O8 - - -O9 - - -O10 - -the one mutant that separates the two rows: -reversed split-combine fold -every operator fires a sentinel from inside the mutant body, so no trial here is a mutant that never ran. path executed, -patch executed and fault injected are three claims, and the counters can only tell you about the first. - +Mutation campaign, with and without golden bytesTen mutation operators. Nine killed by the invariance relations and F1 alone, with the reversed split-combine fold surviving. Ten killed once golden bytes are added as an observer outside the process.CLAIM 2 HARNESS POWERWhat the harness catches, and what took a third observeridentical operator set, identical campaign, one mutant of differenceSOURCEevidence/fuzz-0002.jsonLOCKSTEPinvariance relations and F1 onlythe fold reversal is not a function of the schedule,so the engine agrees with itself and both pass9 of 10 killedO1O2O3O4O5O6O7O8O9O10with golden bytesa committed sha256 over raw fp16 logit bytes,compared exactly, from outside the process10 of 10 killedO1O2O3O4O5O6O7O8O9O10the one mutant that separates the two rows:reversed split-combine foldevery operator fires a sentinel from inside the mutant body, so no trial here is a mutant that never ran. path executed,patch executed and fault injected are three claims, and the counters can only tell you about the first. \ No newline at end of file diff --git a/readme-assets/thesis-dark.svg b/readme-assets/thesis-dark.svg index 2e9a21e..61c140d 100644 --- a/readme-assets/thesis-dark.svg +++ b/readme-assets/thesis-dark.svg @@ -1,173 +1 @@ - -Seventeen findings, laned by who found them -Eighteen tiles for seventeen findings, laned by who found them: eight from this project's own machinery, five from an outside audit, one from an anomaly, two from readers not looking for defects, and two from this project auditing itself later. Findings 9 to 15 came from outside the repository. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -THE THESIS, ON ITS AUTHOR - - - - -Seventeen times this repository declared more surface than it tested -placed by finding index, laned by who found it - - - - - - - - - - - - - - - - - - - - - - - - - -SOURCE -README.md :: tests/test_thesis_table.py -LOCKSTEP - -FOUND FROM OUTSIDE - - -8 -own machinery -a run contradicting a declaration - - -5 -outside audit -commissioned, looking for defects - - -1 -an anomaly -predicted by neither side - - -2 -readers -not looking for defects at all - - -2 -self-audit, later -once it knew where to look - -1 - -2 - -3 - -4 - -5 - -6 - -7 - -8 - -9 - -10 - -11 - -12 - -12b - -13 - -14 - -15 - -16 - -17 - - -1 - -2 - -3 - -4 - -5 - -6 - -7 - -8 - -9 - -10 - -11 - -12 - -12b - -13 - -14 - -15 - -16 - -17 -finding index -eighteen tiles, seventeen findings: 12b is a row and not a count, because the audit named it outright and the witness check only -reproduced it from a different direction. counting it as new would inflate the one table whose only value is that it does not. - +Seventeen findings, laned by who found themEighteen tiles for seventeen findings, laned by who found them: eight from this project's own machinery, five from an outside audit, one from an anomaly, two from readers not looking for defects, and two from this project auditing itself later. Findings 9 to 15 came from outside the repository.THE THESIS, ON ITS AUTHORSeventeen times this repository declared more surface than it testedplaced by finding index, laned by who found itSOURCEREADME.md :: tests/test_thesis_table.pyLOCKSTEPFOUND FROM OUTSIDE8own machinerya run contradicting a declaration5outside auditcommissioned, looking for defects1an anomalypredicted by neither side2readersnot looking for defects at all2self-audit, lateronce it knew where to look12345678910111212b131415161712345678910111212b1314151617finding indexeighteen tiles, seventeen findings: 12b is a row and not a count, because the audit named it outright and the witness check onlyreproduced it from a different direction. counting it as new would inflate the one table whose only value is that it does not. \ No newline at end of file diff --git a/readme-assets/thesis-light.svg b/readme-assets/thesis-light.svg index 10f671d..3beba8d 100644 --- a/readme-assets/thesis-light.svg +++ b/readme-assets/thesis-light.svg @@ -1,173 +1 @@ - -Seventeen findings, laned by who found them -Eighteen tiles for seventeen findings, laned by who found them: eight from this project's own machinery, five from an outside audit, one from an anomaly, two from readers not looking for defects, and two from this project auditing itself later. Findings 9 to 15 came from outside the repository. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -THE THESIS, ON ITS AUTHOR - - - - -Seventeen times this repository declared more surface than it tested -placed by finding index, laned by who found it - - - - - - - - - - - - - - - - - - - - - - - - - -SOURCE -README.md :: tests/test_thesis_table.py -LOCKSTEP - -FOUND FROM OUTSIDE - - -8 -own machinery -a run contradicting a declaration - - -5 -outside audit -commissioned, looking for defects - - -1 -an anomaly -predicted by neither side - - -2 -readers -not looking for defects at all - - -2 -self-audit, later -once it knew where to look - -1 - -2 - -3 - -4 - -5 - -6 - -7 - -8 - -9 - -10 - -11 - -12 - -12b - -13 - -14 - -15 - -16 - -17 - - -1 - -2 - -3 - -4 - -5 - -6 - -7 - -8 - -9 - -10 - -11 - -12 - -12b - -13 - -14 - -15 - -16 - -17 -finding index -eighteen tiles, seventeen findings: 12b is a row and not a count, because the audit named it outright and the witness check only -reproduced it from a different direction. counting it as new would inflate the one table whose only value is that it does not. - +Seventeen findings, laned by who found themEighteen tiles for seventeen findings, laned by who found them: eight from this project's own machinery, five from an outside audit, one from an anomaly, two from readers not looking for defects, and two from this project auditing itself later. Findings 9 to 15 came from outside the repository.THE THESIS, ON ITS AUTHORSeventeen times this repository declared more surface than it testedplaced by finding index, laned by who found itSOURCEREADME.md :: tests/test_thesis_table.pyLOCKSTEPFOUND FROM OUTSIDE8own machinerya run contradicting a declaration5outside auditcommissioned, looking for defects1an anomalypredicted by neither side2readersnot looking for defects at all2self-audit, lateronce it knew where to look12345678910111212b131415161712345678910111212b1314151617finding indexeighteen tiles, seventeen findings: 12b is a row and not a count, because the audit named it outright and the witness check onlyreproduced it from a different direction. counting it as new would inflate the one table whose only value is that it does not. \ No newline at end of file diff --git a/readme-assets/three-numbers-dark.svg b/readme-assets/three-numbers-dark.svg index 6bd6d28..6132d56 100644 --- a/readme-assets/three-numbers-dark.svg +++ b/readme-assets/three-numbers-dark.svg @@ -1,132 +1 @@ - -The three headline numbers -65 of 65 relation runs bitwise identical, 10 of 10 seeded faults killed with none equivalent, and lockstep invariant running at 5.2 to 5.7 times the wall time of vLLM batch-invariant in eager mode. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -HEADLINE - - - -The three numbers -invariance, harness power, and the price of the constraint - - - - - - - - - - - - - - - - - -SOURCE -evidence/verify-0002.json :: fuzz-0002.json :: throughput-0004.json -LOCKSTEP - - -INVARIANCE -65/65 - - - - - - - - - - - - - - - - - - - - -relation runs, bitwise identical -13 relations across 5 block sizes -MR1 to MR8, PATH-EQ, EOS finish - - -HARNESS POWER -10/10 - - - - - - - - - - - - - - - - - - - - -seeded faults killed -0 equivalent, 0 not-exercised -median time to detection 10.6 s - - -COST -5.2to5.7 - - -0x - -2x - -4x - -6x - -x vLLM batch-invariant, eager -1.05x to 1.10x vs its own fast path -two runs, reported as a range - +The three headline numbers65 of 65 relation runs bitwise identical, 10 of 10 seeded faults killed with none equivalent, and lockstep invariant running at 5.2 to 5.7 times the wall time of vLLM batch-invariant in eager mode.HEADLINEThe three numbersinvariance, harness power, and the price of the constraintSOURCEevidence/verify-0002.json :: fuzz-0002.json :: throughput-0004.jsonLOCKSTEPINVARIANCE65/65relation runs, bitwise identical13 relations across 5 block sizesMR1 to MR8, PATH-EQ, EOS finishHARNESS POWER10/10seeded faults killed0 equivalent, 0 not-exercisedmedian time to detection 10.6 sCOST5.2to5.70x2x4x6xx vLLM batch-invariant, eager1.05x to 1.10x vs its own fast pathtwo runs, reported as a range \ No newline at end of file diff --git a/readme-assets/three-numbers-light.svg b/readme-assets/three-numbers-light.svg index 8bb1aab..de4b19b 100644 --- a/readme-assets/three-numbers-light.svg +++ b/readme-assets/three-numbers-light.svg @@ -1,132 +1 @@ - -The three headline numbers -65 of 65 relation runs bitwise identical, 10 of 10 seeded faults killed with none equivalent, and lockstep invariant running at 5.2 to 5.7 times the wall time of vLLM batch-invariant in eager mode. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -HEADLINE - - - -The three numbers -invariance, harness power, and the price of the constraint - - - - - - - - - - - - - - - - - -SOURCE -evidence/verify-0002.json :: fuzz-0002.json :: throughput-0004.json -LOCKSTEP - - -INVARIANCE -65/65 - - - - - - - - - - - - - - - - - - - - -relation runs, bitwise identical -13 relations across 5 block sizes -MR1 to MR8, PATH-EQ, EOS finish - - -HARNESS POWER -10/10 - - - - - - - - - - - - - - - - - - - - -seeded faults killed -0 equivalent, 0 not-exercised -median time to detection 10.6 s - - -COST -5.2to5.7 - - -0x - -2x - -4x - -6x - -x vLLM batch-invariant, eager -1.05x to 1.10x vs its own fast path -two runs, reported as a range - +The three headline numbers65 of 65 relation runs bitwise identical, 10 of 10 seeded faults killed with none equivalent, and lockstep invariant running at 5.2 to 5.7 times the wall time of vLLM batch-invariant in eager mode.HEADLINEThe three numbersinvariance, harness power, and the price of the constraintSOURCEevidence/verify-0002.json :: fuzz-0002.json :: throughput-0004.jsonLOCKSTEPINVARIANCE65/65relation runs, bitwise identical13 relations across 5 block sizesMR1 to MR8, PATH-EQ, EOS finishHARNESS POWER10/10seeded faults killed0 equivalent, 0 not-exercisedmedian time to detection 10.6 sCOST5.2to5.70x2x4x6xx vLLM batch-invariant, eager1.05x to 1.10x vs its own fast pathtwo runs, reported as a range \ No newline at end of file diff --git a/readme-assets/throughput-dark.svg b/readme-assets/throughput-dark.svg index 5195d40..7638277 100644 --- a/readme-assets/throughput-dark.svg +++ b/readme-assets/throughput-dark.svg @@ -1,155 +1 @@ - -Wall time across six configurations, and the kill criterion -Wall time for six configurations, run A solid and run B faded: lockstep fast and invariant, and vLLM default and batch-invariant, each eager and graphed. Below, the 15 percent kill criterion, with the eager comparison at 14.6 and 16.6 percent straddling the bar and the graphed comparison at 10.6 and 11.5 percent consistently below it. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -CLAIM 3 THROUGHPUT - - - -Cost of determinism, two runs of the settled design -8 requests, 2972 tokens, median of 5 samples, every measurement in its own process - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -SOURCE -evidence/throughput-0004.json :: docs/kickoff/01-PRD.md s11 -LOCKSTEP - -0s - -1s - -2s - -3s -lockstep, fast mode - - -2.930 -2.823 -spread 1.24x -lockstep, invariant - - -3.226 -2.957 -spread 1.17x -vLLM default, eager - - -0.470 -0.490 -spread 1.27x -vLLM batch-invariant, eager - - -0.563 -0.574 -spread 1.15x -vLLM default, CUDA graphs - - -0.343 -0.341 -spread 1.08x -vLLM batch-invariant, graphs - - -0.484 -0.475 -spread 1.27x - -KILL CRITERION -set in week one, before anything was built: below 15 percent of vLLM default - - -0% - -5% - -10% - -15% - -20% - -A -B - -14.6 - -16.6 - -10.6 - -11.5 -eager -14.6 and 16.6, straddling -graphs -10.6 and 11.5, below it -the bar is finer than this -measurement can resolve -solid bar run A, faded bar run B. two runs do not establish a distribution, which is why both are drawn. - +Wall time across six configurations, and the kill criterionWall time for six configurations, run A solid and run B faded: lockstep fast and invariant, and vLLM default and batch-invariant, each eager and graphed. Below, the 15 percent kill criterion, with the eager comparison at 14.6 and 16.6 percent straddling the bar and the graphed comparison at 10.6 and 11.5 percent consistently below it.CLAIM 3 THROUGHPUTCost of determinism, two runs of the settled design8 requests, 2972 tokens, median of 5 samples, every measurement in its own processSOURCEevidence/throughput-0004.json :: docs/kickoff/01-PRD.md s11LOCKSTEP0s1s2s3slockstep, fast mode2.9302.823spread 1.24xlockstep, invariant3.2262.957spread 1.17xvLLM default, eager0.4700.490spread 1.27xvLLM batch-invariant, eager0.5630.574spread 1.15xvLLM default, CUDA graphs0.3430.341spread 1.08xvLLM batch-invariant, graphs0.4840.475spread 1.27xKILL CRITERIONset in week one, before anything was built: below 15 percent of vLLM default0%5%10%15%20%AB14.616.610.611.5eager14.6 and 16.6, straddlinggraphs10.6 and 11.5, below itthe bar is finer than thismeasurement can resolvesolid bar run A, faded bar run B. two runs do not establish a distribution, which is why both are drawn. \ No newline at end of file diff --git a/readme-assets/throughput-light.svg b/readme-assets/throughput-light.svg index d0edd50..873d7e3 100644 --- a/readme-assets/throughput-light.svg +++ b/readme-assets/throughput-light.svg @@ -1,155 +1 @@ - -Wall time across six configurations, and the kill criterion -Wall time for six configurations, run A solid and run B faded: lockstep fast and invariant, and vLLM default and batch-invariant, each eager and graphed. Below, the 15 percent kill criterion, with the eager comparison at 14.6 and 16.6 percent straddling the bar and the graphed comparison at 10.6 and 11.5 percent consistently below it. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -CLAIM 3 THROUGHPUT - - - -Cost of determinism, two runs of the settled design -8 requests, 2972 tokens, median of 5 samples, every measurement in its own process - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -SOURCE -evidence/throughput-0004.json :: docs/kickoff/01-PRD.md s11 -LOCKSTEP - -0s - -1s - -2s - -3s -lockstep, fast mode - - -2.930 -2.823 -spread 1.24x -lockstep, invariant - - -3.226 -2.957 -spread 1.17x -vLLM default, eager - - -0.470 -0.490 -spread 1.27x -vLLM batch-invariant, eager - - -0.563 -0.574 -spread 1.15x -vLLM default, CUDA graphs - - -0.343 -0.341 -spread 1.08x -vLLM batch-invariant, graphs - - -0.484 -0.475 -spread 1.27x - -KILL CRITERION -set in week one, before anything was built: below 15 percent of vLLM default - - -0% - -5% - -10% - -15% - -20% - -A -B - -14.6 - -16.6 - -10.6 - -11.5 -eager -14.6 and 16.6, straddling -graphs -10.6 and 11.5, below it -the bar is finer than this -measurement can resolve -solid bar run A, faded bar run B. two runs do not establish a distribution, which is why both are drawn. - +Wall time across six configurations, and the kill criterionWall time for six configurations, run A solid and run B faded: lockstep fast and invariant, and vLLM default and batch-invariant, each eager and graphed. Below, the 15 percent kill criterion, with the eager comparison at 14.6 and 16.6 percent straddling the bar and the graphed comparison at 10.6 and 11.5 percent consistently below it.CLAIM 3 THROUGHPUTCost of determinism, two runs of the settled design8 requests, 2972 tokens, median of 5 samples, every measurement in its own processSOURCEevidence/throughput-0004.json :: docs/kickoff/01-PRD.md s11LOCKSTEP0s1s2s3slockstep, fast mode2.9302.823spread 1.24xlockstep, invariant3.2262.957spread 1.17xvLLM default, eager0.4700.490spread 1.27xvLLM batch-invariant, eager0.5630.574spread 1.15xvLLM default, CUDA graphs0.3430.341spread 1.08xvLLM batch-invariant, graphs0.4840.475spread 1.27xKILL CRITERIONset in week one, before anything was built: below 15 percent of vLLM default0%5%10%15%20%AB14.616.610.611.5eager14.6 and 16.6, straddlinggraphs10.6 and 11.5, below itthe bar is finer than thismeasurement can resolvesolid bar run A, faded bar run B. two runs do not establish a distribution, which is why both are drawn. \ No newline at end of file