PROOF.bend

bend-osdev-word64@0.1.0.0 · 47 lines · 0 definitions

1import Base
2import bend-osdev-word64@0.1.0.0/word64.bend as W
3import bend-osdev-word64@0.1.0.0/LAWS.bend as Laws
4
5def Laws.add_wraps():
6  {==}
7
8def Laws.sub_wraps():
9  {==}
10
11def Laws.hi_of_parts():
12  {==}
13
14def Laws.lo_of_parts():
15  {==}
16
17def Laws.shl_crosses_halves():
18  {==}
19
20def Laws.shr_crosses_halves():
21  {==}
22
23def Laws.mul_of_max_halves():
24  {==}
25
26def Laws.show_max():
27  {==}
28
29def Laws.show_hex_parts():
30  {==}
31
32def Laws.show_hex_zero():
33  {==}
34
35def Laws.lo_from_u32(a):
36  {==}
37
38def Laws.hi_from_parts(h, l):
39  {==}
40
41def Laws.lo_from_parts(h, l):
42  {==}
43
44def Laws.parts_of(v):
45  match v:
46    case W.W64{h, l}:
47      {==}