diff --git a/src/pages/concepts/qualification.astro b/src/pages/concepts/qualification.astro index b5fc681..019924f 100644 --- a/src/pages/concepts/qualification.astro +++ b/src/pages/concepts/qualification.astro @@ -112,8 +112,9 @@ const crumbs = [
- Status as of 11 Oct 2026, flight v0.2.0. The F´ components and the C interface have numbered requirements, + Status as of 17 Oct 2026, flight v0.3.1. The F´ components and the C interface have numbered requirements, each with a verification method, but no trace to mission or standard requirements.
diff --git a/src/pages/concepts/shrinking-quorum.astro b/src/pages/concepts/shrinking-quorum.astro index b9d5436..9fcc357 100644 --- a/src/pages/concepts/shrinking-quorum.astro +++ b/src/pages/concepts/shrinking-quorum.astro @@ -9,7 +9,7 @@ const crumbs = [ { label: 'Concepts', href: '/concepts/shrinking-quorum/' }, { label: 'Shrinking quorum' }, ]; -const proofs = 'https://github.com/mruspace/flight/blob/v0.2.0/quorum/src/lib.rs'; +const proofs = 'https://github.com/mruspace/flight/blob/v0.3.1/quorum/src/lib.rs'; ---stuckbit:I@T/LOC.BIT.V: from tick T, bit BIT of LOC is forced to V (0 or 1), in both
self-check runs and in the known-answer test. LOC is in (the input, bits 0 to 63),{' '}
block (the 4 KiB working block, bits 0 to 32767), acc (the hash accumulator, 0
- to 63) or out (the result, 0 to 63). Added after v0.2.0. See{' '}
+ to 63) or out (the result, 0 to 63). Added in v0.3.0. See{' '}
known-answer test coverage.
policy=shrink ticks=20000 seed=1 upset_rate=0.001 -useful=14989 detected=11 wrong=0 halted_at=never alive_at_end=1 stopped=completed last_useful=20000 -footprint: voter_max_rss=1920KiB replica_max_rss=1808KiB cpu=0.48s wall=0.46s +useful=14989 detected=11 wrong=0 halted_at=never alive_at_end=1 stopped=completed last_useful=20000 kat_tests=174 +footprint: voter_max_rss=1936KiB replica_max_rss=1824KiB cpu=0.429s wall=0.420s limits: memory=128MB/process cpu_time=none cpu_share=none max_run=none reply_timeout=2000ms
- flight v0.2.0 on an Apple M4. The footprint line varies by host. + flight v0.3.1 on an Apple M4. The footprint line varies by host.
last_useful is the tick of the last correct result. With a scheduled stuck, hang or corrupt fault,
- the output adds a detection: line (also for stuckbit, after v0.2.0): the faults
+ the output adds a detection: line (also for stuckbit, since v0.3.0): the faults
injected, how many the voter caught, and the mean and longest ticks from fault to first reaction. The{' '}
bench runs this program over a matrix of faults.
- For the experiment registered with ESA's OPS-SAT Space Lab for OPS-SAT PRETTY (exp4051, October 2026). Nothing
- has run on the satellite yet. opssat/run is the entry point the OPS-SAT runner executes: the
- shrinking quorum and fixed TMR one after the other, same seed and fault schedule, all output in a folder for
- downlink, finished inside a five-minute window. opssat/package.sh builds the package from a
- checksum-verified release binary. opssat/run.sh starts, checks and stops a long run on any Linux
- system. Tagged releases ship each static Linux binary (three ARM, one x86_64) with both launchers, the fault
- schedules and the operations note.
+ For the experiment registered with ESA's OPS-SAT Space Lab for OPS-SAT PRETTY (exp4051, October 2026). ESA ran
+ the v0.3.1 package in its software environment on 15 October 2026, and TU Graz ran it on the PRETTY FlatSat, the
+ flight processor on the bench, on 16 October 2026. Both runs exited 0, every fault landed on its scheduled tick,
+ and no result was wrong. On the flight processor at the 5% CPU share the voter made about 45 ticks per second (
+ operations note, with the measured
+ results). Nothing has run on the satellite yet; the run in orbit is next. opssat/run is the entry
+ point the OPS-SAT runner executes: the shrinking quorum and fixed TMR one after the other, same seed and fault
+ schedule, all output in a folder for downlink, finished inside a five-minute window.{' '}
+ opssat/package.sh builds the package from a checksum-verified release binary.{' '}
+ opssat/run.sh starts, checks and stops a long run on any Linux system. Tagged releases ship each
+ static Linux binary (three ARM, one x86_64) with both launchers, the fault schedules and the operations note.
- Its output, from cargo run against v0.2.0:
+ Its output, from cargo run against v0.3.1:
[Single(7), Single(7), Single(9)]: command 7
[Absent, Single(7), Single(7)]: command 7
@@ -370,7 +370,7 @@ quorum = {'{'} git = "https://github.com/mruspace/flight"
- Each proof name links to its source at v0.2.0.
+Each proof name links to its source at v0.3.1.
F´ components around the Rust core, a C interface for other frameworks, and the operations note and - package for the registered OPS-SAT PRETTY experiment. + package for the OPS-SAT PRETTY experiment (exp4051): software environment and FlatSat tests passed, the run in + orbit next.
@@ -66,12 +67,12 @@ cargo run --release --bin quorum -- --policy shrink --ticks 20000 --seed 1 \ Run the same seed with--policy tmr to compare. The first two lines of each run:
policy=shrink ticks=20000 seed=1 upset_rate=0.001 -useful=14989 detected=11 wrong=0 halted_at=never alive_at_end=1 stopped=completed last_useful=20000 +useful=14989 detected=11 wrong=0 halted_at=never alive_at_end=1 stopped=completed last_useful=20000 kat_tests=174 policy=tmr ticks=20000 seed=1 upset_rate=0.001 -useful=9990 detected=9 wrong=0 halted_at=10000 alive_at_end=1 stopped=halted last_useful=9999+useful=9990 detected=9 wrong=0 halted_at=10000 alive_at_end=1 stopped=halted last_useful=9999 kat_tests=0
- flight v0.2.0 on an Apple M4. The counts depend only on the seed. + flight v0.3.1 on an Apple M4. The counts depend only on the seed.
Fixed TMR halts at tick 10000, when the second replica dies. The shrinking quorum keeps running on the last