Type-core: natural float params + results (Increments A/A+/B)#7
Merged
Conversation
…er fns work param_is_float now marks a param __float_ when it is an operand of a comparison (< > <= >= == !=) whose other operand is unambiguously float (an FL literal or an already-float operand). Previously such params (e.g. minmod a b = if a < b then a else b) stayed unmarked, so `a < b` fell through to the _rail_lt runtime helper, which dereferences an even-LSB operand as a heap pointer -> data-dependent segfault (and returned the wrong value for odd-LSB bit patterns). This is safe where the arithmetic-sibling rule was not: `int < 0.0` is ALREADY mishandled today (the FL literal forces the native-float path, which reads the int's tag bits as a double), so marking here cannot break a currently-correct mixed pattern. By contrast `0.0 +. int` IS correct via runtime mixed-promotion, which is why arithmetic-sibling marking stays omitted. Real-world victim: stdlib/mhd_kernel.rail mk_minmod, which broke the entire MUSCL second-order solver path -- the repo's own tools/plasma/mhd_muscl_test.rail segfaulted. With this fix the UNMODIFIED kernel runs: machine-precision conservation (dm 2e-13, dE 6e-15), divB growth as documented, sharpness ratio 1.76 vs LF. t136 float_user_fn_minmod locks the regression. 142/142, byte-identical self-compile fixed point (gen2 == gen3).
…ia call-site agreement A user-fn param is marked __float_ when EVERY call site passes a provably-float arg (infer_ty==2) in that position -- new __argf_<fn>_<i> whole-program analysis (collect_argf/argf_scan) with a COMPLETE AST traversal (incl. lambda bodies), partial-application demotion, and value-reference demotion (a fn used as a value can't have its indirect calls enumerated -> demote). Hooked in compile_func after mark_float_params. Monotone-safe: any int/unknown/under-applied/value-ref site demotes the slot, so legit int-param code is never mismarked. Fixes the long-standing bug: mul2 a b = a * b; mul2 3.0 4.0 was 4.94e-324 (tagged ints read as doubles), now 12. Validated: 144/144 (new t137 arith_float_2arg + t138 argf_int_param_safe guard), byte-identical 2-pass fixed point (gen2==gen3), diff-fuzzer 20/20 agree / 0 divergence. Found en route (out of scope, NOT fixed): 0.0 + int_param is a SEPARATE pre-existing miscompile (denormal via the use_float else-fmov path) -- the design doc's 'mixed-promotion correct for params' claim is false. Candidate for a later increment (runtime tag-check on unknown float-context operands).
…es 0.0+int_param denormal) Generalizes Increment A's call-site analysis to a true lub: a param's __argf_<fn>_<i> slot is 2 iff EVERY call site is float, 1 iff every site is int, else 0 (mixed/unknown/value-ref/under-applied). compile_func marks the param __float_ (slot 2) or __int_ (slot 1, never overriding an existing __float_). An int param in a float context (0.0 + x) is then scvtf-promoted instead of read as float bits. Fixes the denormal found during Increment A: addk x = 0.0 + x; addk 5 was 5.43e-323, now 5. Validated: 145/145 (new t139 argi_int_into_float), byte-identical fixed point (gen2==gen3), diff-fuzzer 20/20 agree / 0 divergence. Monotone-safe by the lub (any disagreeing site -> unmarked).
…type-core fixes A 2-layer MLP forward pass (5-float-param neurons, chained hidden activations, ReLU) written with float scalars as ordinary params -- no float_arr boxing, no out-cell workarounds. SEGFAULTS on the pre-type-layer compiler (master 548dcd7); runs correctly since d653a72 + f6231c8 (A) + f042b6b (A+). Verified before/after: master crashes, this prints mlp(1.0,2.0)=1.125 / mlp(1.0,0.0)=0.375.
…nt inference fixpoint) Execution-ready handoff for a fresh dedicated session to tackle the fixed-point-risky float-RESULT inference fixpoint (the mse/loss-composition gap diagnosed this session). Includes the minimal repro, keystone line refs (returns_float:1989, infer_ty:2411, get_arities two-phase), a Phase-0-diagnose-first plan, the bootstrap discipline + gates, and the gotchas. Deliberately deferred from marathon-tail per the never-gamble-the-fixed-point rule.
…marker A float user-fn RESULT bound to a let-local (let y = mlp 1.0 2.0) now composes as a float at a later call site (mse y 1.0): was 5.3e+36 garbage, now 0.015625. Unblocks natural ML code (autograd/transformer) where a forward pass is bound to a local before loss/activation. Mechanism: argf_scan's let case (new argf_scan_d) threads a __vf_<name> marker into the rmap iff the bound value is provably float (infer_ty==2); infer_ty's "V" case reads it so a bare local contributes FLOAT(2) instead of UNKNOWN(0). __argf_mse_0 then sees y as float -> pred marked __float_ -> d*d takes the float-mul path. Inert for int code (infer_ty never 2 there; TD tuple-lets are HEAP-typed so the marker branch never fires) -- diff-fuzzer grammar unaffected. Phase 0 empirically showed Increment A (call-site agreement) was already landed, so the only remaining gap was let-local propagation: a 2-edit fix, not the design's feared 2.8 joint fixpoint. Locked by t140 float_result_compose; 146/146, byte-identical fixed point (gen2==gen3), diff-fuzzer seed=42 n=20 (20/20 agree, 0 divergence). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…ndently verified Increment B (float-result-compose) is done and re-verified from source by a separate session. Records the conclusion + findings on the handoff doc: - What landed: a 2-edit additive fix (argf_scan_d __vf_ marker + infer_ty V-case), NOT the feared joint inference fixpoint. Two-pass machinery left untouched. - Independent verification (throwaway worktree, canonical clone + beacon untouched): 146/146; mse y 1.0 -> 0.015625; mlp_natural unchanged; diff-fuzzer 20/20; byte-identical fixed point (self-compile SHA-256 b5e35770...de3df1 == committed); t140 confirmed a real regression lock (parent bec321f, same source -> 5.3e+36). - Verdict: correct and honest -- scope claimed == scope delivered. - Finding: the handoff's required-reading ref (rail-compiler-phase-design.md §2.8) lives on feat/verifiable-language @ 337d66a, not this branch; noted inline. - Open: recursive-return + show-on-unboxed-float (Phase 2) deliberately not done. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
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.
Summary
Makes float scalars work as ordinary user-function parameters AND results, so natural ML code compiles without
float_arrboxing or out-cell threading. This is the "checked type layer" enabling substrate for the verifiable-language pillars (auth-typed data, attested numerics, source-to-source AD).Three compiler increments + a proof example + handoff/findings docs (all gated to the byte-identical self-hosting fixed point):
d653a72— comparison float-params:a < bhitsfcmpinstead of_rail_ltderef-segfaultf6231c8— Increment A (arithmetic): whole-call-site agreement (__argf_<fn>_<i>) marks a param__float_iff every call site passes a provably-float argf042b6b— Increment A+ (int-param dual): true lub (all-float→float, all-int→int); fixes the0.0 + int_paramdenormal4cf64de— Increment B (float-result-compose): a float user-fn RESULT bound to a let-local composes downstream, via a__vf_marker threaded byargf_scan_d+ read ininfer_ty's V-caseee25340— proof artifactexamples/mlp_natural.rail(segfaults on master, runs on this branch)bec321f/dcf255f— Increment B handoff + the independent-verification findingsWhat it fixes (before → after, identical source)
mul2 3.0 4.04.94e-32412addk 5(0.0 + x)5.43e-3235let y = mlp 1.0 2.0; mse y 1.05.3e+360.015625neuron(arity ≥4)Verification (independently reproduced from source, not trusted)
b5e357706114f2106fece1e87a1b105528d9d0d5b4cf0f8cf0ac9bb751de3df1--seed=42 --n=20→ 20 agree / 0 divergenceexamples/mlp_natural.rail→1.125 / 0.375 / 0 / 2.75t140confirmed a real regression lock (parentbec321f→5.3e+36on identical source)returns_float/collect_float_ret_fnsmachinery is untouched — the fix is strictly additive, inert for int code (fuzzer grammar unaffected)Deliberately NOT included
Recursive-float-return +
showon an unboxed float (Phase 2). The joint-fixpoint + param V-tweak path remains documented for if/when it's needed.Test plan
./rail_native test→ 146/146./rail_native self→ byte-identical fixed point (cmp rail_native /tmp/rail_self)./rail_native run tools/fuzz/diff_fuzz.rail --seed=42 --n=20→ 20/20 agree./rail_native run examples/mlp_natural.rail→ 1.125 / 0.375 / 0 / 2.75🤖 Generated with Claude Code