Module fp_receipt 

The card’s measurement of its floating-point DSP block as a receipt (benchmarks/silicon/d5005/fp_hard_receipts.json): what the oracle persona (super::fp_oracle) measured on the card, tied to the build that compiled it and the image the card ran, with what each mode’s block is for the engine (super::fp_hard). The block is the vendor’s and encrypted, so a receipt is a measurement recorded as one; the proofs hold everything around it.

A receipt reads (receipt) only when:

• the build is a row of the build ledger that passed, naming the engine it compiled (hw/rtl/logos_engine.v, by SHA-256);
• the card’s run configured the image (gbs.sha256, the run’s own hash of what it loaded), partial reconfiguration reported no error (PR_ERR all zero), the user clock was set, and the run finished no earlier than it started;
• the measurement finished.

Each mode is its depths, the one class that agreed with the block on every step (or how many did, and the steps no class explains), the classes that differed on the fewest steps, and the engine’s unit at its latency on that block: the wrapper’s build (plan) or why there is none. The multiply-add is its depth and its rounding.

record refuses besides a receipt whose discriminator ledger does not regenerate the engine the build compiled (the persona’s oracle is that ledger’s classes and vectors), and a measurement the ledger already holds. Its inputs are kept beside the ledger (KEPT in kept_dir, each as kept keeps it), so every receipt reads again from them.

Structs

CardRun

What the card’s run left beside its measurement, each file as the run wrote it.

Inputs

Everything a receipt is read from.

Ledger

The receipts ledger.

Mode

One mode of the block as the card measured it.

Near

One class and the steps on which it differed from the block over every run.

Receipt

A receipt: the run’s identity, the measurement’s size, and each mode.

Steps

The steps of each run.

Enums

ReceiptError

Why a receipt is not read or not recorded.

Unit

The engine’s unit on one mode’s block.

Constants

KEPT

The inputs a receipt keeps beside the ledger, each under the name the card’s run wrote it (the discriminator ledger as discriminators.json), in kept_dir.

LEDGER_WHAT

What the receipts ledger says of itself when it starts.

NEAREST

How many of the classes nearest the block a mode keeps.

Functions

engine_held

Whether engine is the engine the build compiled and was made of discriminators: its SHA-256 the build row’s hw/rtl/logos_engine.v, and every module of it the oracle writes itself (Oracle::own_verilog) the text the oracle of discriminators writes now, byte for byte. A receipt is recorded under it; kept, the engine is held by its SHA-256 thereafter, so the oracle’s code may move on. The library the engine embeds (the engine’s crossing and ports, the store’s memory) is held by the build’s SHA-256 alone, so the library may move on between a build and its receipt; an own module that does not regenerate is refused by name.

kept

A card run’s file name as the ledger keeps it: as the run wrote it, but for a sha256sum line (gbs.sha256), which names its image by its file name alone, so no kept input names one machine’s directories.

kept_dir

Where a receipt’s inputs are kept, under fp_receipts/ beside the ledger: the build and the measurement’s first twelve hex digits, one directory a measurement.

receipt

The receipt inputs make, as recorded at recorded.

receipt_of

The receipt that records measurement, by its SHA-256: the card run a hard-float build takes its blocks from, read against the discriminator ledger kept beside it (fp_receipts/<kept_dir>/discriminators.json).

record

receipt, refused unless engine is held (engine_held) and ledger (none: a new ledger) holds no receipt of the same measurement; with the ledger it is appended to, as written.