src/tensor/word_conversion_LAWS.bend
bendtorch-core@0.1.0.0 · 60 lines · 12 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
3import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
4
5law 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
11law 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
17law 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
23law word_natural_exact:
24 for +word: U32
25 {U32.from_nat(U32.to_nat(word)) == word : U32}
26
27law 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
33law 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
38law increment_le:
39 for +word: U32
40 {Nat.is_le(U32.to_nat(U32.inc(word)), 1n+U32.to_nat(word)) == True{} : Bool}
41
42law natural_word_le:
43 for +number: Nat
44 {Nat.is_le(U32.to_nat(U32.from_nat(number)), number) == True{} : Bool}
45
46law capacity_word_nat:
47 {U32.to_nat(1048576) == 1048576n : Nat}
48
49law 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
54law shape_count_exact:
55 for +shape: Shape.Shape
56 {U32.to_nat(Shape.count(shape)) == Shape.elements(shape) : Nat}
57
58law shape_count_within:
59 for +shape: Shape.Shape
60 {U32.is_le(Shape.count(shape), 1048576) == True{} : Bool}