G3 — the assurance matrix¶
Generated file. Do not edit. Rendered from
docs/assurance-matrix.tomlbypython tools/assurance_matrix.py --markdown. That file is the single source of truth; this page is a view of it.
G3 is collected at every gate, not frozen to a commit. A hand-kept
table with four dimensions is out of date the day it is published, so
the cells here come from executed tests and each names the node that
produced it. G1 remains separately frozen at a8e686ba.
A cell is supported only on end-to-end evidence — a unit test can
show the frontend accepts a construct while no backend ever emitted
it. unsupported/refused requires an executed negative test with a
stable typed code. not-applicable requires a semantic reason.
unmeasured names the issue that carries the gap.
Language features¶
| feature | state | why / evidence |
|---|---|---|
assurance/policy |
supported | tests/test_assurance_example_reaches_both_backends.py::test_the_assurance_example_reaches_both_backends |
compose/continuous |
supported | tests/test_examples_coverage.py::test_every_example_produces_rust_that_actually_compiles[pasteurizer/TemperaturePID.zqel] |
compose/wiring |
supported | tests/test_examples_coverage.py::test_every_example_produces_rust_that_actually_compiles[algorithms/lm_step/LMFit.zqel] |
contract/clauses |
supported | tests/test_examples_coverage.py::test_every_example_produces_rust_that_actually_compiles[algorithms/fibonacci.zqel] |
contract/rule |
supported | tests/test_examples_coverage.py::test_every_example_produces_rust_that_actually_compiles[algorithms/is_prime.zqel] |
contract/section |
supported | tests/test_examples_coverage.py::test_every_example_produces_rust_that_actually_compiles[motor_contract.zqel] |
contract/temporal |
supported | tests/test_examples_coverage.py::test_every_example_produces_rust_that_actually_compiles[algorithms/fibonacci.zqel] |
conv/explicit |
supported | tests/test_examples_coverage.py::test_every_example_produces_rust_that_actually_compiles[dint/dint_scale.zqel] |
decl/const |
supported | tests/test_examples_coverage.py::test_every_example_produces_rust_that_actually_compiles[const_limit.zqel] |
decl/parameter |
supported | tests/test_examples_coverage.py::test_every_example_produces_rust_that_actually_compiles[analog/pid.zqel] |
decl/var_sections |
supported | tests/test_examples_coverage.py::test_every_example_produces_rust_that_actually_compiles[algorithms/bubble_sort5.zqel] |
expr/aggregate |
supported | tests/test_examples_coverage.py::test_every_example_produces_rust_that_actually_compiles[algorithms/insertion_sort.zqel] |
expr/arithmetic |
supported | tests/test_examples_coverage.py::test_every_example_produces_rust_that_actually_compiles[algorithms/fibonacci.zqel] |
expr/clamp |
supported | tests/test_examples_coverage.py::test_every_example_produces_rust_that_actually_compiles[analog/flow_totalizer.zqel] |
expr/comparison |
supported | tests/test_examples_coverage.py::test_every_example_produces_rust_that_actually_compiles[algorithms/bubble_sort5.zqel] |
expr/index |
supported | tests/test_examples_coverage.py::test_every_example_produces_rust_that_actually_compiles[algorithms/insertion_sort.zqel] |
expr/len |
supported | tests/test_examples_coverage.py::test_every_example_produces_rust_that_actually_compiles[mtp/anaview.zqel] |
expr/logic |
supported | tests/test_examples_coverage.py::test_every_example_produces_rust_that_actually_compiles[algorithms/fibonacci.zqel] |
extern/by |
supported | tests/test_examples_coverage.py::test_every_example_produces_rust_that_actually_compiles[extern/sat_add_u8.zqel] |
extern/function |
supported | tests/test_examples_coverage.py::test_every_example_produces_rust_that_actually_compiles[extern/sat_add_u8.zqel] |
extern/real_contract |
supported | observed by an executed frontend test; this row does not claim backend support — see feature_by_backend |
impl/realization_by |
supported | tests/test_examples_coverage.py::test_every_example_produces_rust_that_actually_compiles[realization/TripLatchBy.zqel] |
impl/register_rules |
supported | tests/test_examples_coverage.py::test_every_example_produces_rust_that_actually_compiles[algorithms/fibonacci.zqel] |
polarity/inverted |
supported | tests/test_examples_coverage.py::test_every_example_produces_rust_that_actually_compiles[rias/ConveyorInterlock.zqel] |
pou/function |
supported | tests/test_examples_coverage.py::test_every_example_produces_rust_that_actually_compiles[algorithms/insertion_sort.zqel] |
pou/function_block |
supported | tests/test_array_of_fb_reaches_the_targets.py::test_the_generated_st_runs_under_matiec_and_matches_the_reference |
pou/program |
supported | tests/test_examples_coverage.py::test_every_example_produces_rust_that_actually_compiles[algorithms/lm_step/LMFit.zqel] |
pou/ssfc |
supported | tests/test_examples_coverage.py::test_every_example_produces_rust_that_actually_compiles[pasteurizer/BatchPasteurizer.zqel] |
spec/predicates |
supported | tests/test_examples_coverage.py::test_every_example_produces_rust_that_actually_compiles[algorithms/insertion_sort.zqel] |
ssfc/actions |
supported | tests/test_examples_coverage.py::test_every_example_produces_rust_that_actually_compiles[analog/differentiator.zqel] |
ssfc/parallel |
supported | tests/test_t48_backend_lower.py::test_bl01_compile_pipeline |
ssfc/states |
supported | tests/test_examples_coverage.py::test_every_example_produces_rust_that_actually_compiles[pasteurizer/BatchPasteurizer.zqel] |
ssfc/transitions |
supported | tests/test_examples_coverage.py::test_every_example_produces_rust_that_actually_compiles[pasteurizer/BatchPasteurizer.zqel] |
type/array |
supported | tests/test_examples_coverage.py::test_every_example_produces_rust_that_actually_compiles[algorithms/insertion_sort.zqel] |
type/bitstring |
supported | tests/test_examples_coverage.py::test_every_example_produces_rust_that_actually_compiles[bits/quality_byte.zqel] |
type/boolean |
supported | tests/test_array_of_fb_reaches_the_targets.py::test_the_generated_st_runs_under_matiec_and_matches_the_reference |
type/integer |
supported | tests/test_examples_coverage.py::test_every_example_produces_rust_that_actually_compiles[algorithms/bubble_sort5.zqel] |
type/real |
supported | tests/test_examples_coverage.py::test_every_example_produces_rust_that_actually_compiles[algorithms/lm_step/LMFit.zqel] |
type/string |
supported | tests/test_examples_coverage.py::test_every_example_produces_rust_that_actually_compiles[mtp/anaview.zqel] |
type/time |
supported | tests/test_examples_coverage.py::test_every_example_produces_rust_that_actually_compiles[iec/tof.zqel] |
type/unsigned |
supported | tests/test_examples_coverage.py::test_every_example_produces_rust_that_actually_compiles[extern/sat_add_u8.zqel] |
Toolchains¶
| toolchain | state | declared evidence nodes | why |
|---|---|---|---|
cbmc |
supported | 21 | |
creusot (on darwin) |
not-applicable | 1 | the pinned upstream package cannot be built on darwin, so the devShell omits it (#139); the canonical node declares platforms=('linux',). |
creusot (on linux) |
supported | 1 | |
cvc5 (on darwin) |
not-applicable | 0 | reachable only through creusot, which is not available on darwin (#139). |
cvc5 (on linux) |
unmeasured | 0 | reachable only through creusot; the creusot-proof gate runs both proofs green (#152) with cvc5 among the four provers, but no log has yet shown a goal discharged BY cvc5 — a solver that starts is not proof evidence. |
gappa |
supported | 20 | |
kani |
supported | 33 | |
matiec |
supported | 8 | |
rust-runtime |
supported | 1 | |
rustc |
supported | 100 | |
z3 |
supported | 121 |
Feature × backend¶
The flat list above says a feature was OBSERVED. This says whether
a backend supports it. mixed means the backends disagree and the
row below it is where the disagreement lives — it is derived, never
stored.
| feature | st | rust | rollup |
|---|---|---|---|
assurance/policy |
supported | supported | supported |
compose/continuous |
supported | supported | supported |
compose/wiring |
supported | supported | supported |
contract/clauses |
supported | supported | supported |
contract/rule |
supported | supported | supported |
contract/section |
supported | supported | supported |
contract/temporal |
supported | supported | supported |
conv/explicit |
supported | supported | supported |
decl/const |
supported | supported | supported |
decl/parameter |
supported | supported | supported |
decl/var_sections |
supported | supported | supported |
expr/aggregate |
supported | supported | supported |
expr/arithmetic |
supported | supported | supported |
expr/clamp |
supported | supported | supported |
expr/comparison |
supported | supported | supported |
expr/index |
supported | supported | supported |
expr/len |
supported | supported | supported |
expr/logic |
supported | supported | supported |
extern/by |
unsupported/refused | supported | mixed |
extern/function |
supported | supported | supported |
extern/real_contract |
not-applicable | not-applicable | not-applicable |
impl/realization_by |
supported | supported | supported |
impl/register_rules |
supported | supported | supported |
polarity/inverted |
supported | supported | supported |
pou/function |
supported | supported | supported |
pou/function_block |
supported | supported | supported |
pou/program |
supported | supported | supported |
pou/ssfc |
supported | supported | supported |
spec/predicates |
supported | supported | supported |
ssfc/actions |
supported | supported | supported |
ssfc/parallel |
supported | supported | supported |
ssfc/states |
supported | supported | supported |
ssfc/transitions |
supported | supported | supported |
type/array |
supported | supported | supported |
type/bitstring |
supported | supported | supported |
type/boolean |
supported | supported | supported |
type/integer |
supported | supported | supported |
type/real |
supported | supported | supported |
type/string |
supported | supported | supported |
type/time |
supported | supported | supported |
type/unsigned |
supported | supported | supported |
Feature × toolchain¶
"matiec is supported" and "matiec has been shown to accept a MATHREAL programme" are different claims. The per-tool total above is the coarser one; this is the finer, and it is the one worth citing.
Two rows here are STAGES rather than tools. rustc says the emitted
code compiles; rust-runtime says the compiled programme was run and
compared against the reference. A gap in the second is not a fault of
the first.
| feature | toolchain | state |
|---|---|---|
assurance/policy |
gappa |
supported |
compose/instance |
matiec |
supported |
impl/register_rules |
matiec |
supported |
pou/function_block |
matiec |
supported |
pou/ssfc |
z3 |
supported |
ssfc/actions |
z3 |
supported |
ssfc/parallel |
z3 |
supported |
ssfc/states |
z3 |
supported |
ssfc/transitions |
z3 |
supported |
type/boolean |
matiec |
supported |
type/integer |
matiec |
supported |
type/real |
matiec |
supported |
type/real |
rust-runtime |
supported |
Feature × profile¶
A bound is compared against a proved error envelope, and an envelope exists only where a representation does. The same feature is therefore accepted under one profile and refused under another, with different codes — two facts, not one verdict.
| feature | profile | state |
|---|---|---|
assurance/policy |
default |
unsupported/refused (assurance-policy-unprovable) |
assurance/policy |
float64_repr |
supported |
assurance/policy |
pilot |
unsupported/refused (overflow) |
type/real |
float64_repr |
supported |
Refusals¶
| cell | code | evidence |
|---|---|---|
extern/by@st |
st-extern-no-binding |
tests/test_st_refusal_is_typed.py::test_the_st_backend_refuses_a_rust_only_extern_with_a_code |