Repository navigation
Proof scope, baselines, coverage, prior art and qualification path - #18
Merged
Merged
Conversation
…ints to its section Prior art lists only verified references (von Neumann, Lyons and Vanderkulk, STAR, Sklaroff, Meyer, Lamport et al., Spector and Gifford, Rasmussen) with how Mru relates to each. Qualification path maps what exists to NPR 7150.2, NASA-STD-8739.8, ECSS-E-ST-40C and ECSS-Q-ST-80C by topic and makes no compliance claim. Metadata for both, and descriptions updated for the shrinking quorum, quorum crate and Dusk pages.
…mmand path, open questions New lede without 'decides exactly as fixed TMR'. Each Kani harness is linked with its scope. Fixed TMR is framed as the baseline, not as what spacecraft fly; the Shuttle and degradable systems are cited as prior art. Adds the Degradation-First Principle and corollary (whitepaper section 5), the KAT outcomes at two replicas with their gaps, the command path, and open questions. The 1.34x states its no-ground-support assumption. A RISK-METRIC marker holds the place for Dusk's per-mission risk.
…covered, and a command gate example The gate example compiles and runs against v0.2.0; its output is pasted. F´ page: name the four functions the C interface proofs cover; null pointers are unit-tested, not proved.
…ground support section cargo run needs --bin because the package has two programs. Times are from a run on an Apple M4. Useful, service and wrong days are defined as src/model.rs computes them. The ground table is pasted from a real run and the 1.34x states that it falls to 1.00x when support never ends. A DUSK-BASELINES marker holds the place for the new baselines.
…ed; llms.txt summary Quickstart uses --bin quorum and --bin dusk (cargo run alone is ambiguous in both repos) and shows the real output lines. Bench run times measured on an Apple M4. Bench page no longer says both policies 'make the same decision'. Architecture labels Layers 0 and 2 to 5 'Not built' and the 1.34x states its ground assumption. llms.txt: no TRL, nine proofs (four core, five C interface).
…d risk, known-answer test coverage on the bench page, stuckbit in the CLI page; shared styles synced
Closed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Pages
#gateexample that gates commands onVerdict.mode(compiled and run; also in flight asquorum/examples/gate.rs).src/model.rs; new Baselines section (TMR with an unchecked fallback; cold standby swept over spare aging 0.1 to 1.0); default output from a real run; ground support section.bench/results/*-kat.json).stuckbitfault and thecorruptfix.--bin quorum/--bin dusk, with the real output.Shared files
scripts/sync-tokens.mjsnow also copiessrc/data/claims.json,src/data/claims.tsandsrc/components/Claim.astrofrom the website;check:tokensfails if they drift. The sync also bringssrc/styles/shared/site.cssup to date with website PRs #31 and #32, which had not been synced.Checks
npm run checkpasses locally against the local website. Visual check of 10 pages in light and dark at 1280 and 375 px: no overflow, no console errors.Merge order
Merge after website #34: CI's
check:tokensreads website main, so it fails here until then. The bench page links tobench/results/2026-10-11-darwin-arm64-kat.json, which exists on flight main after flight #9 merges.