Form contract

Every program flowRS exports — an app for this computer, an app for a Linux board, a microcontroller's whole firmware — carries a FORM.json beside its source. It lists the properties below, 16 of them, and for each one says what enforces it, whether it holds for this program (live), holds in part (partial) or does not hold yet (not yet), why, and the evidence: the tests, proofs and tools in flowRS's gate that enforce it, and what was checked on this program when it was exported. A property that is not a property of that kind of program (no heap, on a computer) says so. The project's README.md states the same contract in plain words.

No status is written by hand. Each is computed when the program is exported, from the program as generated (its unsafe, read as syntax; its #![no_std]; its failure path), its graph (the nodes against what the generator lowers, the units on each wire), its Cargo.lock against flowRS's own, and, for a firmware, the board's binding, its twin, and the program's own Kani proof: a firmware ships its harness in proof/ with its record, proof/proofs.json, and the no-panic property is live only when that record says Kani proved exactly this program (the SHA-256 of its mod flow), every cover reached. Where flowRS's build host has proved the same program, the record arrives proved; otherwise flowrsc prove runs it, within a memory and a time budget. A test holds every live or partial claim to a second reading of the same files and fails when a status claims more than the code enforces.

The format is published as a JSON Schema: /schemas/form-contract-1.json ($schema in every FORM.json).

The properties

The counts are this build's: each example on the editor's start screen exported as an app (16 exported), and the board generator's acceptance graph (every embedded widget but PWM) exported as a firmware for each board the generator covers, on both executors (10 exported). Each export's own contract is read back and counted.

Not counted, because the exporter refuses them, by name:

• ds-sales: the program needs polars, which the Linux project generator has no pinned version for
• ds-regression: the program needs polars, which the Linux project generator has no pinned version for
• ml-classify: the program needs flowrs_ml, polars, tract_onnx, which the Linux project generator has no pinned version for
• detect-blobs: the program needs image, imageproc, which the Linux project generator has no pinned version for

The software bill of materials

Every export that carries its Cargo.lock carries sbom.cdx.json beside it: CycloneDX 1.6 JSON made from that lock, so it lists every package the project can build, for any feature and target. Each crates.io crate is there with its package URL, its SHA-256 and the licence its own manifest declares, each flowRS crate in vendor/ with its licence, and the lock's dependency graph with them. FORM.json names it in its sbom member, with its SHA-256 and the lock's, and the exporter refuses to ship one its lock does not bear out. Of the exports counted above, 26 carry one, listing from 15 to 23 components.

What each board's twin models

A firmware's contract carries its board's fidelity contract, generated from the twin census: the rung of the twin ladder its twin stands on, what executes its CPU, and which of its part's peripherals a model answers. The register-configuration property names, for each peripheral the program uses, whether the twin models it.

Whatever its rung, no twin models:

• the electrical side of the pins: drive strength, rise times, analogue levels and loading
• anything outside the chip that the board's wiring row does not describe
• the air: a radio's registers and timing may be modelled, its transmissions are not