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