1	import Base
2	import ../../../spec/lib/common.bend as C
3	import ../../lib/logic.bend as L
4	import ../../lib/u32.bend as U
5	import ../../math/typed/u32.bend as U32P
6	import ../../math/typed/width.bend as WW
7	
8	# The U32 value model the Argon2 proofs use (from proofs/math/typed/u32laws.bend
9	# and w64sh.bend, restated here so the package does not import their
10	# neighbours: Bend 2.0.34 checks every imported definition, and one of them
11	# expands 2^13 to a unary Nat, too deep for its stack next to this package).
12	# Width 32 stays symbolic inside the proofs.
13	
14	def v(+x: U32) -> Nat:
15	  U32.to_nat(x)
16	
17	def vb_k(+k: Nat, +hk: {k == 32n : Nat}, +x: U32) -> {C.fits(k, v(x)) == True{} : Bool}:
18	  %Equal.sym(Bool, C.fits(k, v(x)), Nat.is_lt(v(x), C.pow2(k)), WW.fits_lt(k, v(x))) : {_ == True{} : Bool}
19	  U32P.val_lt(1n, {==}, k, hk, x)
20	
21	# every U32 value fits 32 bits
22	def vb(+x: U32) -> {C.fits(32n, v(x)) == True{} : Bool}:
23	  vb_k(32n, {==}, x)
24	
25	def lt_k(+k: Nat, +n: Nat, +h: {C.fits(k, n) == True{} : Bool}) -> {Nat.is_lt(n, C.pow2(k)) == True{} : Bool}:
26	  %WW.fits_lt(k, n) : {_ == True{} : Bool}
27	  h
28	
29	def vo_k(+k: Nat, +hk: {k == 32n : Nat}, +n: Nat, +h: {C.fits(k, n) == True{} : Bool}) -> {v(U32.from_nat(n)) == n : Nat}:
30	  U.to_nat_from_nat(n, k, U32P.le_k(k, hk), lt_k(k, n, h))
31	
32	# a value that fits is the value of its U32
33	def vo(+n: Nat, +h: {C.fits(32n, n) == True{} : Bool}) -> {v(U32.from_nat(n)) == n : Nat}:
34	  vo_k(32n, {==}, n, h)
35	
36	def rt(+x: U32) -> {U32.from_nat(v(x)) == x : U32}:
37	  U32P.round_trip(x)
38	
39	# the high part of a value of t + s bits has s bits
40	def fits_high(+t: Nat, +s: Nat, +x: Nat, +h: {C.fits(Nat.add(t, s), x) == True{} : Bool}) -> {C.fits(s, C.high(t, x)) == True{} : Bool}:
41	  L.subst(Nat, z => {Nat.is_eq(z, 0n) == True{} : Bool}, C.high(Nat.add(t, s), x), C.high(s, C.high(t, x)), WW.high_comp(s, t, x), h)