[float_bounded_axiomatic] fix the floor error typo

[Robertboy18]

hey! this fixes the floor typo from #24.

basically:

• uses the actual absolute input error
• uses absolute error in the result too
• switches the bound to e1 + 1, which matches the already-proved version in float_unbounded

checked it with PVS 8.1:

• the old FALSE repro does not go through anymore
• ./prove-all -do=float/float_bounded_axiomatic passes all 344/344 proofs

pretty small fix, just making the axiom say what it was meant to say.

Closes #24

[Copilot]

Pull request overview

This PR fixes an unsoundness in the float_bounded_axiomatic floor absolute-error/ULP axiom (aerr_ulp_floor_correct) that previously allowed deriving contradictions (Issue #24). It updates the axiom to use absolute error on both the premise and the result, and adjusts the bound to a conservative e1 + 1, aligning with the already-proved unbounded development.

Changes:

• Redefines aerr_ulp_floor(r1, e1) to the conservative bound e1 + 1.
• Updates aerr_ulp_floor_correct to use abs(proj(f1) - r1) in the premise and abs(proj(floor_ieee754(f1)) - floor(r1)) in the conclusion.
• Adds/updates the proveit summary output for float/float_bounded_axiomatic reflecting all proofs succeeding.

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated no comments.

File	Description
float/float_bounded_axiomatic/aerr_ulp_floor.pvs	Fixes the floor axiom’s premise/conclusion to use absolute error and updates the bound to e1 + 1.
summaries/float-float_bounded_axiomatic.summary	Records the latest proof run summary showing the float_bounded_axiomatic library proofs succeeding.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.