float-aligned-quantize.tri (3610B)
1 -- Positive normalized-magnitude addition/subtraction followed by one RNE. 2 -- Input (dominantScale, (gap, (a,b))); exact value is 3 -- (a +/- b*2^-gap) * 2^(dominantScale-2304). 4 -- Preconditions: 2^52<=a,b<2^53, scale>=3, gap>=0; 5 -- near branch additionally scale>=gap; subtraction at gap zero needs a>=b. 6 -- Operands are positive normalized significands satisfying these preconditions. 7 !import native_math as N 8 !import kernels as K 9 !import quantize as Q 10 !import fast as F 11 !import pipelines as P 12 !export * 13 -- For gap>=55, 0<b*2^-gap<1/4. Replace it with a same-direction 14 -- 1/8 perturbation. All relevant RNE midpoints classify identically. 15 above a = t (t t) (F.zeros2 a) 16 below a = t (t t) (t (t t) (t (t t) (N.predecessor a))) 17 farAdd scale a = F.selective (N.subtract scale 3) (above a) 18 farSubtract scale a = F.selective (N.subtract scale 3) (below a) 19 -- Under the normalized-a invariant, normal-range far results are unchanged; 20 -- above the maximum scale even the subtract case stays beyond overflow midpoint. 21 fastFar scale a tiny = K.lazy (_ : Q.answer Q.infinity (t t) t) 22 (_ : K.lazy 23 (_ : Q.answer (F.pack (N.successor (N.subtract scale 1230)) a) (t t) t) 24 tiny (N.gte scale 1230)) (N.gt scale 3275) 25 add scale gap a b = K.lazy (_ : fastFar scale a (_ : farAdd scale a)) 26 (_ : F.selective (N.subtract scale gap) (N.add (F.shiftSelective gap a) b)) (N.gte gap 55) 27 subtract scale gap a b = K.lazy (_ : fastFar scale a (_ : farSubtract scale a)) 28 (_ : F.selective (N.subtract scale gap) (N.subtract (F.shiftSelective gap a) b)) (N.gte gap 55) 29 addOne x = let scale = K.head x in let rest = K.tail x in 30 let gap = K.head rest in let ab = K.tail rest in 31 add scale gap (K.head ab) (K.tail ab) 32 subtractOne x = let scale = K.head x in let rest = K.tail x in 33 let gap = K.head rest in let ab = K.tail rest in 34 subtract scale gap (K.head ab) (K.tail ab) 35 adds xs = K.map addOne xs 36 subtracts xs = K.map subtractOne xs 37 -- Negative control: discard the residual and adjust the inexact flag. 38 discardOne x = let rounded = F.selective (K.head x) (K.head (K.tail (K.tail x))) in 39 t (K.head rounded) (t (t t) (N.lt (K.head rounded) 4503599627370496)) 40 discardControl xs = K.map discardOne xs 41 -- Compare with a genuinely exact, materialized shift for bounded control gaps. 42 exactAddOne x = let scale = K.head x in let rest = K.tail x in 43 let gap = K.head rest in let ab = K.tail rest in 44 F.selective (N.subtract scale gap) (N.add (P.shiftLeft gap (K.head ab)) (K.tail ab)) 45 exactSubtractOne x = let scale = K.head x in let rest = K.tail x in 46 let gap = K.head rest in let ab = K.tail rest in 47 F.selective (N.subtract scale gap) (N.subtract (P.shiftLeft gap (K.head ab)) (K.tail ab)) 48 exactAdds xs = K.map exactAddOne xs 49 exactSubtracts xs = K.map exactSubtractOne xs 50 -- Far-path diagnostics rely on the trusted normalized-b invariant. 51 farAddDemand x = add 1177 55 4503599627370496 (Q.spin x) 52 farSubtractDemand x = subtract 1178 55 6755399441055744 (Q.spin x) 53 cancellationDemand x = subtract (Q.spin x) 0 4503599627370496 4503599627370496 54 -- General same-direction surrogate retained as an ablation on far inputs. 55 surrogateAddOne x = let scale = K.head x in let rest = K.tail x in 56 farAdd scale (K.head (K.tail rest)) 57 surrogateSubtractOne x = let scale = K.head x in let rest = K.tail x in 58 farSubtract scale (K.head (K.tail rest)) 59 surrogateAdds xs = K.map surrogateAddOne xs 60 surrogateSubtracts xs = K.map surrogateSubtractOne xs 61 normalAddDemand x = add 2252 55 4503599627370496 (Q.spin x) 62 normalSubtractDemand x = subtract 2252 55 4503599627370496 (Q.spin x) 63 overflowDemand x = add 3276 55 (Q.spin x) (Q.spin x)