1	import Base
2	import ../../../spec/lib/common.bend as C
3	import ../../../spec/math/w64.bend as SW
4	import ../../../src/math/w64.bend as X
5	import ../../../src/math/u64.bend as WU
6	import ../../lib/u32.bend as U
7	import ../../lib/logic.bend as L
8	import ../../math/typed/w64mul.bend as W64M
9	import ./words.bend as LW
10	import ../../math/typed/width.bend as WW
11	import ../../../src/crypto/blake/blake2b/types.bend as T
12	import ../../../src/crypto/argon2/types.bend as A
13	import ../../../src/crypto/argon2/blamka.bend as G
14	import ../../../src/crypto/argon2/argon2.bend as I
15	import ../../../spec/crypto/blake/blake2b.bend as B
16	import ../../../spec/crypto/argon2/blamka.bend as SG
17	import ../../../spec/crypto/argon2/argon2.bend as SA
18	import ./gb.bend as GB
19	import ./blamka.bend as BL
20	
21	# The reference-index computation of the implementation (U32 products,
22	# src/math/w64.bend's mul32) equals the specification's (Nat arithmetic,
23	# RFC 9106 section 3.4.1.2), and so do the address blocks of the
24	# data-independent segments.
25	
26	# ---------------------------------------------------------------- lanes of a block
27	
28	def row_at_eq(+b: A.Block, +i: Nat) -> {I.row_at(b, i) == SG.row(b, i) : T.State}:
29	  match b i:
30	    case A.B{r0, r1, r2, r3, r4, r5, r6, r7} 0n:
31	      {==}
32	    case A.B{r0, r1, r2, r3, r4, r5, r6, r7} 1n:
33	      {==}
34	    case A.B{r0, r1, r2, r3, r4, r5, r6, r7} 2n:
35	      {==}
36	    case A.B{r0, r1, r2, r3, r4, r5, r6, r7} 3n:
37	      {==}
38	    case A.B{r0, r1, r2, r3, r4, r5, r6, r7} 4n:
39	      {==}
40	    case A.B{r0, r1, r2, r3, r4, r5, r6, r7} 5n:
41	      {==}
42	    case A.B{r0, r1, r2, r3, r4, r5, r6, r7} 6n:
43	      {==}
44	    case A.B{r0, r1, r2, r3, r4, r5, r6, r7} 7n+z:
45	      {==}
46	
47	def at_eq(+v: T.State, +j: Nat) -> {I.at(v, j) == B.at(v, j) : T.Lane}:
48	  match v j:
49	    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 0n:
50	      {==}
51	    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 1n:
52	      {==}
53	    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 2n:
54	      {==}
55	    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 3n:
56	      {==}
57	    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 4n:
58	      {==}
59	    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 5n:
60	      {==}
61	    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 6n:
62	      {==}
63	    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 7n:
64	      {==}
65	    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 8n:
66	      {==}
67	    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 9n:
68	      {==}
69	    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 10n:
70	      {==}
71	    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 11n:
72	      {==}
73	    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 12n:
74	      {==}
75	    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 13n:
76	      {==}
77	    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 14n:
78	      {==}
79	    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 15n:
80	      {==}
81	    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 16n+z:
82	      {==}
83	
84	def lane_eq(+b: A.Block, +n: Nat) -> {I.lane(b, n) == SG.lane(b, n) : T.Lane}:
85	  Equal.trans(T.Lane, I.at(I.row_at(b, Nat.div(n, 16n)), Nat.mod(n, 16n)), I.at(SG.row(b, Nat.div(n, 16n)), Nat.mod(n, 16n)), SG.lane(b, n),
86	    Equal.cong(T.State, T.Lane, z => I.at(z, Nat.mod(n, 16n)), I.row_at(b, Nat.div(n, 16n)), SG.row(b, Nat.div(n, 16n)), row_at_eq(b, Nat.div(n, 16n))),
87	    at_eq(SG.row(b, Nat.div(n, 16n)), Nat.mod(n, 16n)))
88	
89	def pick_eq(+indep: Bool, +addr: A.Block, +idx: Nat, +prev: A.Block) -> {I.pick(indep, addr, idx, prev) == SA.pick(indep, addr, idx, prev) : T.Lane}:
90	  match indep:
91	    case True{}:
92	      lane_eq(addr, Nat.mod(idx, 128n))
93	    case False{}:
94	      lane_eq(prev, 0n)
95	
96	def hi_eq(+x: T.Lane) -> {I.hi(x) == SA.hi(x) : U32}:
97	  match x:
98	    case T.W{l, h}:
99	      {==}
100	
101	def lo_eq(+x: T.Lane) -> {G.lo(x) == SA.lo(x) : U32}:
102	  match x:
103	    case T.W{l, h}:
104	      {==}
105	
106	# ---------------------------------------------------------------- the reference area
107	
108	def ref_lane_eq(+forced: Bool, +l: Nat, +j2: U32, +p: Nat) -> {I.ref_lane(forced, l, j2, p) == SA.ref_lane(forced, l, j2, p) : Nat}:
109	  match forced:
110	    case True{}:
111	      {==}
112	    case False{}:
113	      {==}
114	
115	def area_base_eq(+r0: Bool, +s: Nat, +sl: Nat, +q: Nat) -> {I.area_base(r0, s, sl, q) == SA.area_base(r0, s, sl, q) : Nat}:
116	  match r0:
117	    case True{}:
118	      {==}
119	    case False{}:
120	      {==}
121	
122	def area_other_eq(+base: Nat, +zero: Bool) -> {I.area_other(base, zero) == SA.area_other(base, zero) : Nat}:
123	  match zero:
124	    case True{}:
125	      {==}
126	    case False{}:
127	      {==}
128	
129	def area_eq(+base: Nat, +idx: Nat, +same: Bool) -> {I.area(base, idx, same) == SA.area(base, idx, same) : Nat}:
130	  match same:
131	    case True{}:
132	      {==}
133	    case False{}:
134	      area_other_eq(base, Nat.is_eq(idx, 0n))
135	
136	def start_last_eq(+s: Nat, +sl: Nat, +last: Bool) -> {I.start_last(s, sl, last) == SA.start_last(s, sl, last) : Nat}:
137	  match last:
138	    case True{}:
139	      {==}
140	    case False{}:
141	      {==}
142	
143	def start_eq(+r0: Bool, +s: Nat, +sl: Nat) -> {I.start(r0, s, sl) == SA.start(r0, s, sl) : Nat}:
144	  match r0:
145	    case True{}:
146	      {==}
147	    case False{}:
148	      start_last_eq(s, sl, Nat.is_eq(s, 3n))
149	
150	def prev_index_eq(+l: Nat, +q: Nat, +j: Nat, +first: Bool) -> {I.prev_index(l, q, j, first) == SA.prev_index(l, q, j, first) : Nat}:
151	  match first:
152	    case True{}:
153	      {==}
154	    case False{}:
155	      {==}
156	
157	def start_index_eq(+first: Bool) -> {I.start_index(first) == SA.start_index(first) : Nat}:
158	  match first:
159	    case True{}:
160	      {==}
161	    case False{}:
162	      {==}
163	
164	def fits_value(+x: WU.U64) -> {C.fits(64n, SW.value(x)) == True{} : Bool}:
165	  match x:
166	    case WU.U64{+l, +h}:
167	      WW.limbs_fit(32n, 32n, LW.v(l), LW.v(h), LW.vb(l), LW.vb(h))
168	
169	# ---------------------------------------------------------------- x = J1^2 / 2^32, y = |W| x / 2^32
170	
171	# The high word of mul32(a, b) is a * b div 2^32.
172	def hi_mul(+a: U32, +b: U32) -> {U32.to_nat(X.hi(X.mul32(a, b))) == C.high(32n, Nat.mul(U32.to_nat(a), U32.to_nat(b))) : Nat}:
173	  +n = Nat.mul(U32.to_nat(a), U32.to_nat(b))
174	  +f64 = L.subst(Nat, z => {C.fits(64n, z) == True{} : Bool}, SW.value(X.mul32(a, b)), n, W64M.mul32_value(a, b), fits_value(X.mul32(a, b)))
175	  +f32 = LW.fits_high(32n, 32n, n, f64)
176	  %Equal.sym(WU.U64, X.mul32(a, b), SW.of_nat(n), GB.mul32_of(a, b)) : {U32.to_nat(X.hi(_)) == C.high(32n, n) : Nat}
177	  LW.vo(C.high(32n, n), f32)
178	
179	# rel: |W| - 1 - (|W| * (J1^2 / 2^32)) / 2^32, for |W| < 2^k with k <= 32.
180	def rel_eq(+w: Nat, +j1: U32, +k: Nat, +hk: {Nat.is_le(k, 32n) == True{} : Bool}, +hw: {Nat.is_lt(w, C.pow2(k)) == True{} : Bool}) -> {I.rel(w, j1) == SA.rel(w, j1) : Nat}:
181	  +xi = X.hi(X.mul32(j1, j1))
182	  +xs = C.high(32n, Nat.mul(U32.to_nat(j1), U32.to_nat(j1)))
183	  +ew = U.to_nat_from_nat(w, k, hk, hw)
184	  +e1 = hi_mul(U32.from_nat(w), xi)
185	  +e2 = Equal.trans(Nat, C.high(32n, Nat.mul(U32.to_nat(U32.from_nat(w)), U32.to_nat(xi))), C.high(32n, Nat.mul(w, U32.to_nat(xi))), C.high(32n, Nat.mul(w, xs)),
186	    Equal.cong(Nat, Nat, z => C.high(32n, Nat.mul(z, U32.to_nat(xi))), U32.to_nat(U32.from_nat(w)), w, ew),
187	    Equal.cong(Nat, Nat, z => C.high(32n, Nat.mul(w, z)), U32.to_nat(xi), xs, hi_mul(j1, j1)))
188	  Equal.cong(Nat, Nat, z => Nat.sub(Nat.sub(w, 1n), z), U32.to_nat(X.hi(X.mul32(U32.from_nat(w), xi))), C.high(32n, Nat.mul(w, xs)), Equal.trans(Nat, U32.to_nat(X.hi(X.mul32(U32.from_nat(w), xi))), C.high(32n, Nat.mul(U32.to_nat(U32.from_nat(w)), U32.to_nat(xi))), C.high(32n, Nat.mul(w, xs)), e1, e2))
189	
190	# ---------------------------------------------------------------- address blocks
191	
192	def input_eq(+r: Nat, +l: Nat, +s: Nat, +mm: Nat, +t: Nat, +ctr: Nat) -> {I.input_block(r, l, s, mm, t, ctr) == SA.input_block(r, l, s, mm, t, ctr) : A.Block}:
193	  match r:
194	    case 0n:
195	      {==}
196	    case 1n+x:
197	      {==}
198	
199	def addresses_eq(+r: Nat, +l: Nat, +s: Nat, +mm: Nat, +t: Nat, +ctr: Nat) -> {I.addresses(r, l, s, mm, t, ctr) == SA.addresses(r, l, s, mm, t, ctr) : A.Block}:
200	  +z = SA.input_block(r, l, s, mm, t, ctr)
201	  Equal.trans(A.Block, G.compress(G.zero(), G.compress(G.zero(), I.input_block(r, l, s, mm, t, ctr))), G.compress(G.zero(), G.compress(G.zero(), z)), SG.G(SG.zero(), SG.G(SG.zero(), z)),
202	    Equal.cong(A.Block, A.Block, x => G.compress(G.zero(), G.compress(G.zero(), x)), I.input_block(r, l, s, mm, t, ctr), z, input_eq(r, l, s, mm, t, ctr)),
203	    Equal.trans(A.Block, G.compress(G.zero(), G.compress(G.zero(), z)), G.compress(G.zero(), SG.G(SG.zero(), z)), SG.G(SG.zero(), SG.G(SG.zero(), z)),
204	      Equal.cong(A.Block, A.Block, x => G.compress(G.zero(), x), G.compress(G.zero(), z), SG.G(SG.zero(), z), BL.compress_correct(G.zero(), z)),
205	      BL.compress_correct(G.zero(), SG.G(SG.zero(), z))))
206	
207	def regen_eq(+need: Bool, +addr: A.Block, +r: Nat, +l: Nat, +s: Nat, +mm: Nat, +t: Nat, +idx: Nat) -> {I.regen(need, addr, r, l, s, mm, t, idx) == SA.regen(need, addr, r, l, s, mm, t, idx) : A.Block}:
208	  match need:
209	    case True{}:
210	      addresses_eq(r, l, s, mm, t, Nat.add(Nat.div(idx, 128n), 1n))
211	    case False{}:
212	      {==}