Add bounded memory-safety harnesses for core::num::flt2dec (challenge #28) - #601

Open

MavenRain wants to merge 84 commits into

model-checking:mainfrom

MavenRain:verify-flt2dec-challenge-28

Commits on Jun 16, 2026

Verify core::num::flt2dec memory safety (challenge #28)
MavenRain
committed
e4e3297

Commits on Jun 17, 2026

Challenge #28: fix CI (autoharness debug-asserts + partition-2 OOM)
MavenRain
committed
e104d40

Commits on Jun 22, 2026

Challenge #28: drop debug-assertions-off harnesses, revert
MavenRain
committed
9d5b396

Commits on Jun 24, 2026

Challenge #28: make dragon stub harnesses robust to debug-assertions ON
MavenRain
committed
c02f4fd

Commits on Jul 8, 2026

Merge branch 'main' into verify-flt2dec-challenge-28
MavenRain
authored
6cbcdbc

Commits on Aug 17, 2026

Commits on Sep 12, 2026

Commits on Sep 13, 2026

Add a bounded rounding contract for flt2dec strategy proofs
MavenRain
committed
eb897d4
Import core's Kani module in the rounding proofs
MavenRain
committed
28c3b7e
Use Kissat for the direct flt2dec generator proofs
MavenRain
committed
41e1d36
Serialize CI verification for partition 2
MavenRain
committed
102b1a2
Give autoharness proofs a serial execution budget
MavenRain
committed
6c28835
Preserve thread labels in serial CI logs
MavenRain
committed
1ab9926
Support serial Kani verification in PR CI
MavenRain
committed
c68c227
Partition floating-point generator proofs by exponent
MavenRain
committed
bc720cc
Report failed and timed-out Kani proofs promptly
MavenRain
committed
e9c5e45
ci: trust the existing CBMC tap on macOS runners
MavenRain
committed
b396b58
Add a storage contract for bounded Dragon division
MavenRain
committed
d66a5d7
Avoid panics in the division contract's old expression
MavenRain
committed
d989659
Check flt2dec proof families independently in CI
MavenRain
committed
a1b733a
Reduce symbolic iteration in flt2dec contract predicates
MavenRain
committed
cc01efe
Probe flt2dec verification with a fixed binary exponent
MavenRain
committed
5ff6a97
Decompose the flt2dec bigint division contract by limb
MavenRain
committed
8ece960
Run focused flt2dec proofs with CVC5 and preserve contract diagnostics
MavenRain
committed
3ebd8e7
Avoid recursive substitution in the bigint division contract proof
MavenRain
committed
23192a4
Retain harness solvers after the CVC5 translation failure
MavenRain
committed
40e3b33
Scope Dragon unwind limits to the float input family
MavenRain
committed
058cfa7
Give f32 and f64 generator proofs independent CI jobs
MavenRain
committed
39e2996
Verify the bigint limb loop independently of power-of-ten division
MavenRain
committed
e7bd2d5
Match the bigint division adapter return type
MavenRain
committed
2c1cad5
Limit bigint division contracts to their writable limbs
MavenRain
committed
dc8fc03
Keep bounded generator lengths narrow during symbolic execution
MavenRain
committed
c5d48b4
Prove equivalence of constant-index bigint comparison models
MavenRain
committed
b3072db
Use Grisu exact mode's error counter to bound loop unwinding
MavenRain
committed
26975f9
Use Kani's default symbolic object capacity
MavenRain
committed
67718cc
Keep bigint comparison models linear in their limb count
MavenRain
committed
4e233ff
Select symbolic object capacity for each CI proof kind
MavenRain
committed
d701b3d
Match bigint comparison models to the real active prefixes
MavenRain
committed
94f5b7c
Compose Grisu exact proofs with a final-rounding contract
MavenRain
committed
f08eb0d
Keep unused bigint size bits concrete in the equivalence proof
MavenRain
committed
98b3aef
Keep the Grisu rounding contract's write set empty
MavenRain
committed
5c22322
Check bigint model equivalence without a function write frame
MavenRain
committed
9b887fd
Compose Grisu shortest with an independent final-rounding proof
MavenRain
committed
04a312c
Reduce rounding contract argument tracking
MavenRain
committed
5a14fbb
Compare CBMC encodings in focused flt2dec probes
MavenRain
committed
1f6ea34
Use an additive shortest-rounding stopping predicate
MavenRain
committed
98e050b
Probe a smaller object table for Grisu exact
MavenRain
committed
946da21
Reduce exact-rounding contract call state
MavenRain
committed
e5cfcf6
Restore sufficient object capacity for the exact Grisu probe
MavenRain
committed
81de91a
Add exact bit-scan models with independent equivalence proof
MavenRain
committed
431e679
Share Grisu exact rounding across generator exits
MavenRain
committed
49acde4

Commits on Sep 14, 2026

Share Grisu shortest rounding across generator exits
MavenRain
committed
0bbe551
Add an exact estimator model with independent equivalence proof
MavenRain
committed
5a571b3
Use scalar inputs for the shortest-rounding contract
MavenRain
committed
df8bbbb
Split estimator equivalence and bound CI proof batches
MavenRain
committed
c108d77
Give generator proofs more time within bounded CI batches
MavenRain
committed
d8c4abe
Expose checked constant scaling in Dragon diagnostic proofs
MavenRain
committed
c9e6a24
Expose checked exponent bits in Dragon proofs
MavenRain
committed
ee24d41
Assign flt2dec proofs once per operating system
MavenRain
committed
c4a9310
Merge main to restore PR CI
MavenRain
committed
6aaa21e
Expose checked bigint counts in Dragon diagnostics
MavenRain
committed
5a269ad
Check constant cached-power selection in Grisu probes
MavenRain
committed
559e45f
Check bigint arithmetic models in Dragon diagnostics
MavenRain
committed
1dd861f
Allow composed Kani stubs to expand in core
MavenRain
committed
0e3ea78
Give Grisu shortest proofs more time in smaller CI batches
MavenRain
committed
6915963
Split multiplication equivalence by exhaustive storage sizes
MavenRain
committed
4fb7f47
Expose literal decimal divisors in Grisu shortest proofs
MavenRain
committed
7288012
Use Z3 for exhaustive multiplication equivalence cases
MavenRain
committed
b9e2db1
Use Z3 for full-range Grisu shortest proofs
MavenRain
committed
5653b8a
Use SAT arithmetic refinement for remaining flt2dec proofs
MavenRain
committed
971b426
Apply arithmetic refinement to both Grisu float kinds
MavenRain
committed
87c3397
Compose an exact limb multiplication contract in Dragon proofs
MavenRain
committed
50d1b01
Test datatype-free SMT encoding for Grisu shortest probes
MavenRain
committed
1e37fdd
Use Z3 for composed multiplication proofs
MavenRain
committed
2a9e0b9
Separate Grisu shortest scaling from digit-loop proofs
MavenRain
committed
48116d9
Share scalar multiplication expressions in equivalence proofs
MavenRain
committed
4bd2580
Check packed multiplication results before individual limbs
MavenRain
committed
f926a7a
Strengthen Grisu interval facts and compose proved scalar models
MavenRain
committed
2b15b71
Partition scaling proofs across the full normalized exponent range
MavenRain
committed
7cc96c8
Reuse checked limb counts in symbolic storage predicates
MavenRain
committed
f60b933
Expose checked cached-power ranges in scaling proofs
MavenRain
committed
368085f
Retry failed dependency downloads in GitHub CI
MavenRain
committed
64147ad