cvlr_fixed_fv

Formal verification of the fixed crate's FixedU64 arithmetic against the NativeFixedU64 reference model from cvlr-fixed, using the Certora CVLR Solana prover.

Layout

• src/certora/specs/arith/ — rules comparing FixedU64::<UN>::checked_* / strict ops against NativeFixedU64<N> for each N.
• src/certora/specs/cmp.rs, convert.rs — comparison and conversion rules.
• src/certora/confs/ — per-rule prover configurations.

Known limitations

N = 64 (fully fractional) is not verified

NativeFixedU64<64> cannot be instantiated because cvlr-fixed defines

const BASE: u64 = 2u64.pow(Self::FRAC);

(see cvlr-fixed/src/native_fixed.rs). When FRAC = 64, 2^64 overflows u64 and const evaluation fails — any monomorphization of NativeFixedU64::<64> that touches BASE (i.e. from_val, checked_mul, checked_div, and the conversion helpers) errors at compile time with E0080.

Consequence: the 64, U64, … row is omitted from the gen_rules_unsigned! invocation in both arith/checked.rs and arith/strict.rs. Rules are generated for N = 0..=63 only.

A proper fix requires patching cvlr-fixed upstream (e.g. widening BASE to u128, or special-casing N = 64).