fp8 E5M2 addition under roundNearestTiesToEven is monotone in its first argument

Identifier: F:fp8-add-monotone-rne
Proof route: smt-clausal
External status: proved
Axiom footprint: ieee754-2019-arithmetic-semantics-for-the-OCP-fp8-E5M2-layout-as-encoded-by-axeyum-fp-fpa2bv-lowering-and-as-implemented-by-rustc_apfloat, axeyum-fp.add-is-a-differentially-VALIDATED-not-proven-bit-blaster, rounding-mode-roundNearestTiesToEven-only-for-this-fact-though-all-five-were-swept-on-the-enumeration-route, smtlib2-fp.leq-ordering-nan-unordered-plus-zero-equals-minus-zero, tseitin-cnf-encoding-preserves-satisfiability, drat-refutation-semantics-as-implemented-by-axeyum-cnf-check-drat, the-enumeration-covers-the-domain-exactly-2^24-triples-is-every-triple-of-an-8-bit-format, format-fp8-E5M2-only-this-fact-is-not-format-generic-and-says-nothing-about-E4M3

Recorded description

Let F be the IEEE-754-conformant 8-bit format OCP fp8 E5M2, SMT-LIB `(_ FloatingPoint 5 3)`, and let RNE denote roundNearestTiesToEven. For all values a, b, c of F: if fp.leq(a, b) holds and neither fp.add(RNE, a, c) nor fp.add(RNE, b, c) is NaN, then fp.leq(fp.add(RNE, a, c), fp.add(RNE, b, c)). Note that fp.leq is false whenever either operand is NaN, so the antecedent already excludes NaN inputs; the two explicit guards exclude only NaN RESULTS, which arise from (+oo) + (-oo). This is the property that licenses interval and bound propagation through a rounded-addition kernel.

Formal statement

(assert (=> (and (fp.leq a b) (not (fp.isNaN (fp.add RNE a c))) (not (fp.isNaN (fp.add RNE b c)))) (fp.leq (fp.add RNE a c) (fp.add RNE b c))))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

0 direct dependencies 0 direct dependents

Evidence

fp8-monotone-exhaustive-apfloat

Kind: exhaustive-enumeration
Status: checked

Supports: Every fp8 E5M2 triple (a, b, c) satisfying the antecedent was enumerated -- 7843500 of the 16777216 triples -- and the consequent held at all of them, under RNE and under each of the other four SMT-LIB rounding modes.

Checker command

cargo run --release -q -p axeyum-fp --example kernel_equivalence -- monotone --all-modes

Evidence notes

Ran 2026-08-14. examined=7843500 failures=0 at RNE, and identically at RNA, RTP, RTN and RTZ. The enumeration is over all 2^24 = 16777216 triples of the 8-bit format; 7843500 of them pass the guard (fp.leq(a,b) holds and neither result is NaN) and are the ones the claim speaks about. `rustc_apfloat` 0.2.3 (LLVM APFloat) shares no code with axeyum's bit-blaster, CNF encoder or SAT core. Ordering is APFloat's PartialOrd, which is SMT-LIB fp.leq: NaN unordered, +0 and -0 equal. The binary exits non-zero on any violation.

fp8-monotone-unsat-drat

Kind: unsat-certificate
Status: checked

Supports: The negation of formal.statement is unsatisfiable over fp8 E5M2, decided symbolically -- without enumerating the 2^24 triples.

Evidence notes

Ran 2026-08-14: `; evidence kind=unsat-drat certified=1 recheck=ok arena=ok ms=928629`, verdict `unsat`, 25m46.4s wall in a release build on a machine at load 16-25. `recheck=ok` is axeyum's own `check_drat` (RUP+RAT, ADR-0011) re-checking the emitted refutation; `arena=ok` is `Evidence::check` against a fresh parse. NO EXTERNAL ORACLE AGREES OR DISAGREES, because neither can read the query: z3 4.13.3 returns `unknown` with `(:reason-unknown "addition/subtract with ebits > sbits not supported")` -- E5M2 is (_ FloatingPoint 5 3) and 5 > 3 -- and bitwuzla 0.9.1 rejects the format as experimental, its own suggested `--fpexp` escape being a BUILD option that the binary refuses as an invalid runtime flag. The independent confirmation is the exhaustive row above, not a second solver. THIS ROW CARRIES NO `checker_command` ON PURPOSE. At 25m46s it would blow any per-checker budget scripts/check-fact-evidence-replay.sh runs with. The fact stays covered by the exhaustive row, which re-runs in about three seconds. To re-derive this row by hand: cargo run --release -q -p axeyum-bench --example smtcomp_cli -- --evidence artifacts/facts/smt2/neg-fp8-add-monotone-rne.smt2

Provenance

{
  "date": "2026-08-14",
  "established_by": "fp-kernels lane; an exhaustive LLVM-APFloat enumeration of all 2^24 fp8 E5M2 triples, and independently a symbolic CNF/DRAT refutation from axeyum",
  "source": "authored here. The proposition is the one a bound-propagation or interval-arithmetic pass over a quantized kernel silently assumes.",
  "prior_art": [
    {
      "who": "IEEE 754-2019, clause 4.3 (rounding-direction attributes)",
      "what": "That each rounding-direction attribute defines a monotone (non-decreasing) map from the extended reals to the format, so a correctly-rounded operation inherits the monotonicity of the exact operation it rounds.",
      "where": "IEEE Standard for Floating-Point Arithmetic",
      "year": 2019,
      "attribution": "standard textbook attribution; this lane did not consult the primary source, and records the citation as the received one. Nothing in the evidence above depends on it -- the property is enumerated here, not derived."
    }
  ]
}