working.tri (5665B)
1 -- Pure binary64 implementation; trusted internal helpers. 2 !import native_math as N 3 !import binary64_kernels as K 4 !import binary64_layouts as L 5 !import binary64_fast as F 6 !import binary64_quantize as Q 7 !import binary64_near as H 8 !import binary64_adders as A 9 !import binary64_finite as B 10 !import binary64_product_quotient as P 11 !import binary64_ieee as I 12 !import binary64_chains as C 13 !export fromWord 14 !export step 15 !export toWord 16 17 make kind sign scale payload = t kind (t sign (t scale payload)) 18 kind x = K.head x 19 sign x = K.head (K.tail x) 20 scale x = K.head (C.drop2 x) 21 payload x = C.drop3 x 22 zero x = N.zero (kind x) 23 inf x = N.equal (kind x) 2 24 nan x = N.equal (kind x) 3 25 zeroValue sign = make 0 sign 0 0 26 infinity sign = make 2 sign 0 0 27 invalidResult = I.answer (make 3 t 0 2251799813685248) (t t) t t t t 28 withSign negative x = t (kind x) (t negative (C.drop2 x)) 29 signed negative reply = t (withSign negative (K.head reply)) (K.tail reply) 30 fromWord word = let e = B.exponent word in let f = L.low52 word in let negative = B.signBit word in K.lazy 31 (_ : K.lazy (_ : infinity negative) (_ : make 3 negative 0 f) (N.zero f)) 32 (_ : K.lazy 33 (_ : K.lazy (_ : zeroValue negative) 34 (_ : let normalized = B.subnormal f in make 1 negative (K.head normalized) (K.tail normalized)) (N.zero f)) 35 (_ : make 1 negative (N.add e 1229) (F.pack 1 word)) (N.zero e)) (N.equal e 2047) 36 toWord value = let magnitude = K.lazy (_ : 0) 37 (_ : K.lazy (_ : K.lazy 38 (_ : F.pack (N.subtract (scale value) 1229) (payload value)) 39 (_ : K.head (K.shiftL (N.subtract 1230 (scale value)) (payload value))) (N.gte (scale value) 1230)) 40 (_ : K.lazy (_ : 9218868437227405312) (_ : F.pack 2047 (payload value)) (inf value)) 41 (N.equal (kind value) 1)) (zero value) in B.attach (sign value) magnitude 42 finish scale m width ix tiny = K.lazy 43 (_ : I.answer (zeroValue t) t t t ix ix) 44 (_ : let pad = N.subtract 53 width in let s = N.subtract scale pad in 45 let normalized = F.shiftSelective pad m in K.lazy 46 (_ : I.answer (infinity t) t t (t t) t (t t)) 47 (_ : let uf = K.both ix (K.either (N.lt s 1230) 48 (K.both (N.equal s 1230) (K.both (N.equal normalized 4503599627370496) (tiny t)))) in 49 I.answer (make 1 t s normalized) t t t uf ix) (N.gt s 3275)) (N.zero m) 50 carry scale m ix tiny = let width = K.width m in K.lazy 51 (_ : finish (N.successor scale) (K.tail m) (N.predecessor width) ix tiny) 52 (_ : finish scale m width ix tiny) (N.gt width 53) 53 quantize scale n = K.lazy (_ : I.exact (zeroValue t)) 54 (_ : let cut = Q.max (N.subtract (K.width n) 53) (N.subtract 1230 scale) in 55 let rounded = K.roundL cut n in 56 carry (N.add scale cut) (K.head rounded) (K.tail rounded) (_ : I.precisionTiny scale n)) (N.zero n) 57 magnitude subtract s gap a b = K.lazy 58 (_ : I.answer (make 1 t s a) t t t t (t t)) 59 (_ : K.lazy 60 (_ : let shifted = F.shiftSelective gap a in 61 quantize (N.subtract s gap) (K.choose (N.subtract shifted b) (N.add shifted b) subtract)) 62 (_ : let wide = H.wide a in let aligned = H.align gap b in 63 quantize (N.subtract s 3) (K.choose (N.subtract wide aligned) (N.add wide aligned) subtract)) 64 (N.lt gap 8)) (N.gte gap 55) 65 ordered a b = let subtract = K.xor (sign a) (sign b) in let gap = N.subtract (scale a) (scale b) in K.lazy 66 (_ : I.exact (zeroValue t)) 67 (_ : signed (sign a) (magnitude subtract (scale a) gap (payload a) (payload b))) 68 (K.both subtract (K.both (N.zero gap) (N.equal (payload a) (payload b)))) 69 finiteAdd subtract a originalB = let b = withSign (K.xor subtract (sign originalB)) originalB in K.lazy 70 (_ : K.lazy (_ : I.exact (zeroValue (K.both (sign a) (sign b)))) (_ : I.exact b) (zero b)) 71 (_ : K.lazy (_ : I.exact a) 72 (_ : K.lazy (_ : ordered a b) (_ : ordered b a) (B.dominates (K.tail a) (K.tail b))) (zero b)) (zero a) 73 finiteProduct a b = let negative = K.xor (sign a) (sign b) in K.lazy 74 (_ : I.exact (zeroValue negative)) 75 (_ : signed negative (quantize (N.subtract (N.add (scale a) (scale b)) 2304) 76 (A.orderedMultiply (payload a) (payload b)))) (K.either (zero a) (zero b)) 77 finiteQuotient a b = let negative = K.xor (sign a) (sign b) in K.lazy 78 (_ : I.exact (zeroValue negative)) 79 (_ : signed negative (quantize (N.subtract (N.add 2248 (scale a)) (scale b)) 80 (P.jam (P.boundedQuotient (payload a) (payload b))))) (zero a) 81 signaling x = K.both (nan x) (K.not (I.quietBit (payload x))) 82 nanResult a b = let chosen = K.choose a b (nan a) in 83 I.answer (make 3 (sign chosen) 0 (I.quiet (payload chosen))) 84 (K.either (signaling a) (signaling b)) t t t t 85 add subtract a b = let sa = sign a in let sb = K.xor subtract (sign b) in K.lazy 86 (_ : K.lazy (_ : invalidResult) (_ : I.exact (infinity (K.choose sa sb (inf a)))) 87 (K.both (K.both (inf a) (inf b)) (K.xor sa sb))) 88 (_ : finiteAdd subtract a b) (K.either (inf a) (inf b)) 89 multiply a b = let negative = K.xor (sign a) (sign b) in K.lazy 90 (_ : K.lazy (_ : invalidResult) (_ : I.exact (infinity negative)) (K.either (zero a) (zero b))) 91 (_ : finiteProduct a b) (K.either (inf a) (inf b)) 92 divide a b = let negative = K.xor (sign a) (sign b) in K.lazy 93 (_ : K.lazy (_ : invalidResult) (_ : I.exact (infinity negative)) (inf b)) 94 (_ : K.lazy (_ : I.exact (zeroValue negative)) 95 (_ : K.lazy (_ : K.lazy (_ : invalidResult) 96 (_ : I.answer (infinity negative) t (t t) t t t) (zero a)) 97 (_ : finiteQuotient a b) (zero b)) (inf b)) (inf a) 98 operation op a b = K.lazy (_ : add t a b) 99 (_ : K.lazy (_ : add (t t) a b) 100 (_ : K.lazy (_ : multiply a b) (_ : divide a b) (N.equal op 2)) (N.equal op 1)) (N.zero op) 101 step op a b = K.lazy (_ : nanResult a b) (_ : operation op a b) (K.either (nan a) (nan b))