1 import Base 2 import ./natural_addition.bend as Addition 3 import ./u32_successor.bend as U32Successor 4 import ./word_arithmetic.bend as WordArithmetic 5 import ./bounded_u32_arithmetic.bend as Arithmetic 6 import ./u32_comparison.bend as Comparison 7 import ./nat_to_u32_bounds.bend as Bounds 8 import ./word_encoding.bend as WordEncoding 9 import ./nat_order.bend as Order 10 import ./word_power_of_two.bend as WordPowerOfTwo 11 12 law out_pad: 13 for +n: Nat 14 for +c: Bool 15 for +w: Word(n) 16 {Word.shl.out(1n+n,c,Word.shr.pad(n,w)) == (False{},Word.shl.put(1n+n,c,Word.shr.pad(n,w))) : Bool & Word(1n+n)} 17 def out_pad(n,c,w): 18 match n: 19 case 0n: 20 {==} 21 case 1n+ +p: 22 WCon{+bit,+tail} = w 23 %Equal.sym(Bool & Word(1n+p),Word.shl.out(1n+p,bit,Word.shr.pad(p,tail)),(False{},Word.shl.put(1n+p,bit,Word.shr.pad(p,tail))),out_pad(p, 24 bit,tail)) : {Word.shl.out.con(1n+p,c,_) == (False{},WCon{c,Word.shl.put(1n+p,bit,Word.shr.pad(p,tail))}) : Bool & Word(2n+p)} 25 {==} 26 27 def Goal(+w: Word(32n),+c: Bool) -> Type: 28 {U32.is_lt(U32{w},2147483648) == True{} : Bool} -> {Word.shl.out(32n,c,w) == (False{},Word.shl.put(32n,c,w)) : Bool & Word(32n)} 29 30 def parts(+c: Bool,+parts: WordEncoding.Split<31n,1n>) -> Goal(WordEncoding.join(31n,1n,parts),c): 31 WordEncoding.Parts{+low,+high} = parts 32 bound => 33 %Equal.sym(Word(1n),high,Word.zero(1n),WordEncoding.upper_zero(31n,0n,low,high,bound)) : {Word.shl.out(32n,c,WordEncoding.concat(31n,1n,low, 34 _)) == (False{},Word.shl.put(32n,c,WordEncoding.concat(31n,1n,low,_))) : Bool & Word(32n)} 35 %Equal.sym(Word(32n),WordEncoding.concat(31n,1n,low,Word.zero(1n)),Word.shr.pad(31n,low),U32Successor.concat_pad(31n, 36 low)) : {Word.shl.out(32n,c,_) == (False{},Word.shl.put(32n,c,_)) : Bool & Word(32n)} 37 out_pad(31n,c,low) 38 39 def no_carry(+w: Word(32n),+c: Bool) -> Goal(w,c): 40 %WordEncoding.recover(31n,1n,w) : Goal(_,c) 41 parts(c,WordEncoding.split(31n,1n,w)) 42 43 def put_inc(+n: Nat,+w: Word(n)) -> {Word.shl.put(n,True{},w) == Word.inc(n,Word.shl(n,w)) : Word(n)}: 44 match n: 45 case 0n: 46 {==} 47 case 1n+p: 48 WCon{bit,tail} = w 49 {==} 50 51 def encoded_shift(+w: Word(32n)) -> {U32{Word.shl(32n,w)} == U32.from_nat(Nat.double(Word.to_nat(32n,w))) : U32}: 52 %WordArithmetic.double_word(32n,w) : {U32{_} == U32.from_nat(Nat.double(Word.to_nat(32n,w))) : U32} 53 %Addition.double(Word.to_nat(32n,w)) : {U32{Word.add(32n,w,w)} == U32.from_nat(_) : U32} 54 Arithmetic.native_add(U32{w},U32{w}) 55 56 def encoded_put(+c: Bool,+w: Word(32n)) -> {U32{Word.shl.put(32n,c,w)} == U32.from_nat(Comparison.digit(c,Word.to_nat(32n,w))) : U32}: 57 match c: 58 case False{}: 59 %WordArithmetic.shift_put(32n,w) : {U32{_} == U32.from_nat(Nat.double(Word.to_nat(32n,w))) : U32} 60 encoded_shift(w) 61 case True{}: 62 %Equal.sym(Word(32n),Word.shl.put(32n,True{},w),Word.inc(32n,Word.shl(32n,w)),put_inc(32n, 63 w)) : {U32{_} == U32.inc(U32.from_nat(Nat.double(Word.to_nat(32n,w)))) : U32} 64 %encoded_shift(w) : {U32.inc(U32{Word.shl(32n,w)}) == U32.inc(_) : U32} 65 {==} 66 67 def bounded_put(+c: Bool,+w: Word(32n),+cap: U32,cap_ok: {U32.is_le(cap,2147483648) == True{} : Bool},h: {Nat.is_le(Comparison.digit(c, 68 Word.to_nat(32n,w)),U32.to_nat(cap)) == True{} : Bool}) -> {U32.to_nat(U32{Word.shl.put(32n,c,w)}) == Comparison.digit(c, 69 Word.to_nat(32n,w)) : Nat}: 70 %Equal.sym(U32,U32{Word.shl.put(32n,c,w)},U32.from_nat(Comparison.digit(c,Word.to_nat(32n,w))),encoded_put(c, 71 w)) : {U32.to_nat(_) == Comparison.digit(c,Word.to_nat(32n,w)) : Nat} 72 Bounds.roundtrip(Comparison.digit(c,Word.to_nat(32n,w)),cap,cap_ok,h) 73 74 def put_pad(+n: Nat,+c: Bool,+w: Word(n)) -> {Word.shl.put(1n+n,c,Word.shr.pad(n,w)) == WCon{c,w} : Word(1n+n)}: 75 match n: 76 case 0n: 77 WNil{} = w 78 {==} 79 case 1n+ +p: 80 WCon{+b,+tail} = w 81 %put_pad(p,b,tail) : {WCon{c,Word.shl.put(1n+p,b,Word.shr.pad(p,tail))} == WCon{c,_} : Word(2n+p)} 82 {==} 83 84 def DoubleGoal(+w: Word(32n)) -> Type: 85 {U32.is_lt(U32{w},2147483648) == True{} : Bool} -> {Word.to_nat(32n,Word.shl(32n,w)) == Nat.double(Word.to_nat(32n,w)) : Nat} 86 87 def double_parts(+parts: WordEncoding.Split<31n,1n>) -> DoubleGoal(WordEncoding.join(31n,1n,parts)): 88 WordEncoding.Parts{+low,+high} = parts 89 bound => 90 %Equal.sym(Word(1n),high,Word.zero(1n),WordEncoding.upper_zero(31n,0n,low,high,bound)) : {Word.to_nat(32n,Word.shl(32n, 91 WordEncoding.concat(31n,1n,low,_))) == Nat.double(Word.to_nat(32n,WordEncoding.concat(31n,1n,low,_))) : Nat} 92 %Equal.sym(Word(32n),WordEncoding.concat(31n,1n,low,Word.zero(1n)),Word.shr.pad(31n,low),U32Successor.concat_pad(31n, 93 low)) : {Word.to_nat(32n,Word.shl(32n,_)) == Nat.double(Word.to_nat(32n,_)) : Nat} 94 %Equal.sym(Word(32n),Word.shl(32n,Word.shr.pad(31n,low)),Word.shl.put(32n,False{},Word.shr.pad(31n,low)),WordArithmetic.shift_put(32n, 95 Word.shr.pad(31n,low))) : {Word.to_nat(32n,_) == Nat.double(Word.to_nat(32n,Word.shr.pad(31n,low))) : Nat} 96 %Equal.sym(Word(32n),Word.shl.put(32n,False{},Word.shr.pad(31n,low)),WCon{False{},low},put_pad(31n,False{},low)) : {Word.to_nat(32n, 97 _) == Nat.double(Word.to_nat(32n,Word.shr.pad(31n,low))) : Nat} 98 %U32Successor.pad_nat(31n,low) : {Nat.double(_) == Nat.double(Word.to_nat(32n,Word.shr.pad(31n,low))) : Nat} 99 {==} 100 101 def double_word(+w: Word(32n)) -> DoubleGoal(w): 102 %WordEncoding.recover(31n,1n,w) : DoubleGoal(_) 103 double_parts(WordEncoding.split(31n,1n,w)) 104 105 def double(+x: U32,h: {U32.is_lt(x,2147483648) == True{} : Bool}) -> {U32.to_nat(U32.shl(x)) == Nat.double(U32.to_nat(x)) : Nat}: 106 match x: 107 case U32{w}: 108 double_word(w)(h) 109 110 def power_fits(+depth: Nat,+depth_ok: {Nat.is_le(depth,30n) == True{} : Bool}) -> {U32.is_le(U32.shln(1,depth),2147483648) == True{} : Bool}: 111 WordPowerOfTwo.native_power_bound(depth,Order.transitive(depth,30n,31n,depth_ok,{==}))