1712665dfe
Some checks failed
WAI breaking changes and the conformance runner / WAI breaking · does this change touch WAI (push) Successful in 8s
WAI breaking changes and the conformance runner / WAI breaking · wire, record and API against main · linux (push) Failing after 45s
repository checks / lockfiles, advisories, tests in CI, workflow hygiene, spec and section references, public text (push) Successful in 11m51s
WAI breaking changes and the conformance runner / WAI breaking and conform · their tests, and the independent verifiers through wai conform · linux (push) Successful in 7m31s
settle_decide now refuses (returns -3, before any record or the chain changes) a meter whose grade or weakest input's grade is not one of oer-receipts §2's four, or which grades a figure measured by a method other than hardware_meter, the corpus's term for a meter that reads an instrument. The kernel already writes the grade its meter states (1f5bfbd1e); a model's figure handed to it as a reading can no longer be signed as one. The host harness checks, after writing its file, three refusals (a model graded measured, a grade outside the four, a weakest grade outside them) and that a measured figure from hardware_meter is taken, and exits 4 otherwise. So the existing CI step that rebuilds firmware_vectors.json checks the rule on every unix leg; its comment says so. The pinned corpus is unchanged. Re-landed from PR #459 (8570389f9,a184a44cf): main took the grade from the meter and regenerated the one pinned corpus, so the branch's issued/modelled modes and its second corpus are not carried; its refusal is. Tested on the M3 Ultra (Apple clang 21) and the Linux build host (gcc 15.2), with the CI step's flags: no warning in settle.c or host_main.c; the output equals ../firmware_vectors.json under cmp; oer2_verify.py passes it on the M3 (the Linux host has no Ed25519 library for that check). Falsified on both: the method rule removed, and the call removed, each make the harness exit 4; so does refusing every measured figure. Co-Authored-By: Claude Opus 5.5 <[email protected]>
38 lines
2.8 KiB
Markdown
38 lines
2.8 KiB
Markdown
# settle: the settlement kernel in portable C
|
|
|
|
The keystone loop as code that runs on a microcontroller and on a host: canonicalize a question, hash its key,
|
|
look it up, verify, decide with compiled rules, record with a validity window, and emit an OER/2 receipt
|
|
(draft 0.1 as profiled by [`extensions/oer-receipts.md`](../../extensions/oer-receipts.md)): canonical bytes in the envelope's fixed order, SHA-256 receipt id and chain hash, Ed25519 signature.
|
|
|
|
Files: `settle.c/.h` (the kernel), `sha256.c/.h`, `tweetnacl.c/.h` (public domain Ed25519), `host_main.c`
|
|
(host harness with a modelled meter), `zephyr/` (application skeleton for a Zephyr board; untested build).
|
|
|
|
Build and cross-verify against the Python reference verifier from the OER/2 vector set:
|
|
|
|
make
|
|
./settle_host firmware_vectors.json 400
|
|
python3 ../oer2_verify.py firmware_vectors.json # PASS v10 firmware chain from the C kernel
|
|
cmp firmware_vectors.json ../firmware_vectors.json # the pinned corpus: no drift
|
|
|
|
The harness writes 400 receipts, the records they cite and a ledger identity; the verifier checks canonical
|
|
bytes, ids, chain, sums, floors, records and signatures. Two implementations, one receipt — three with `wai_oer_vectors` in `wai-rs`, which CI runs over this output.
|
|
|
|
What the kernel does not do yet: escalate new questions upstream (a callback hook is the next addition),
|
|
read a rail meter (the host models one; the Zephyr skeleton counts cycles), and hold the signing seed in a
|
|
secure element. Energy constants inside the kernel (cycle energy, bits committed) are the model's projected
|
|
values until the bench node measures them.
|
|
|
|
So no receipt here is a reading. The kernel writes the grade and the device the meter states
|
|
(`settle_meter_t.how`, `.device`) and no longer fixes them to `measured` from `hardware`: the host harness
|
|
states `projected`, from a `simulation`, by the method `model_estimated`, and the Zephyr skeleton
|
|
`projected` on `hardware` by the same method (oer-receipts §2: a figure computed from constants is an
|
|
`Estimator` figure, graded `projected`). The ledger's `meter_joules` is the sum of those projected figures,
|
|
and the harness says so when it prints it.
|
|
|
|
The kernel also refuses to sign a grade its meter cannot support: `settle_decide` returns -3, before any
|
|
record or the chain changes, for a meter whose grade or weakest input's grade is not one of oer-receipts
|
|
§2's four, or which grades a figure `measured` by a method other than `hardware_meter` (the corpus's term
|
|
for a meter that reads an instrument). So a model's figure cannot be signed as a reading whatever its meter
|
|
states. After writing its file the harness checks three such refusals, and that a `measured` figure from
|
|
`hardware_meter` is taken; it exits 4 if any check fails, so the CI step that rebuilds the corpus checks the
|
|
rule on every run.
|