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]>
50 lines
4.1 KiB
C
50 lines
4.1 KiB
C
/* SPDX-License-Identifier: Apache-2.0 */
|
|
/* Host harness: replays a day of demand through the kernel with a modelled meter and writes an OER/2 vector file.
|
|
The meter is a model of constants (a cycle count, standby and shared draws, a link energy), none measured on the
|
|
node, so every figure is graded projected (oer-receipts §2: an Estimator figure), from a simulation, by a modelled
|
|
method: the receipts never present the model as a reading. */
|
|
#include "settle.h"
|
|
#include <stdio.h>
|
|
#include <stdlib.h>
|
|
#include <string.h>
|
|
static uint32_t rng_s = 42; static double urand(void){ rng_s = rng_s * 1664525u + 1013904223u; return (rng_s >> 8) / 16777216.0; }
|
|
int main(int argc, char **argv){
|
|
const char *path = argc > 1 ? argv[1] : "firmware_vectors.json"; int n_events = argc > 2 ? atoi(argv[2]) : 400;
|
|
static settle_ctx_t ctx; uint8_t seed[32]; int i; for (i = 0; i < 32; i++) seed[i] = (uint8_t)(i * 7 + 3);
|
|
settle_init(&ctx, seed, 300.0, 86400.0);
|
|
FILE *f = fopen(path, "w"); if (!f) return 1;
|
|
char pk[65]; settle_pk_hex(&ctx, pk);
|
|
fprintf(f, "{\"oer\":\"2.0\",\"draft\":\"0.1\",\"source\":\"settle kernel host harness, %d events\",\"keys\":{\"ed25519:bench-node-01\":\"%s\"},\"vectors\":[{\"name\":\"v10 firmware chain from the C kernel\",\"receipts\":[", n_events, pk);
|
|
static char buf[4096]; double now = 0, last = 0, meter = 0; const double standby_w = 1.8e-3, shared_w = 0.06;
|
|
for (i = 0; i < n_events; i++) {
|
|
now += 20 + 80 * urand(); char cls = urand() < 0.34 ? 'A' : 'B';
|
|
double z = urand(); uint32_t id = (uint32_t)(cls == 'A' ? 1 + 2999 * z * z * z : 1 + 399 * z * z * z);
|
|
settle_meter_t m; m.compute_j = 120000.0 * ctx.cycle_j; m.movement_j = cls == 'A' ? 2.3e-6 : 0; m.idle_alloc_j = standby_w * (now - last); m.shared_alloc_j = shared_w * (now - last); m.upstream_j = 0;
|
|
m.latency_s = cls == 'A' ? 0.019 : 0.0017; m.method = "model_estimated"; m.how = "projected"; m.device = "simulation"; m.weakest_how = "projected"; m.weakest_input = "wire_w";
|
|
settle_result_t res; if (settle_decide(&ctx, cls, id, now, &m, buf, sizeof buf, &res)) { fprintf(stderr, "decide failed\n"); return 2; }
|
|
meter += res.joules_total; last = now;
|
|
fprintf(f, "%s%s", i ? "," : "", buf);
|
|
}
|
|
static char recbuf[1 << 20]; fprintf(f, "],\"records\":"); if (settle_records_json(&ctx, recbuf, sizeof recbuf)) { fprintf(stderr, "records overflow\n"); return 3; } fputs(recbuf, f);
|
|
fprintf(f, ",\"ledger\":{\"meter_joules\":\"%.12e\",\"unallocated_joules\":\"0.000000e+00\",\"carried_forward_joules\":\"0.000000e+00\"},\"expected\":[]}]}\n", meter);
|
|
fclose(f); fprintf(stderr, "wrote %s: %d receipts, modelled meter %.6f J (projected, not a reading)\n", path, n_events, meter);
|
|
/* The kernel signs no grade its meter cannot support (oer-receipts §2), checked on every run, after the
|
|
file is written: this harness's model graded measured, a grade outside the four and a weakest grade
|
|
outside them are each refused (-3); the same figure graded measured by a meter that reads an
|
|
instrument is taken, so the rule is not a refusal of every measured figure. */
|
|
{
|
|
static const struct { const char *method, *how, *device, *weakest_how; int want; } cases[] = {
|
|
{ "model_estimated", "measured", "simulation", "projected", -3 },
|
|
{ "model_estimated", "estimated", "simulation", "projected", -3 },
|
|
{ "model_estimated", "projected", "simulation", "estimated", -3 },
|
|
{ "hardware_meter", "measured", "hardware", "projected", 0 },
|
|
};
|
|
for (i = 0; i < 4; i++) {
|
|
settle_meter_t m = { .compute_j = 1e-3, .latency_s = 0.001, .method = cases[i].method, .how = cases[i].how, .device = cases[i].device, .weakest_how = cases[i].weakest_how, .weakest_input = "wire_w" };
|
|
settle_result_t res; int rc = settle_decide(&ctx, 'A', 1, now + 1 + i, &m, buf, sizeof buf, &res);
|
|
if (rc != cases[i].want) { fprintf(stderr, "a meter by %s graded %s (weakest %s): settle_decide gave %d, not %d\n", cases[i].method, cases[i].how, cases[i].weakest_how, rc, cases[i].want); return 4; }
|
|
}
|
|
fprintf(stderr, "a grade the meter cannot support: refused in 3 of 3 cases; a measured figure from an instrument's meter taken\n");
|
|
}
|
|
return 0;
|
|
}
|