Cost estimates for configured binary execution #

These estimates combine arithmetic work with the cost of adapting the selected storage carrier to the proof model. They influence static backend selection only; no semantic theorem depends on their calibration.

Representation-aware cost decoration #

source

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.modelMarshallingCost {format : FloatFormat} (plan : StoragePlan format) (operation : ExecFloat.Backend.Operation) :

ℕ

Estimated cost of adapting one packed public value to and from the proof model.

The count scales with operation arity because every operand is decoded and one result is packed. The values are calibration priors, not semantic facts. A direct carrier kernel sets this cost to zero; benchmark calibration may update the constants without changing any refinement theorem.

Byte and machine-word carriers are charged one unit per adapted value, on the same approximate 100 ns scale as the tiny-format arithmetic estimates. Machine-word carriers decode with BitVec.ofNatLT from the stored range proof and pack with one narrowing conversion.

The limb carrier converts each value through LimbArray.toNat and LimbArray.ofNat, one arbitrary-precision operation per limb, so its adapter cost grows with the limb count. Accepted wide-limb paths avoid this conversion; declined calls use the model adapter for the exact fallback.

Instances For

source