1	import Base
2	import lawful-words@0.1.0.0/proof_nat.bend as WN
3	import lawful-words@0.1.0.0/proof_u32.bend as WU
4	
5	# The U32 and Nat facts the index proofs need, from lawful-words (BendHub), where
6	# they are laws (proof_u32.bend and proof_nat.bend restate them with every
7	# variable reusable). w_shln_fits is to_nat_shln_fits with 2^32 written as
8	# Nat.pow(2n, 32n): the law's D.two32() cannot be checked (lawful-words
9	# notes/proof.md).
10	
11	law w_shr:
12	  for +a: U32
13	  {U32.to_nat(U32.shr(a)) == Nat.div(U32.to_nat(a), 2n) : Nat}
14	
15	def w_shr(a):
16	  WU.to_nat_shr(a)
17	
18	law w_lt:
19	  for +a: U32
20	  for +b: U32
21	  {U32.is_lt(a, b) == Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) : Bool}
22	
23	def w_lt(a, b):
24	  WU.is_lt_to_nat(a, b)
25	
26	law w_le:
27	  for +a: U32
28	  for +b: U32
29	  {U32.is_le(a, b) == Nat.is_le(U32.to_nat(a), U32.to_nat(b)) : Bool}
30	
31	def w_le(a, b):
32	  WU.is_le_to_nat(a, b)
33	
34	law w_sub_le:
35	  for +a: U32
36	  for +b: U32
37	  for +h: {U32.is_le(b, a) == True{} : Bool}
38	  {U32.to_nat(U32.sub(a, b)) == Nat.sub(U32.to_nat(a), U32.to_nat(b)) : Nat}
39	
40	def w_sub_le(a, b, h):
41	  WU.to_nat_sub_le(a, b, h)
42	
43	law w_and_mask:
44	  for +a: U32
45	  for +m: U32
46	  for +k: Nat
47	  for +h: {U32.to_nat(m) == Nat.sub(Nat.pow(2n, k), 1n) : Nat}
48	  {U32.to_nat(U32.and(a, m)) == Nat.mod(U32.to_nat(a), Nat.pow(2n, k)) : Nat}
49	
50	def w_and_mask(a, m, k, h):
51	  WU.to_nat_and_mask(a, m, k, h)
52	
53	law w_shln_fits:
54	  for +a: U32
55	  for +k: Nat
56	  for +h: {Nat.is_lt(Nat.mul(U32.to_nat(a), Nat.pow(2n, k)), Nat.pow(2n, 32n)) == True{} : Bool}
57	  {U32.to_nat(U32.shln(a, k)) == Nat.mul(U32.to_nat(a), Nat.pow(2n, k)) : Nat}
58	
59	def w_shln_fits(a, k, h):
60	  WU.to_nat_shln_fits_p(a, k, h)
61	
62	law n_mod_lt:
63	  for +a: Nat
64	  for +b: Nat
65	  for +h: {Nat.is_lt(0n, b) == True{} : Bool}
66	  {Nat.is_lt(Nat.mod(a, b), b) == True{} : Bool}
67	
68	def n_mod_lt(a, b, h):
69	  WN.mod_lt(a, b, h)
70	
71	law n_mod_small:
72	  for +a: Nat
73	  for +b: Nat
74	  for +h: {Nat.is_lt(a, b) == True{} : Bool}
75	  {Nat.mod(a, b) == a : Nat}
76	
77	def n_mod_small(a, b, h):
78	  WN.mod_small(a, b, h)
79	
80	law n_div_mul_add:
81	  for +q: Nat
82	  for +b: Nat
83	  for +r: Nat
84	  for +h: {Nat.is_lt(r, b) == True{} : Bool}
85	  {Nat.div(Nat.add(Nat.mul(q, b), r), b) == q : Nat}
86	
87	def n_div_mul_add(q, b, r, h):
88	  WN.div_mul_add(q, b, r, h)
89	
90	law n_mul_comm:
91	  for +a: Nat
92	  for +b: Nat
93	  {Nat.mul(a, b) == Nat.mul(b, a) : Nat}
94	
95	def n_mul_comm(a, b):
96	  WN.mul_comm(a, b)