port-audit: Z3 checks of chaceon

chaceon ports WAVEWATCH III (WW3) from Fortran to Rust for the GPU. It checks the port by cmp on whole runs and by captured calls: the Rust and the Fortran give the same bits on the inputs that ran. That evidence says nothing about an input that did not run, and it cannot see a defect that both sides share. Chaceon.scala states facts about chaceon's code for every input and asks Z3 for a counterexample, in the style of the rest of z3-scala/: unsat means none exists. The code is z3-scala/src/main/scala/portaudit/ (Chaceon.scala, Coverage.scala); this folder holds its report.

The audited commit is fe531e1e64950c0f3ce7987ae4ed0325a56adfbe (2026-11-04). Every file:line below is a path in chaceon at that commit.

z3-scala/z3.sh chaceon     # 28 lines of OK, about 10 s; exit code 1 if one fails
z3-scala/z3.sh coverage    # how much of WW3 is translated and integrated (below)
just port-audit            # the same; `just check` runs it too (checks/port-audit.sh)

What Z3 checks

Five checks expect a counterexample. Each one shows a hypothesis that is needed or a gap between a comment and the code:

The last two are not defects of the port: the port is byte-identical to WW3 on every regtest, so the Fortran very likely has the same lines (W3SRCE in w3srcemd.F90; not opened here). They say that damax is a target for the step, not a bound on it.

What Z3 cannot prove here

• That the Rust equals the Fortran. No formal semantics of Fortran or of gfortran -O3 exists to state it against; chaceon's cmp and captures are the evidence (docs/LEAN_202610.md, "Lean and Fortran").
• The division rewrite on IEEE bits, end to end. The direct statement, f32(f64(a) / f64(b)) == a / b over Z3's floating-point theory, did not finish in 8 minutes, even with a, b in [1, 2), and was stopped: Z3 bit-blasts a 53-bit divider. The check goes through the significands (no_tie, margin) and the reals (same_side), as chaceon's Lean proof does. That needs the scaling step: a power of two is exact in the normal range, so only t = 24 and t = 25 remain (Chaceon.scala, group D).
• The device. That OpFConvert rounds to nearest, that a device meets 2.5 ULP in OpFDiv, and that it honours NoContraction (spirv_exact/src/main.rs:2-7) are facts about a driver, not about code.
• Overflow, zero, infinity and NaN operands of the division (main.rs:7-8). They are outside the premises, as in Lean.
• The source terms themselves (sin4.rs, sds4.rs, snl1.rs and the others). Their values come from logf, tanhf, expf and powers in ww3-libm (rust/crates/ww3-libm/src/lib.rs). Z3 has no theory of these functions. The limiter is checked for any source values instead.
• The limiter in f32. limiter_bounds_increment, split_* and step_* hold over the reals. srce.rs:593-607 computes in f32, with rounding in each sum and product; the checks do not cover that rounding.
• The 1e-10 clamps (srce.rs:599-600). The limiter is checked without them; with vs near zero or 1 + afac * vd <= 0 the clamp sets the step, and no bound on the increment follows.
• The whole W3SRCE loop (srce.rs:546-684). Z3 has no induction. step_progress shows that each pass moves forward by min(dtmin, rem), so the loop ends when dtmin > 0; the loop itself and the 0.9999 * dtg exit (srce.rs:681) are not modelled.
• pow5 as GCC's power tree (util.rs:63-68). The tree is the right one only if it is the one gfortran -O3 emits; that is a fact about the compiler.
• x as i32 outside (-2^31, 2^31): Rust saturates, gfortran does not define NINT there. The nint and floor checks assume the range.

Coverage: translated and integrated

Coverage.scala measures how much of WW3 chaceon has translated, and how much of that its switch files compile. The unit is a Fortran code line of model/src/*.F90 at chaceon's WW3 pin: not blank, not a ! comment, not a preprocessor line, as in chaceon's scripts/port_summary.py (the totals agree: 120,705).

• Translated: a line inside a routine that chaceon's rust/ports.tsv lists, so Rust exists for it. Each row's status is its evidence, weakest first: translated, routine (every captured call bit-identical), host and spirv (whole output files byte-identical).
• Integrated: a translated line that the port's target build, switches/switch_chaceon_shrd, compiles. A routine's range also holds the code of other switches (#ifdef W3_MPI, W3_T test prints, other physics), so a translated line can be one the target never compiles.

Z3 reads the switches. WW3 picks code in two ways, and both become formulas over one Boolean per switch: the CMake rules choose the files (model/src/cmake/switches.json gives each switch its build_files; src_list.cmake and CMakeLists.txt list the rest), and #ifdef, #ifndef, #if, #elif, #else choose the lines. A switch file compiles a line when the switch set implies the line's condition (refutation: unsat). Z3 also checks each switch file against the rules of check_switches.cmake (one option per "one" category, at most one or two per "upto" category, no conflicts, every requires), and calls a line dead when no switch set that the rules accept compiles it. Macros that are not switches (TEST_*, ENABLE_*, COAMPS...) are off, as in a build with no -D flag, and NetCDF is found, as in chaceon's build.

z3-scala/z3.sh coverage           # fetch both pins into port-audit/.cache (13 MB), print, ~25 s
z3-scala/z3.sh coverage --write   # rewrite the block below
z3-scala/z3.sh coverage --check   # exit 1 when the block is stale (checks/port-audit.sh runs it)

What it cannot tell: whether a compiled line runs in a given run (a compiled branch can be dead at run time; chaceon's captures and cmp answer that), and whether the Rust of a translated line is right. A row of rust/ports.tsv that names a whole file counts the whole file.

One finding about WW3 itself: STAB3 can never be built. switches.json gives it "requires": ["ST3", "ST4"], and check_switches.cmake reads each string of requires as a switch that must be on (only a nested array means "one of"), while the source-term category allows exactly one ST option. The intent looks like [["ST3", "ST4"]]; this is not reported to WW3.

Generated by z3-scala/z3.sh coverage --write from chaceon fe531e1e (rust/ports.tsv, switches/) and WW3 92e2cf66 (model/src/*.F90, 135 files, and its CMake rules). Unit: Fortran code lines.

Translated lines that are dead: 104. Switch options that no accepted switch set can turn on: STAB3.