proofs/u32_shift.bend
stelliferous@0.0.3.0 · 111 lines · 0 definitions
1import Base
2import stelliferous@0.0.3.0/proofs/natural_addition.bend as Addition
3import stelliferous@0.0.3.0/proofs/u32_successor.bend as U32Successor
4import stelliferous@0.0.3.0/proofs/word_arithmetic.bend as WordArithmetic
5import stelliferous@0.0.3.0/proofs/bounded_u32_arithmetic.bend as Arithmetic
6import stelliferous@0.0.3.0/proofs/u32_comparison.bend as Comparison
7import stelliferous@0.0.3.0/proofs/nat_to_u32_bounds.bend as Bounds
8import stelliferous@0.0.3.0/proofs/word_encoding.bend as WordEncoding
9import stelliferous@0.0.3.0/proofs/nat_order.bend as Order
10import stelliferous@0.0.3.0/proofs/word_power_of_two.bend as WordPowerOfTwo
11
12law 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)}
17def 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
27def 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
30def 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
39def 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
43def 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
51def 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
56def 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
67def 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
74def 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
84def 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
87def 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
101def double_word(+w: Word(32n)) -> DoubleGoal(w):
102 %WordEncoding.recover(31n,1n,w) : DoubleGoal(_)
103 double_parts(WordEncoding.split(31n,1n,w))
104
105def 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
110def 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,{==}))