1	import Base
2	import ./gb.bend as GB
3	import ./blamka.bend as BL
4	import ./hash.bend as HS
5	import ./memory.bend as MEM
6	import ./index.bend as IX
7	import ./fill.bend as FL
8	import ./run.bend as RN
9	import ./top.bend as TOP
10	import ./phc.bend as PP
11	import ./password.bend as PWP
12	import ../../../spec/lib/common.bend as SC
13	import ../../lib/u32.bend as U
14	import ../../lib/logic.bend as L
15	import ./laws.bend as Laws
16	
17	# Gate for the Argon2id package: `bend proofs/crypto/argon2/proof.bend`
18	# prints ALL PROOFS CHECK when every law of laws.bend holds.
19	def Laws.gb_correct(a, b, c, d): GB.gb_correct(a, b, c, d)
20	def Laws.p_correct(v): BL.p_correct(v)
21	def Laws.compress_correct(x, y): BL.compress_correct(x, y)
22	def Laws.compress_xor_correct(x, y, old): BL.compress_xor_correct(x, y, old)
23	def Laws.hash_correct(nn, bs): HS.hash_eq(nn, bs)
24	def Laws.hprime_correct(tl, x): HS.hprime_eq(tl, x)
25	def Laws.h0_correct(p, tl, m, t, pw, salt, key, ad): HS.h0_eq(p, tl, m, t, pw, salt, key, ad)
26	def Laws.rel_correct(w, j1, k, hk, hw): IX.rel_eq(w, j1, k, hk, L.subst(Nat, z => {Nat.is_lt(w, z) == True{} : Bool}, Nat.pow(2n, k), SC.pow2(k), Equal.sym(Nat, SC.pow2(k), Nat.pow(2n, k), U.pow2_pow(k)), hw))
27	def Laws.addresses_correct(r, l, s, mm, t, ctr): IX.addresses_eq(r, l, s, mm, t, ctr)
28	def Laws.argon2id_correct(pw, salt, key, ad, t, m, p, tl, hf): TOP.argon2id_correct(pw, salt, key, ad, t, m, p, tl, hf)
29	def Laws.parse_format(m, t, p, salt, hash, hs, hh): PP.parse_format(m, t, p, salt, hash, hs, hh)
30	def Laws.verify_hash(pw, salt, params, hs): PWP.verify_hash(pw, salt, params, hs)
31	def Laws.rehash_hash(pw, salt, params, hs, hl): PWP.rehash_hash(pw, salt, params, hs, hl)
32	def Laws.tag_length(tl, x): PWP.hprime_len(tl, x)
33	def Laws.tag_bytes(tl, x): PWP.hprime_ok(tl, x)