Repository navigation
Sync: single-precision refusal, framework inputs, band solve - #19
Merged
Merged
Conversation
… folds it into `uaf(p)**2._r8` is a real power, so the literal-exponent rule read no literal and what was emitted was a `pow` call. NumPy answers that one ULP away from `x*x` on about one scalar value in a thousand -- rarely enough that a noon recording of ELM's CanopyFluxes passed bit-exact for months, often enough that a day of it fails on two points of 321,888. GCC folds `pow(x, 2.0)` into the multiplication unconditionally, because that is what the call must return anyway, so the reference binary never made the call. `integral_real_literal` reads the whole-number value of a real literal; the emitter folds it only for 2. Every other whole-number real exponent GCC expands under `-funsafe-math-optimizations` alone, so `**3._r8` and `**(10._r8` stay the call the reference makes, and `getlblcef`'s own `**1.5`, `**1.75` and `**(2._r8/3._r8)` were measured to reproduce the Fortran bit for bit as plain `pow` calls. corpus/elm_leaf carries the shape: the laminar boundary resistance as CanopyFluxes spells it, on drawn values and on one value where the two lowerings disagree. The drawn ones alone did not catch it -- 30 points at one in a thousand pass either way, which is the same reason the noon recording missed it -- so the case pins a friction velocity from nstep 17548 and fails 23/30 points without the fold. The difference is the scalar path only: NumPy turns `array ** 2.0` into `square`, which is the multiplication, and the test says so, so nobody concludes from an array experiment that there is nothing here. Closes 80. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01NJHkv7eHfxh3it54chKLYj Signed-off-by: lewisychen <yueqichen.0x0@gmail.com> Carried-From: 93a7a1cb0d695b060d764fba01da20c3546cb360
…st (83, 84) Two measures the ELM diurnal recording found wrong, each narrow enough to land on its own. **83.** ELM allocates a patch array over every subgrid slot a gridcell could hold and writes elm_varcon's spval into the ones no patch uses. The gate took its scale from the array's largest magnitude, so a 1e36 in an unused slot put every real value of the array three dozen orders below the dominance bar and the ULP tier could never fire -- `max_ulp_dominant` came back 0 for what turned out to be a real emitter defect. The same elements were compared, matched (1e36 equals 1e36) and counted, so 74% of the 321,888 points a day of CanopyFluxes claimed were "no data == no data"; excluding them leaves 82,192, and no verdict moves. The extension declares the value, because only it knows: recast-elm's two recipes now carry `fill_values: [1.0e36]`. **84.** Canopy water goes into an afternoon step at 2.4e-2 and comes out at 7.7e-7. The JAX kernel's difference there is 1.3e-15, which against the quantity that cancelled is 5e-14 -- the same class as every other output of that kernel, with the NumPy translation bit-exact -- and the five-order cancellation turns it into 11,864,064 ULP of the residue. Where an output is a state the kernel updated in place and the update collapsed it, the difference is now judged against the value it updated. Only a *shrinking* update qualifies (COLLAPSE_AT), so the rule excuses what a cancellation explains and nothing else: a verdict that passes today cannot turn red because of it. What 83 does turn red is real: with the fill no longer hiding it, ELM's port ULP tier fires for the first time, and the kernel does not meet 32 ULP per element. The worst is `u10 = ur - ustar/vkc*(...)`, two quantities of order 1.44 leaving 0.0053 -- an amplification of 270, so an ordinary 1.5e-13 relative error on the subtrahend is the whole of the residual's 2.1e-13. That cancellation is between locals, which no signature names and this rule cannot reach; the evidence is on 81, which is where it belongs. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01NJHkv7eHfxh3it54chKLYj Signed-off-by: lewisychen <yueqichen.0x0@gmail.com> Carried-From: 50bf90b408ba2a023596690a2409874d0e740b84
…ed it Two verdicts that both read TOLERANCED are not the same claim: one met the relative bound, the other exceeded both bounds and was excused by the reference's own measured spread. Telling them apart meant reading a sentence of English, and the measurement behind the second was dropped before the summary was written -- `metrics` keeps only scalars, on purpose, because the file is written to be diffed, and the conditioning block is a dict. So: `metrics["tier"]` on every path (`bit-exact`, `ulp`, `relative`, `conditioning`, `none`), and the conditioning measurement twice -- the whole block for the evidence file, its three summary numbers as scalars for the committed record. The file stays flat. What that makes visible: CLUBB's cases-e3sm whole step is excused by an envelope of 42,613,738 ULP, ELM's CanopyFluxes at noon by 6,422,528, and a day of the same ELM routine measures 460 -- five orders, on the same code path, and until now nobody could see it without opening an evidence file by hand. 81 needs exactly that history to judge a replacement criterion against the one in force, which is why this lands first. The four committed corpus port summaries gain the field and nothing else. Closes 85. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01NJHkv7eHfxh3it54chKLYj Signed-off-by: lewisychen <yueqichen.0x0@gmail.com> Carried-From: 405f13d8d9a04f22ed7c5b2aec2d3b994122705e
The tolerance gate holds a port's value to the recording and says nothing about its derivative, which is a second program XLA builds from the same source. ELM's CanopyFluxes port was bit-exact on 1488 recorded steps with a NaN Jacobian on seven of them: sqrt at an exactly zero discriminant, infinite slope times a zero tangent. ``differential.finite-derivative`` differentiates the port's own jitted kernel in forward mode along a random Gaussian direction in the real inputs, on every recorded sample, and requires the tangent finite wherever the value is. One direction detects any non-finite Jacobian entry with probability one, so the seed is on the verdict and more directions are a knob. The wrapper is called concretely first so a tree port's state binding has happened; the kernel's ``static_argnums`` are read from the emitted ``jax.jit`` call and the arguments they name are reported as not differentiated rather than counted as checked. Fill values are neither perturbed nor judged; a non-finite value is the value gate's business and is excluded here. It awards ``SAMPLED``: a property on the recorded samples, with no reference to agree with. ``port`` gains ``derivatives: true``, which adds the stage as a gate after the tolerance gate and is refused without the replay oracle or a JAX backend. Conformance case, export tier, and the import contract's exemption (JAX is the instrument) come with it. The end-to-end test is the 88 kernel itself -- ``sqrt(max(x - c, 0))`` recorded at ``x == c`` -- passing on the runtime's ``_f_sqrt``. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Signed-off-by: lewisychen <yueqichen.0x0@gmail.com> Carried-From: 9b1a3b7ab86c3ab03a3e592b6f6e51888d47b29e
…ions, classify parameters over use-imported constants - Refuse flat kernels the anchor defers, alias allocation locals, take DATA sections - Classify a module parameter over a use-imported constant Signed-off-by: lewisychen <yueqichen.0x0@gmail.com> Carried-From: d742a91af04ae9c8fb05078587cd1c41dab0e9a5
…he runtime's banded solver - Bind a bare call to a library procedure recast supplies - Add the band_solve corpus case Signed-off-by: lewisychen <yueqichen.0x0@gmail.com> Carried-From: d709a3f1a42adea53b9b853c7bd74616d22a9212
ELM's shr_spfn_mod has calerf_r4 beside calerf_r8, the same erf with
`integer, parameter :: rk = r4` and `real(rk)` throughout. The numpy
renderer emitted the r4 routine entirely in float64 -- `np.float64('0.5E0')`
for `0.5E0_rk`, `y = abs(x)` on doubles -- with nothing but `# SKIPPED
local` hoisting notes to show for it, while the constants fold refuses the
same fact in a single constant ("this fold has no single-precision
arithmetic"). A call to shr_spfn_erf_r4 would have returned a double erf
where the Fortran returns a single, and the bit-exact gate would have failed
on it with no note pointing at the kind.
Two causes, both fixed:
* the frontend typed `real(rk)` as UNKNOWN_REAL_KIND(rk) because the kind
map was the module's only, and every consumer read an unknown kind as a
double. `local_kind_aliases` now reads a routine's own integer kind
parameters (`rk = r4`, `rk = selected_real_kind(12)`, `rk = 8` where a
declaration spells it as a kind) against the module's map, the
subprogram record carries them as `kind_map`, and the declarations, the
result, the constants fold of the local parameters and the expression
renderer's kind lookups all resolve through them. calerf_r8's
declarations are float64 now, and its `0.5E0_rk` folds instead of being
skipped as a kind the fold does not know.
* the prologue refuses a subprogram any of whose dummies, result, locals
or local parameters is float32 or complex64 -- a named single kind, the
bare default real, or an alias of either -- as P001 with every such
entity named, and raises before a statement of the body can run. This is
the existing single-precision policy applied at the routine's scale.
Four test fixtures that declared bare `real` dummies for rules unrelated to
precision now say `real(8)`. The numfor corpus baseline moves by the three
`real(sp)` routines of its strings unit (deferred 2 -> 5, already stopped
by static.rwset); no other case declares a single-precision entity.
Closes 97.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Signed-off-by: lewisychen <yueqichen.0x0@gmail.com>
Carried-From: e898f10b641bf05ab53f088448f38e3b9699d309
ELM's CanopyHydrology and the SoilTemperature data types read the step
size as `dtime = get_step_size()` from elm_time_manager, a module the ELM
extension stands in: its Fortran reads an ESMF clock and cannot be
translated. The stand-in carried the module's initialized entities and
whatever the framework table answered, which for elm_time_manager was
nothing, so the emitted `_elm_time_manager.get_step_size()` was a call
into nothing -- an AttributeError the first time the kernel ran or
traced, and nothing in the translation, the plan or the notes said so.
recast-elm's chain scripts monkeypatched the stand-in with the recorded
`timeinfomod__dtime_mod`, the case supplying a fact the engine should have
asked for.
The rule: an argument-less function of a stub module the unit imports is
a recorded input of the unit, like the module state it reads.
* frontend -- among the stub procedures, a name that is a function with no
dummies in the tree's source of the stub module, with a result a flat
scalar can carry (real, integer, logical, character), goes on the record
as `framework_inputs: [{module, name, local, dtype}]`. A function
returning a derived type (the ESMF time) stays a stub call.
* flatten -- every plan of the unit carries each as the scalar IN
`<module>__<function>`, after the module-state inputs; the stand-in's
answer is one per process, and a callee of the planned subprogram may be
the one that asks.
* oracle/record -- the probe `use`s the function and writes its value as
`# <module>__<function> = ` from a call inside the model, where the stub
module is the real one; a character result through `trim`.
* numpy stand-in -- defines the function as a read of `_answers[name]`,
which the Python flat adapter sets from the argument before the body
runs; a call with nothing set raises with the rule's name instead of
AttributeError. The framework table wins where it defines the same name.
Every stand-in also gains a module `__getattr__` that says what a stub
module can answer, so a name it never carried is refused by name at the
call rather than as a bare AttributeError at the first trace.
* oracle/flat -- the Fortran adapter declares the argument for the shared
signature and says the callee asks the real module itself.
* jax -- the lowering spells `_mod.fn()` as the flat argument; the kernel
makes no call. The value follows the existing `_concrete_scalars` rule
(`dt = _f_pyfloat(_f_float64(clock_mod__step_size))`).
The ELM recording format gains one input per such function the staged
units import (get_step_size, get_nstep, is_first_step, get_calendar, ...);
the case re-records and drops the monkeypatch. CLUBB is unaffected: its
time step is a dummy argument.
Closes 96.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01MsNgub51rv3thHx5mu8ZcL
Signed-off-by: lewisychen <yueqichen.0x0@gmail.com>
Carried-From: c399de7dd35799861273b907092c5b177fde0f19
A unit's subprograms each `use` the stub module for themselves: ELM's CanopyHydrology imports get_step_size in two routines, and the record listed it twice, so the plan carried two arguments of one name and the recorder wrote the line twice. One entry per (module, function). Found on the staged whole-step tree at the first analyze after 99. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MsNgub51rv3thHx5mu8ZcL Signed-off-by: lewisychen <yueqichen.0x0@gmail.com> Carried-From: 9464e132a60c0aa8aca88ecb128bbea5f5940b89
After 101 HydrologyNoDrainage's kernel was refused: its callee `infiltration` (SoilHydrologyMod, a companion) reads get_nstep(), the companion's own plan carried `elm_time_manager__get_nstep`, and the caller's plan did not -- the reach stopped at the unit's own subprograms. The walk now follows calls into the companion procedures the planner's index already knows, and resolves each visited module's own stub imports, so a plan carries every argument-less framework function any procedure it reaches can call (`_framework_inputs_reached`). On the staged tree: CanopyHydrology get_nstep + get_step_size, CanopyFluxes get_step_size (through a companion), HydrologyNoDrainage get_nstep + get_step_size, the other four none. Two consequences fixed with it: the unit's stand-in for the stub module now replaces the one a bundled companion brought (the unit's plans reach the companion's calls, not the other way round), and it answers the union of the record's and every plan's inputs. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MsNgub51rv3thHx5mu8ZcL Signed-off-by: lewisychen <yueqichen.0x0@gmail.com> Carried-From: 4540abb722e14723680770c542dbf6402a850b87
chenyueqi
force-pushed
the
sync/september-17
branch
from
September 17, 2026 21:56
55d575e to
f1cd296
Compare
`integral_real_literal` reused `value` for the float a literal parses to and for the `int | None` a signed operand folds to; mypy has flagged the two assignments since the rule landed. Two names, no behaviour change; the type check is clean again on both editions. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MsNgub51rv3thHx5mu8ZcL Signed-off-by: lewisychen <yueqichen.0x0@gmail.com> Carried-From: 1376f0c3cb0729129f278ed98dc2016b83bee5a6
…olds corpus/baseline.json had been regenerated for numfor alone while the rules of 91 and 92 had already moved fortran-utils: four external calls now translate (blocks 540 -> 544, deferred 54 -> 50), one linalg block and all three splines blocks with them. The public edition's corpus job runs `tools/corpus.py run` on a clean machine and diffs the file, and it said so. Regenerated whole; the numbers are the runner's to the digit. The scalar-pow test asserted that pow(x, 2.0) differs from x * x on one ELM value; that is Apple's libm. glibc folds it to the multiplication to the bit, so on the public runner the test failed on a fact about the platform, not about the rule. The array path is asserted everywhere; the scalar inequality is skipped where the library agrees. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MsNgub51rv3thHx5mu8ZcL Signed-off-by: lewisychen <yueqichen.0x0@gmail.com> Carried-From: 70d8fe5f7ee920a0c59722e83ea5f1b4d328d55e
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Carried by tools/export sync; each commit names its origin in a Carried-From trailer.