proofs/word_arithmetic.bend
stelliferous@0.0.3.0 · 135 lines · 0 definitions
1# Modular arithmetic identities used before applying bounded Nat conversion.
2import Base
3import stelliferous@0.0.3.0/proofs/natural_addition.bend as Addition
4import stelliferous@0.0.3.0/proofs/u32_successor.bend as U32Successor
5
6law carry:
7 for +n: Nat
8 for +a: Word(n)
9 for +b: Word(n)
10 {Word.adc(n,a,b,False{},True{}) == Word.inc(n,Word.add(n,a,b)) : Word(n)}
11def carry(n,a,b):
12 match n:
13 case 0n:
14 {==}
15 case 1n+ +p:
16 match a b:
17 case WCon{False{},at} WCon{False{},bt}:
18 {==}
19 case WCon{False{},+at} WCon{True{},+bt}:
20 %carry(p,at,bt) : {WCon{False{},Word.adc(p,at,bt,False{},True{})} == WCon{False{},_} : Word(1n+p)}
21 {==}
22 case WCon{True{},+at} WCon{False{},+bt}:
23 %carry(p,at,bt) : {WCon{False{},Word.adc(p,at,bt,False{},True{})} == WCon{False{},_} : Word(1n+p)}
24 {==}
25 case WCon{True{},at} WCon{True{},bt}:
26 {==}
27
28law inc_left:
29 for +n: Nat
30 for +a: Word(n)
31 for +b: Word(n)
32 {Word.add(n,Word.inc(n,a),b) == Word.inc(n,Word.add(n,a,b)) : Word(n)}
33def inc_left(n,a,b):
34 match n:
35 case 0n:
36 {==}
37 case 1n+ +p:
38 match a b:
39 case WCon{False{},at} WCon{False{},bt}:
40 {==}
41 case WCon{False{},+at} WCon{True{},+bt}:
42 %carry(p,at,bt) : {WCon{False{},Word.adc(p,at,bt,False{},True{})} == WCon{False{},_} : Word(1n+p)}
43 {==}
44 case WCon{True{},+at} WCon{False{},+bt}:
45 %inc_left(p,at,bt) : {WCon{False{},Word.add(p,Word.inc(p,at),bt)} == WCon{False{},_} : Word(1n+p)}
46 {==}
47 case WCon{True{},+at} WCon{True{},+bt}:
48 %Equal.sym(Word(p),Word.adc(p,at,bt,False{},True{}),Word.inc(p,Word.add(p,at,bt)),carry(p,at,bt)) : {WCon{True{},Word.add(p,Word.inc(p,
49 at),bt)} == WCon{True{},_} : Word(1n+p)}
50 %inc_left(p,at,bt) : {WCon{True{},Word.add(p,Word.inc(p,at),bt)} == WCon{True{},_} : Word(1n+p)}
51 {==}
52
53def encode(a: Nat,+width: Nat) -> Word(width):
54 match a:
55 case 0n:
56 Word.zero(width)
57 case 1n+p:
58 Word.inc(width,encode(p,width))
59
60law encode_add:
61 for +a: Nat
62 for +b: Nat
63 for +width: Nat
64 {Word.add(width,encode(a,width),encode(b,width)) == encode(Nat.add(a,b),width) : Word(width)}
65def encode_add(a,b,width):
66 match a:
67 case 0n:
68 %Equal.sym(Word(width),Word.add(width,Word.zero(width),encode(b,width)),Word.add(width,encode(b,width),Word.zero(width)),
69 Word.add_comm(width,Word.zero(width),encode(b,width))) : {_ == encode(b,width) : Word(width)}
70 U32Successor.adc_zero(width,encode(b,width))
71 case 1n+ +p:
72 %Equal.sym(Word(width),Word.add(width,Word.inc(width,encode(p,width)),encode(b,width)),Word.inc(width,Word.add(width,encode(p,width),
73 encode(b,width))),inc_left(width,encode(p,width),encode(b,width))) : {_ == Word.inc(width,encode(Nat.add(p,b),width)) : Word(width)}
74 %encode_add(p,b,width) : {Word.inc(width,Word.add(width,encode(p,width),encode(b,width))) == Word.inc(width,_) : Word(width)}
75 {==}
76
77law double_carry:
78 for +n: Nat
79 for +w: Word(n)
80 for +c: Bool
81 {Word.adc(n,w,w,False{},c) == Word.shl.put(n,c,w) : Word(n)}
82def double_carry(n,w,c):
83 match n:
84 case 0n:
85 {==}
86 case 1n+ +p:
87 match w c:
88 case WCon{False{},+t} False{}:
89 %double_carry(p,t,False{}) : {WCon{False{},Word.adc(p,t,t,False{},False{})} == WCon{False{},_} : Word(1n+p)}
90 {==}
91 case WCon{False{},+t} True{}:
92 %double_carry(p,t,False{}) : {WCon{True{},Word.adc(p,t,t,False{},False{})} == WCon{True{},_} : Word(1n+p)}
93 {==}
94 case WCon{True{},+t} False{}:
95 %double_carry(p,t,True{}) : {WCon{False{},Word.adc(p,t,t,False{},True{})} == WCon{False{},_} : Word(1n+p)}
96 {==}
97 case WCon{True{},+t} True{}:
98 %double_carry(p,t,True{}) : {WCon{True{},Word.adc(p,t,t,False{},True{})} == WCon{True{},_} : Word(1n+p)}
99 {==}
100
101def shift_put(+n: Nat,+w: Word(n)) -> {Word.shl(n,w) == Word.shl.put(n,False{},w) : Word(n)}:
102 match n:
103 case 0n:
104 {==}
105 case 1n+p:
106 WCon{b,t} = w
107 {==}
108
109def double_word(+n: Nat,+w: Word(n)) -> {Word.add(n,w,w) == Word.shl(n,w) : Word(n)}:
110 %Equal.sym(Word(n),Word.shl(n,w),Word.shl.put(n,False{},w),shift_put(n,w)) : {Word.add(n,w,w) == _ : Word(n)}
111 double_carry(n,w,False{})
112
113def encode_double(+a: Nat,+width: Nat) -> {encode(Nat.double(a),width) == Word.shl(width,encode(a,width)) : Word(width)}:
114 %Addition.double(a) : {encode(_,width) == Word.shl(width,encode(a,width)) : Word(width)}
115 %encode_add(a,a,width) : {_ == Word.shl(width,encode(a,width)) : Word(width)}
116 double_word(width,encode(a,width))
117
118law native_encoding:
119 for +a: Nat
120 {U32.from_nat(a) == U32{encode(a,32n)} : U32}
121def native_encoding(a):
122 match a:
123 case 0n:
124 {==}
125 case 1n+ +p:
126 %native_encoding(p) : {U32.inc(U32.from_nat(p)) == U32.inc(_) : U32}
127 {==}
128
129def native_add(+a: Nat,+b: Nat) -> {U32.add(U32.from_nat(a),U32.from_nat(b)) == U32.from_nat(Nat.add(a,b)) : U32}:
130 %Equal.sym(U32,U32.from_nat(Nat.add(a,b)),U32{encode(Nat.add(a,b),32n)},native_encoding(Nat.add(a,b))) : {U32.add(U32.from_nat(a),
131 U32.from_nat(b)) == _ : U32}
132 %Equal.sym(U32,U32.from_nat(a),U32{encode(a,32n)},native_encoding(a)) : {U32.add(_,U32.from_nat(b)) == U32{encode(Nat.add(a,b),32n)} : U32}
133 %Equal.sym(U32,U32.from_nat(b),U32{encode(b,32n)},native_encoding(b)) : {U32.add(U32{encode(a,32n)},_) == U32{encode(Nat.add(a,b),32n)} : U32}
134 %encode_add(a,b,32n) : {U32{Word.add(32n,encode(a,32n),encode(b,32n))} == U32{_} : U32}
135 {==}