1	import Base
2	import ../shape/core.bend as Shape
3	import ./word_conversion.bend as Conversion
4	
5	law word_increment_exact:
6	  for +width: Nat
7	  for +word: Word(width)
8	  for zero: {Conversion.word_has_zero(width, word) == True{} : Bool}
9	  {Word.to_nat(width, Word.inc(width, word)) == 1n+Word.to_nat(width, word) : Nat}
10	
11	law increment_below_exact:
12	  for +word: U32
13	  for +limit: U32
14	  for below: {U32.is_lt(word, limit) == True{} : Bool}
15	  {U32.to_nat(U32.inc(word)) == 1n+U32.to_nat(word) : Nat}
16	
17	law natural_word_exact:
18	  for +number: Nat
19	  for +limit: U32
20	  for +within: {Nat.is_le(number, U32.to_nat(limit)) == True{} : Bool}
21	  {U32.to_nat(U32.from_nat(number)) == number : Nat}
22	
23	law word_natural_exact:
24	  for +word: U32
25	  {U32.from_nat(U32.to_nat(word)) == word : U32}
26	
27	law naturals_words_fitting:
28	  for +dims: List<&2, U32>
29	  for +values: List<&2, Nat>
30	  for +fit: {True{} == Shape.fit(Shape.naturals(dims), values) : Bool}
31	  {Shape.naturals(Shape.words(values)) == values : List<&2, Nat>}
32	
33	law word_increment_le:
34	  for +width: Nat
35	  for +word: Word(width)
36	  {Nat.is_le(Word.to_nat(width, Word.inc(width, word)), 1n+Word.to_nat(width, word)) == True{} : Bool}
37	
38	law increment_le:
39	  for +word: U32
40	  {Nat.is_le(U32.to_nat(U32.inc(word)), 1n+U32.to_nat(word)) == True{} : Bool}
41	
42	law natural_word_le:
43	  for +number: Nat
44	  {Nat.is_le(U32.to_nat(U32.from_nat(number)), number) == True{} : Bool}
45	
46	law capacity_word_nat:
47	  {U32.to_nat(1048576) == 1048576n : Nat}
48	
49	law capacity_natural_word_exact:
50	  for +number: Nat
51	  for within: Shape.LE(number, 1048576n)
52	  {U32.to_nat(U32.from_nat(number)) == number : Nat}
53	
54	law shape_count_exact:
55	  for +shape: Shape.Shape
56	  {U32.to_nat(Shape.count(shape)) == Shape.elements(shape) : Nat}
57	
58	law shape_count_within:
59	  for +shape: Shape.Shape
60	  {U32.is_le(Shape.count(shape), 1048576) == True{} : Bool}