float-working.tri (8181B)
1 -- Retain rounded working values across operations; pack at interchange. 2 -- Value (kind,(sign,(scale,payload))): kind 0 zero, 1 finite, 2 infinity, 3 NaN. 3 -- Finite payload is normalized 53-bit significand, scale 1178..3275. 4 -- NaN payload is raw 52-bit fraction (including quiet bit). Zero/inf use 0,0. 5 -- Input words/instructions satisfy the same trusted contract as C.cached. 6 !import native_math as N 7 !import kernels as K 8 !import layouts as L 9 !import fast as F 10 !import quantize as Q 11 !import near as H 12 !import adders as A 13 !import finite as B 14 !import product_quotient as P 15 !import ieee as I 16 !import chains as C 17 !export * 18 make kind sign scale payload = t kind (t sign (t scale payload)) 19 kind x = K.head x 20 sign x = K.head (K.tail x) 21 scale x = K.head (C.drop2 x) 22 payload x = C.drop3 x 23 zero x = N.zero (kind x) 24 inf x = N.equal (kind x) 2 25 nan x = N.equal (kind x) 3 26 zeroValue sign = make 0 sign 0 0 27 infinity sign = make 2 sign 0 0 28 invalidResult = I.answer (make 3 t 0 2251799813685248) (t t) t t t t 29 withSign negative x = t (kind x) (t negative (C.drop2 x)) 30 signed negative reply = t (withSign negative (K.head reply)) (K.tail reply) 31 fromWord word = let e = B.exponent word in let f = L.low52 word in let negative = B.signBit word in K.lazy 32 (_ : K.lazy (_ : infinity negative) (_ : make 3 negative 0 f) (N.zero f)) 33 (_ : K.lazy 34 (_ : K.lazy (_ : zeroValue negative) 35 (_ : let normalized = B.subnormal f in make 1 negative (K.head normalized) (K.tail normalized)) (N.zero f)) 36 (_ : make 1 negative (N.add e 1229) (F.pack 1 word)) (N.zero e)) (N.equal e 2047) 37 toWord value = let magnitude = K.lazy (_ : 0) 38 (_ : K.lazy (_ : K.lazy 39 (_ : F.pack (N.subtract (scale value) 1229) (payload value)) 40 (_ : K.head (K.shiftL (N.subtract 1230 (scale value)) (payload value))) (N.gte (scale value) 1230)) 41 (_ : K.lazy (_ : 9218868437227405312) (_ : F.pack 2047 (payload value)) (inf value)) 42 (N.equal (kind value) 1)) (zero value) in B.attach (sign value) magnitude 43 -- Combine precision/minimum-exponent cuts, then normalize each nonzero rounded 44 -- result, including subnormals, to a 53-bit working significand. 45 finish scale m width ix tiny = K.lazy 46 (_ : I.answer (zeroValue t) t t t ix ix) 47 (_ : let pad = N.subtract 53 width in let s = N.subtract scale pad in 48 let normalized = F.shiftSelective pad m in K.lazy 49 (_ : I.answer (infinity t) t t (t t) t (t t)) 50 (_ : let uf = K.both ix (K.either (N.lt s 1230) 51 (K.both (N.equal s 1230) (K.both (N.equal normalized 4503599627370496) (tiny t)))) in 52 I.answer (make 1 t s normalized) t t t uf ix) (N.gt s 3275)) (N.zero m) 53 carry scale m ix tiny = let width = K.width m in K.lazy 54 (_ : finish (N.successor scale) (K.tail m) (N.predecessor width) ix tiny) 55 (_ : finish scale m width ix tiny) (N.gt width 53) 56 quantize scale n = K.lazy (_ : I.exact (zeroValue t)) 57 (_ : let cut = Q.max (N.subtract (K.width n) 53) (N.subtract 1230 scale) in 58 let rounded = K.roundL cut n in 59 carry (N.add scale cut) (K.head rounded) (K.tail rounded) (_ : I.precisionTiny scale n)) (N.zero n) 60 -- Finite input scales guarantee a far-gap dominant operand is normal: since 61 -- min scale is 1178, gap >=55 implies dominant scale >=1233 (and <=3275). 62 magnitude subtract s gap a b = K.lazy 63 (_ : I.answer (make 1 t s a) t t t t (t t)) 64 (_ : K.lazy 65 (_ : let shifted = F.shiftSelective gap a in 66 quantize (N.subtract s gap) (K.choose (N.subtract shifted b) (N.add shifted b) subtract)) 67 (_ : let wide = H.wide a in let aligned = H.align gap b in 68 quantize (N.subtract s 3) (K.choose (N.subtract wide aligned) (N.add wide aligned) subtract)) 69 (N.lt gap 8)) (N.gte gap 55) 70 ordered a b = let subtract = K.xor (sign a) (sign b) in let gap = N.subtract (scale a) (scale b) in K.lazy 71 (_ : I.exact (zeroValue t)) 72 (_ : signed (sign a) (magnitude subtract (scale a) gap (payload a) (payload b))) 73 (K.both subtract (K.both (N.zero gap) (N.equal (payload a) (payload b)))) 74 finiteAdd subtract a originalB = let b = withSign (K.xor subtract (sign originalB)) originalB in K.lazy 75 (_ : K.lazy (_ : I.exact (zeroValue (K.both (sign a) (sign b)))) (_ : I.exact b) (zero b)) 76 (_ : K.lazy (_ : I.exact a) 77 (_ : K.lazy (_ : ordered a b) (_ : ordered b a) (B.dominates (K.tail a) (K.tail b))) (zero b)) (zero a) 78 finiteProduct a b = let negative = K.xor (sign a) (sign b) in K.lazy 79 (_ : I.exact (zeroValue negative)) 80 (_ : signed negative (quantize (N.subtract (N.add (scale a) (scale b)) 2304) 81 (A.orderedMultiply (payload a) (payload b)))) (K.either (zero a) (zero b)) 82 finiteQuotient a b = let negative = K.xor (sign a) (sign b) in K.lazy 83 (_ : I.exact (zeroValue negative)) 84 (_ : signed negative (quantize (N.subtract (N.add 2248 (scale a)) (scale b)) 85 (P.jam (P.boundedQuotient (payload a) (payload b))))) (zero a) 86 signaling x = K.both (nan x) (K.not (I.quietBit (payload x))) 87 nanResult a b = let chosen = K.choose a b (nan a) in 88 I.answer (make 3 (sign chosen) 0 (I.quiet (payload chosen))) 89 (K.either (signaling a) (signaling b)) t t t t 90 add subtract a b = let sa = sign a in let sb = K.xor subtract (sign b) in K.lazy 91 (_ : K.lazy (_ : invalidResult) (_ : I.exact (infinity (K.choose sa sb (inf a)))) 92 (K.both (K.both (inf a) (inf b)) (K.xor sa sb))) 93 (_ : finiteAdd subtract a b) (K.either (inf a) (inf b)) 94 multiply a b = let negative = K.xor (sign a) (sign b) in K.lazy 95 (_ : K.lazy (_ : invalidResult) (_ : I.exact (infinity negative)) (K.either (zero a) (zero b))) 96 (_ : finiteProduct a b) (K.either (inf a) (inf b)) 97 divide a b = let negative = K.xor (sign a) (sign b) in K.lazy 98 (_ : K.lazy (_ : invalidResult) (_ : I.exact (infinity negative)) (inf b)) 99 (_ : K.lazy (_ : I.exact (zeroValue negative)) 100 (_ : K.lazy (_ : K.lazy (_ : invalidResult) 101 (_ : I.answer (infinity negative) t (t t) t t t) (zero a)) 102 (_ : finiteQuotient a b) (zero b)) (inf b)) (inf a) 103 operation op a b = K.lazy (_ : add t a b) 104 (_ : K.lazy (_ : add (t t) a b) 105 (_ : K.lazy (_ : multiply a b) (_ : divide a b) (N.equal op 2)) (N.equal op 1)) (N.zero op) 106 step op a b = K.lazy (_ : nanResult a b) (_ : operation op a b) (K.either (nan a) (nan b)) 107 keep x = x 108 roundtrip x = fromWord (toWord x) 109 lookupFresh index pool = fromWord (C.at index pool) 110 walk convert lookup pool instructions state flags = K.triage (t state flags) (_ : t state flags) 111 (instruction rest : let next = step (K.head instruction) state (lookup (K.tail instruction) pool) in 112 walk convert lookup pool rest 113 (K.lazy (_ : K.head next) (_ : convert (K.head next)) (N.zero rest)) 114 (C.flagsOr flags (K.tail next))) instructions 115 chain convert lookup pool input = walk convert lookup pool (K.tail (K.tail input)) 116 (fromWord (K.head input)) (K.tail (I.exact 0)) 117 internal input = chain keep C.at (K.map fromWord (K.head (K.tail input))) input 118 internalRoundtrip input = chain roundtrip C.at (K.map fromWord (K.head (K.tail input))) input 119 internalFresh input = chain keep lookupFresh (K.head (K.tail input)) input 120 interchange reply = t (toWord (K.head reply)) (K.tail reply) 121 working input = interchange (internal input) 122 workingRoundtrip input = interchange (internalRoundtrip input) 123 workingFresh input = interchange (internalFresh input) 124 checkedBatch xs = C.checkedBatch xs 125 cachedBatch xs = C.cachedBatch xs 126 workingBatch xs = K.map working xs 127 roundtripBatch xs = K.map workingRoundtrip xs 128 freshBatch xs = K.map workingFresh xs 129 internalBatch xs = K.map internal xs 130 transportOne w = toWord (fromWord w) 131 transport xs = K.map transportOne xs 132 quantizedOne x = interchange (quantize (K.head x) (K.tail x)) 133 quantized xs = K.map quantizedOne xs 134 retainWords xs = xs 135 retainCached xs = K.map C.prepare xs 136 retainWorking xs = K.map fromWord xs 137 spin x = spin x 138 emptyDemand x = working (t 9223372036854775808 (t (spin x) t)) 139 unusedDemand x = working (t 4607182418800017408 (t (t 0 (spin x)) (t (t 0 0) t))) 140 zeroScaleDemand x = interchange (quantize (spin x) 0) 141 farDemand x = interchange (magnitude t 2252 55 4503599627370496 (spin x)) 142 nanWordDemand x = toWord (K.head (step 0 (make 3 t 0 2251799813685249) (spin x))) 143 zeroProductDemand x = interchange (finiteProduct (zeroValue t) (make 1 (t t) (spin x) (spin x)))