proof_fast_word.bend

lawful-bytes@0.1.1.0 · 249 lines · 15 definitions

1import Base
2import lawful-words@0.1.0.0/defs.bend as W
3import lawful-bytes@0.1.1.0/defs.bend as D
4import lawful-bytes@0.1.1.0/fast.bend as FA
5import lawful-bytes@0.1.1.0/proof_core.bend as C
6import lawful-words@0.1.0.0/proof_nat.bend as N
7import lawful-words@0.1.0.0/proof_u32.bend as U
8import lawful-words@0.1.0.0/proof_zb.bend as Z
9import lawful-arrays@0.1.0.0/proof_base.bend as AB
10import lawful-bytes@0.1.1.0/proof_fast_w1.bend as W1
11import lawful-bytes@0.1.1.0/proof_fast_w2.bend as W2
12
13# Word facts behind fast.bend's find: the zero-byte flags (FA.zb) and the
14# place of the lowest flag (FA.bidx), the broadcast byte (FA.rep) and the mask
15# of the bytes below a start (FA.low).
16
17# The place of the first zero byte of v (4 when there is none).
18def P0(+v: U32) -> Nat:
19  D.run_len(C.L4(v), 0)
20
21# The k = 1 test of the or of two flag words.
22law tko1:
23  for +v1: U32
24  for +v2: U32
25  {U32.is_zero(U32.and(U32.or(W.zb(v1), W.zb(v2)), 128)) == Bool.and(Bool.and(U32.is_ne(W.byte(v1, 0n), 0), True{}), Bool.and(U32.is_ne(W.byte(v2, 0n), 0), True{})) : Bool}
26
27def tko1(v1, v2):
28  %W1.tk1(v1) :
29    {U32.is_zero(U32.and(U32.or(W.zb(v1), W.zb(v2)), 128)) == Bool.and(_, Bool.and(U32.is_ne(W.byte(v2, 0n), 0), True{})) : Bool}
30  %W1.tk1(v2) :
31    {U32.is_zero(U32.and(U32.or(W.zb(v1), W.zb(v2)), 128)) == Bool.and(U32.is_zero(U32.and(W.zb(v1), 128)), _) : Bool}
32  W2.uorm(W.zb(v1), W.zb(v2), 128)
33
34# The k = 2 test of the or of two flag words.
35law tko2:
36  for +v1: U32
37  for +v2: U32
38  {U32.is_zero(U32.and(U32.or(W.zb(v1), W.zb(v2)), 32896)) == Bool.and(Bool.and(U32.is_ne(W.byte(v1, 0n), 0), Bool.and(U32.is_ne(W.byte(v1, 1n), 0), True{})), Bool.and(U32.is_ne(W.byte(v2, 0n), 0), Bool.and(U32.is_ne(W.byte(v2, 1n), 0), True{}))) : Bool}
39
40def tko2(v1, v2):
41  %W1.tk2(v1) :
42    {U32.is_zero(U32.and(U32.or(W.zb(v1), W.zb(v2)), 32896)) == Bool.and(_, Bool.and(U32.is_ne(W.byte(v2, 0n), 0), Bool.and(U32.is_ne(W.byte(v2, 1n), 0), True{}))) : Bool}
43  %W1.tk2(v2) :
44    {U32.is_zero(U32.and(U32.or(W.zb(v1), W.zb(v2)), 32896)) == Bool.and(U32.is_zero(U32.and(W.zb(v1), 32896)), _) : Bool}
45  W2.uorm(W.zb(v1), W.zb(v2), 32896)
46
47# The k = 3 test of the or of two flag words.
48law tko3:
49  for +v1: U32
50  for +v2: U32
51  {U32.is_zero(U32.and(U32.or(W.zb(v1), W.zb(v2)), 8421504)) == Bool.and(Bool.and(U32.is_ne(W.byte(v1, 0n), 0), Bool.and(U32.is_ne(W.byte(v1, 1n), 0), Bool.and(U32.is_ne(W.byte(v1, 2n), 0), True{}))), Bool.and(U32.is_ne(W.byte(v2, 0n), 0), Bool.and(U32.is_ne(W.byte(v2, 1n), 0), Bool.and(U32.is_ne(W.byte(v2, 2n), 0), True{})))) : Bool}
52
53def tko3(v1, v2):
54  %W1.tk3(v1) :
55    {U32.is_zero(U32.and(U32.or(W.zb(v1), W.zb(v2)), 8421504)) == Bool.and(_, Bool.and(U32.is_ne(W.byte(v2, 0n), 0), Bool.and(U32.is_ne(W.byte(v2, 1n), 0), Bool.and(U32.is_ne(W.byte(v2, 2n), 0), True{})))) : Bool}
56  %W1.tk3(v2) :
57    {U32.is_zero(U32.and(U32.or(W.zb(v1), W.zb(v2)), 8421504)) == Bool.and(U32.is_zero(U32.and(W.zb(v1), 8421504)), _) : Bool}
58  W2.uorm(W.zb(v1), W.zb(v2), 8421504)
59
60# The zero-byte flags are all clear exactly when no byte is zero.
61law zb_none:
62  for +v: U32
63  {U32.is_zero(FA.zb(v)) == Nat.is_eq(P0(v), 4n) : Bool}
64
65def zb_none(v):
66  %Equal.sym(U32, FA.zb(v), W.zb(v), W1.zb_eq(v)) : {U32.is_zero(_) == Nat.is_eq(P0(v), 4n) : Bool}
67  Equal.trans(Bool, U32.is_zero(W.zb(v)), Bool.and(U32.is_ne(W.byte(v, 0n), 0), Bool.and(U32.is_ne(W.byte(v, 1n), 0), Bool.and(U32.is_ne(W.byte(v, 2n), 0), U32.is_ne(W.byte(v, 3n), 0)))),
68    Nat.is_eq(P0(v), 4n), Z.zb_zero(v), W2.bt_none(U32.is_eq(W.byte(v, 0n), 0), U32.is_eq(W.byte(v, 1n), 0), U32.is_eq(W.byte(v, 2n), 0), U32.is_eq(W.byte(v, 3n), 0)))
69
70# bidx finds the first zero byte.
71law zb_bidx:
72  for +v: U32
73  for +h: {Nat.is_lt(P0(v), 4n) == True{} : Bool}
74  {U32.to_nat(FA.bidx(FA.zb(v))) == P0(v) : Nat}
75
76def zb_bidx(v, h):
77  %Equal.sym(U32, FA.zb(v), W.zb(v), W1.zb_eq(v)) : {U32.to_nat(FA.bidx(_)) == P0(v) : Nat}
78  %Equal.sym(Bool, U32.is_zero(U32.and(W.zb(v), 128)), Bool.and(U32.is_ne(W.byte(v, 0n), 0), True{}), W1.tk1(v)) : {U32.to_nat(U32.add(U32.add(FA.b2u(_), FA.b2u(U32.is_zero(U32.and(W.zb(v), 32896)))), FA.b2u(U32.is_zero(U32.and(W.zb(v), 8421504))))) == P0(v) : Nat}
79  %Equal.sym(Bool, U32.is_zero(U32.and(W.zb(v), 32896)), Bool.and(U32.is_ne(W.byte(v, 0n), 0), Bool.and(U32.is_ne(W.byte(v, 1n), 0), True{})), W1.tk2(v)) : {U32.to_nat(U32.add(U32.add(FA.b2u(Bool.and(U32.is_ne(W.byte(v, 0n), 0), True{})), FA.b2u(_)), FA.b2u(U32.is_zero(U32.and(W.zb(v), 8421504))))) == P0(v) : Nat}
80  %Equal.sym(Bool, U32.is_zero(U32.and(W.zb(v), 8421504)), Bool.and(U32.is_ne(W.byte(v, 0n), 0), Bool.and(U32.is_ne(W.byte(v, 1n), 0), Bool.and(U32.is_ne(W.byte(v, 2n), 0), True{}))), W1.tk3(v)) : {U32.to_nat(U32.add(U32.add(FA.b2u(Bool.and(U32.is_ne(W.byte(v, 0n), 0), True{})), FA.b2u(Bool.and(U32.is_ne(W.byte(v, 0n), 0), Bool.and(U32.is_ne(W.byte(v, 1n), 0), True{})))), FA.b2u(_))) == P0(v) : Nat}
81  W2.bt_bidx(U32.is_eq(W.byte(v, 0n), 0), U32.is_eq(W.byte(v, 1n), 0), U32.is_eq(W.byte(v, 2n), 0), U32.is_eq(W.byte(v, 3n), 0), h)
82
83# The same for the flags of two words or-ed (find2).
84law zb2_none:
85  for +v1: U32
86  for +v2: U32
87  {U32.is_zero(U32.or(FA.zb(v1), FA.zb(v2))) == Nat.is_eq(Nat.min(P0(v1), P0(v2)), 4n) : Bool}
88
89def zb2_none(v1, v2):
90  %Equal.sym(U32, FA.zb(v1), W.zb(v1), W1.zb_eq(v1)) : {U32.is_zero(U32.or(_, FA.zb(v2))) == Nat.is_eq(Nat.min(P0(v1), P0(v2)), 4n) : Bool}
91  %Equal.sym(U32, FA.zb(v2), W.zb(v2), W1.zb_eq(v2)) : {U32.is_zero(U32.or(W.zb(v1), _)) == Nat.is_eq(Nat.min(P0(v1), P0(v2)), 4n) : Bool}
92  %Equal.sym(Bool, U32.is_zero(U32.or(W.zb(v1), W.zb(v2))), Bool.and(U32.is_zero(W.zb(v1)), U32.is_zero(W.zb(v2))), W2.uor0(W.zb(v1), W.zb(v2))) : {_ == Nat.is_eq(Nat.min(P0(v1), P0(v2)), 4n) : Bool}
93  %Equal.sym(Bool, U32.is_zero(W.zb(v1)), Bool.and(U32.is_ne(W.byte(v1, 0n), 0), Bool.and(U32.is_ne(W.byte(v1, 1n), 0), Bool.and(U32.is_ne(W.byte(v1, 2n), 0), U32.is_ne(W.byte(v1, 3n), 0)))), Z.zb_zero(v1)) : {Bool.and(_, U32.is_zero(W.zb(v2))) == Nat.is_eq(Nat.min(P0(v1), P0(v2)), 4n) : Bool}
94  %Equal.sym(Bool, U32.is_zero(W.zb(v2)), Bool.and(U32.is_ne(W.byte(v2, 0n), 0), Bool.and(U32.is_ne(W.byte(v2, 1n), 0), Bool.and(U32.is_ne(W.byte(v2, 2n), 0), U32.is_ne(W.byte(v2, 3n), 0)))), Z.zb_zero(v2)) : {Bool.and(Bool.and(U32.is_ne(W.byte(v1, 0n), 0), Bool.and(U32.is_ne(W.byte(v1, 1n), 0), Bool.and(U32.is_ne(W.byte(v1, 2n), 0), U32.is_ne(W.byte(v1, 3n), 0)))), _) == Nat.is_eq(Nat.min(P0(v1), P0(v2)), 4n) : Bool}
95  W2.bt2_none(U32.is_eq(W.byte(v1, 0n), 0), U32.is_eq(W.byte(v1, 1n), 0), U32.is_eq(W.byte(v1, 2n), 0), U32.is_eq(W.byte(v1, 3n), 0), U32.is_eq(W.byte(v2, 0n), 0), U32.is_eq(W.byte(v2, 1n), 0), U32.is_eq(W.byte(v2, 2n), 0), U32.is_eq(W.byte(v2, 3n), 0))
96
97law zb2_bidx:
98  for +v1: U32
99  for +v2: U32
100  for +h: {Nat.is_lt(Nat.min(P0(v1), P0(v2)), 4n) == True{} : Bool}
101  {U32.to_nat(FA.bidx(U32.or(FA.zb(v1), FA.zb(v2)))) == Nat.min(P0(v1), P0(v2)) : Nat}
102
103def zb2_bidx(v1, v2, h):
104  %Equal.sym(U32, FA.zb(v1), W.zb(v1), W1.zb_eq(v1)) : {U32.to_nat(FA.bidx(U32.or(_, FA.zb(v2)))) == Nat.min(P0(v1), P0(v2)) : Nat}
105  %Equal.sym(U32, FA.zb(v2), W.zb(v2), W1.zb_eq(v2)) : {U32.to_nat(FA.bidx(U32.or(W.zb(v1), _))) == Nat.min(P0(v1), P0(v2)) : Nat}
106  %Equal.sym(Bool, U32.is_zero(U32.and(U32.or(W.zb(v1), W.zb(v2)), 128)), Bool.and(Bool.and(U32.is_ne(W.byte(v1, 0n), 0), True{}), Bool.and(U32.is_ne(W.byte(v2, 0n), 0), True{})), tko1(v1, v2)) : {U32.to_nat(U32.add(U32.add(FA.b2u(_), FA.b2u(U32.is_zero(U32.and(U32.or(W.zb(v1), W.zb(v2)), 32896)))), FA.b2u(U32.is_zero(U32.and(U32.or(W.zb(v1), W.zb(v2)), 8421504))))) == Nat.min(P0(v1), P0(v2)) : Nat}
107  %Equal.sym(Bool, U32.is_zero(U32.and(U32.or(W.zb(v1), W.zb(v2)), 32896)), Bool.and(Bool.and(U32.is_ne(W.byte(v1, 0n), 0), Bool.and(U32.is_ne(W.byte(v1, 1n), 0), True{})), Bool.and(U32.is_ne(W.byte(v2, 0n), 0), Bool.and(U32.is_ne(W.byte(v2, 1n), 0), True{}))), tko2(v1, v2)) : {U32.to_nat(U32.add(U32.add(FA.b2u(Bool.and(Bool.and(U32.is_ne(W.byte(v1, 0n), 0), True{}), Bool.and(U32.is_ne(W.byte(v2, 0n), 0), True{}))), FA.b2u(_)), FA.b2u(U32.is_zero(U32.and(U32.or(W.zb(v1), W.zb(v2)), 8421504))))) == Nat.min(P0(v1), P0(v2)) : Nat}
108  %Equal.sym(Bool, U32.is_zero(U32.and(U32.or(W.zb(v1), W.zb(v2)), 8421504)), Bool.and(Bool.and(U32.is_ne(W.byte(v1, 0n), 0), Bool.and(U32.is_ne(W.byte(v1, 1n), 0), Bool.and(U32.is_ne(W.byte(v1, 2n), 0), True{}))), Bool.and(U32.is_ne(W.byte(v2, 0n), 0), Bool.and(U32.is_ne(W.byte(v2, 1n), 0), Bool.and(U32.is_ne(W.byte(v2, 2n), 0), True{})))), tko3(v1, v2)) : {U32.to_nat(U32.add(U32.add(FA.b2u(Bool.and(Bool.and(U32.is_ne(W.byte(v1, 0n), 0), True{}), Bool.and(U32.is_ne(W.byte(v2, 0n), 0), True{}))), FA.b2u(Bool.and(Bool.and(U32.is_ne(W.byte(v1, 0n), 0), Bool.and(U32.is_ne(W.byte(v1, 1n), 0), True{})), Bool.and(U32.is_ne(W.byte(v2, 0n), 0), Bool.and(U32.is_ne(W.byte(v2, 1n), 0), True{}))))), FA.b2u(_))) == Nat.min(P0(v1), P0(v2)) : Nat}
109  W2.bt2_bidx(U32.is_eq(W.byte(v1, 0n), 0), U32.is_eq(W.byte(v1, 1n), 0), U32.is_eq(W.byte(v1, 2n), 0), U32.is_eq(W.byte(v1, 3n), 0), U32.is_eq(W.byte(v2, 0n), 0), U32.is_eq(W.byte(v2, 1n), 0), U32.is_eq(W.byte(v2, 2n), 0), U32.is_eq(W.byte(v2, 3n), 0), h)
110
111# Searching w for c is searching w xor rep(c) for a zero byte.
112law p0_xor:
113  for +w: U32
114  for +c: U32
115  for +hc: {U32.is_lt(c, 256) == True{} : Bool}
116  {P0(U32.xor(w, FA.rep(c))) == D.run_len(C.L4(w), c) : Nat}
117
118def p0_xor(w, c, hc):
119  %Equal.sym(Bool, U32.is_eq(W.byte(U32.xor(w, FA.rep(c)), 0n), 0), U32.is_eq(W.byte(w, 0n), c), W2.ej_xor(w, c, 0n, hc, {==})) :
120    {W2.R4(_, U32.is_eq(W.byte(U32.xor(w, FA.rep(c)), 1n), 0), U32.is_eq(W.byte(U32.xor(w, FA.rep(c)), 2n), 0), U32.is_eq(W.byte(U32.xor(w, FA.rep(c)), 3n), 0)) == D.run_len(C.L4(w), c) : Nat}
121  %Equal.sym(Bool, U32.is_eq(W.byte(U32.xor(w, FA.rep(c)), 1n), 0), U32.is_eq(W.byte(w, 1n), c), W2.ej_xor(w, c, 1n, hc, {==})) :
122    {W2.R4(U32.is_eq(W.byte(w, 0n), c), _, U32.is_eq(W.byte(U32.xor(w, FA.rep(c)), 2n), 0), U32.is_eq(W.byte(U32.xor(w, FA.rep(c)), 3n), 0)) == D.run_len(C.L4(w), c) : Nat}
123  %Equal.sym(Bool, U32.is_eq(W.byte(U32.xor(w, FA.rep(c)), 2n), 0), U32.is_eq(W.byte(w, 2n), c), W2.ej_xor(w, c, 2n, hc, {==})) :
124    {W2.R4(U32.is_eq(W.byte(w, 0n), c), U32.is_eq(W.byte(w, 1n), c), _, U32.is_eq(W.byte(U32.xor(w, FA.rep(c)), 3n), 0)) == D.run_len(C.L4(w), c) : Nat}
125  %Equal.sym(Bool, U32.is_eq(W.byte(U32.xor(w, FA.rep(c)), 3n), 0), U32.is_eq(W.byte(w, 3n), c), W2.ej_xor(w, c, 3n, hc, {==})) :
126    {W2.R4(U32.is_eq(W.byte(w, 0n), c), U32.is_eq(W.byte(w, 1n), c), U32.is_eq(W.byte(w, 2n), c), _) == D.run_len(C.L4(w), c) : Nat}
127  {==}
128
129law plk0:
130  for +w: U32
131  for +c: U32
132  for +hc: {U32.is_lt(c, 256) == True{} : Bool}
133  {P0(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(0, 3n)))))) == Nat.add(U32.to_nat(0), D.run_len(List.drop(&2, U32, C.L4(w), U32.to_nat(0)), c)) : Nat}
134
135def plk0(w, c, hc):
136  %Equal.sym(Bool, U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(0, 3n))))), 0n), 0), U32.is_eq(W.byte(w, 0n), c), W2.e_hi(w, c, U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(0, 3n)))), 0n, hc, {==}, {==})) :
137    {W2.R4(_, U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(0, 3n))))), 1n), 0), U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(0, 3n))))), 2n), 0), U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(0, 3n))))), 3n), 0)) == Nat.add(U32.to_nat(0), D.run_len(List.drop(&2, U32, C.L4(w), U32.to_nat(0)), c)) : Nat}
138  %Equal.sym(Bool, U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(0, 3n))))), 1n), 0), U32.is_eq(W.byte(w, 1n), c), W2.e_hi(w, c, U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(0, 3n)))), 1n, hc, {==}, {==})) :
139    {W2.R4(U32.is_eq(W.byte(w, 0n), c), _, U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(0, 3n))))), 2n), 0), U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(0, 3n))))), 3n), 0)) == Nat.add(U32.to_nat(0), D.run_len(List.drop(&2, U32, C.L4(w), U32.to_nat(0)), c)) : Nat}
140  %Equal.sym(Bool, U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(0, 3n))))), 2n), 0), U32.is_eq(W.byte(w, 2n), c), W2.e_hi(w, c, U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(0, 3n)))), 2n, hc, {==}, {==})) :
141    {W2.R4(U32.is_eq(W.byte(w, 0n), c), U32.is_eq(W.byte(w, 1n), c), _, U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(0, 3n))))), 3n), 0)) == Nat.add(U32.to_nat(0), D.run_len(List.drop(&2, U32, C.L4(w), U32.to_nat(0)), c)) : Nat}
142  %Equal.sym(Bool, U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(0, 3n))))), 3n), 0), U32.is_eq(W.byte(w, 3n), c), W2.e_hi(w, c, U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(0, 3n)))), 3n, hc, {==}, {==})) :
143    {W2.R4(U32.is_eq(W.byte(w, 0n), c), U32.is_eq(W.byte(w, 1n), c), U32.is_eq(W.byte(w, 2n), c), _) == Nat.add(U32.to_nat(0), D.run_len(List.drop(&2, U32, C.L4(w), U32.to_nat(0)), c)) : Nat}
144  {==}
145
146law plk1:
147  for +w: U32
148  for +c: U32
149  for +hc: {U32.is_lt(c, 256) == True{} : Bool}
150  {P0(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(1, 3n)))))) == Nat.add(U32.to_nat(1), D.run_len(List.drop(&2, U32, C.L4(w), U32.to_nat(1)), c)) : Nat}
151
152def plk1(w, c, hc):
153  %Equal.sym(Bool, U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(1, 3n))))), 0n), 0), False{}, W2.e_lo(w, c, U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(1, 3n)))), 0n, {==})) :
154    {W2.R4(_, U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(1, 3n))))), 1n), 0), U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(1, 3n))))), 2n), 0), U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(1, 3n))))), 3n), 0)) == Nat.add(U32.to_nat(1), D.run_len(List.drop(&2, U32, C.L4(w), U32.to_nat(1)), c)) : Nat}
155  %Equal.sym(Bool, U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(1, 3n))))), 1n), 0), U32.is_eq(W.byte(w, 1n), c), W2.e_hi(w, c, U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(1, 3n)))), 1n, hc, {==}, {==})) :
156    {W2.R4(False{}, _, U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(1, 3n))))), 2n), 0), U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(1, 3n))))), 3n), 0)) == Nat.add(U32.to_nat(1), D.run_len(List.drop(&2, U32, C.L4(w), U32.to_nat(1)), c)) : Nat}
157  %Equal.sym(Bool, U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(1, 3n))))), 2n), 0), U32.is_eq(W.byte(w, 2n), c), W2.e_hi(w, c, U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(1, 3n)))), 2n, hc, {==}, {==})) :
158    {W2.R4(False{}, U32.is_eq(W.byte(w, 1n), c), _, U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(1, 3n))))), 3n), 0)) == Nat.add(U32.to_nat(1), D.run_len(List.drop(&2, U32, C.L4(w), U32.to_nat(1)), c)) : Nat}
159  %Equal.sym(Bool, U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(1, 3n))))), 3n), 0), U32.is_eq(W.byte(w, 3n), c), W2.e_hi(w, c, U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(1, 3n)))), 3n, hc, {==}, {==})) :
160    {W2.R4(False{}, U32.is_eq(W.byte(w, 1n), c), U32.is_eq(W.byte(w, 2n), c), _) == Nat.add(U32.to_nat(1), D.run_len(List.drop(&2, U32, C.L4(w), U32.to_nat(1)), c)) : Nat}
161  {==}
162
163law plk2:
164  for +w: U32
165  for +c: U32
166  for +hc: {U32.is_lt(c, 256) == True{} : Bool}
167  {P0(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(2, 3n)))))) == Nat.add(U32.to_nat(2), D.run_len(List.drop(&2, U32, C.L4(w), U32.to_nat(2)), c)) : Nat}
168
169def plk2(w, c, hc):
170  %Equal.sym(Bool, U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(2, 3n))))), 0n), 0), False{}, W2.e_lo(w, c, U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(2, 3n)))), 0n, {==})) :
171    {W2.R4(_, U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(2, 3n))))), 1n), 0), U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(2, 3n))))), 2n), 0), U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(2, 3n))))), 3n), 0)) == Nat.add(U32.to_nat(2), D.run_len(List.drop(&2, U32, C.L4(w), U32.to_nat(2)), c)) : Nat}
172  %Equal.sym(Bool, U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(2, 3n))))), 1n), 0), False{}, W2.e_lo(w, c, U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(2, 3n)))), 1n, {==})) :
173    {W2.R4(False{}, _, U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(2, 3n))))), 2n), 0), U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(2, 3n))))), 3n), 0)) == Nat.add(U32.to_nat(2), D.run_len(List.drop(&2, U32, C.L4(w), U32.to_nat(2)), c)) : Nat}
174  %Equal.sym(Bool, U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(2, 3n))))), 2n), 0), U32.is_eq(W.byte(w, 2n), c), W2.e_hi(w, c, U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(2, 3n)))), 2n, hc, {==}, {==})) :
175    {W2.R4(False{}, False{}, _, U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(2, 3n))))), 3n), 0)) == Nat.add(U32.to_nat(2), D.run_len(List.drop(&2, U32, C.L4(w), U32.to_nat(2)), c)) : Nat}
176  %Equal.sym(Bool, U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(2, 3n))))), 3n), 0), U32.is_eq(W.byte(w, 3n), c), W2.e_hi(w, c, U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(2, 3n)))), 3n, hc, {==}, {==})) :
177    {W2.R4(False{}, False{}, U32.is_eq(W.byte(w, 2n), c), _) == Nat.add(U32.to_nat(2), D.run_len(List.drop(&2, U32, C.L4(w), U32.to_nat(2)), c)) : Nat}
178  {==}
179
180law plk3:
181  for +w: U32
182  for +c: U32
183  for +hc: {U32.is_lt(c, 256) == True{} : Bool}
184  {P0(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(3, 3n)))))) == Nat.add(U32.to_nat(3), D.run_len(List.drop(&2, U32, C.L4(w), U32.to_nat(3)), c)) : Nat}
185
186def plk3(w, c, hc):
187  %Equal.sym(Bool, U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(3, 3n))))), 0n), 0), False{}, W2.e_lo(w, c, U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(3, 3n)))), 0n, {==})) :
188    {W2.R4(_, U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(3, 3n))))), 1n), 0), U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(3, 3n))))), 2n), 0), U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(3, 3n))))), 3n), 0)) == Nat.add(U32.to_nat(3), D.run_len(List.drop(&2, U32, C.L4(w), U32.to_nat(3)), c)) : Nat}
189  %Equal.sym(Bool, U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(3, 3n))))), 1n), 0), False{}, W2.e_lo(w, c, U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(3, 3n)))), 1n, {==})) :
190    {W2.R4(False{}, _, U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(3, 3n))))), 2n), 0), U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(3, 3n))))), 3n), 0)) == Nat.add(U32.to_nat(3), D.run_len(List.drop(&2, U32, C.L4(w), U32.to_nat(3)), c)) : Nat}
191  %Equal.sym(Bool, U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(3, 3n))))), 2n), 0), False{}, W2.e_lo(w, c, U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(3, 3n)))), 2n, {==})) :
192    {W2.R4(False{}, False{}, _, U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(3, 3n))))), 3n), 0)) == Nat.add(U32.to_nat(3), D.run_len(List.drop(&2, U32, C.L4(w), U32.to_nat(3)), c)) : Nat}
193  %Equal.sym(Bool, U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(3, 3n))))), 3n), 0), U32.is_eq(W.byte(w, 3n), c), W2.e_hi(w, c, U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(3, 3n)))), 3n, hc, {==}, {==})) :
194    {W2.R4(False{}, False{}, False{}, _) == Nat.add(U32.to_nat(3), D.run_len(List.drop(&2, U32, C.L4(w), U32.to_nat(3)), c)) : Nat}
195  {==}
196
197# The first word for a start place a (0 to 3, given as r).
198law pl:
199  for +w: U32
200  for +c: U32
201  for +a: U32
202  for +r: Nat
203  for +hc: {U32.is_lt(c, 256) == True{} : Bool}
204  for +hr: {U32.to_nat(a) == r : Nat}
205  for +hlt: {Nat.is_lt(r, 4n) == True{} : Bool}
206  {P0(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(a, 3n)))))) == Nat.add(U32.to_nat(a), D.run_len(List.drop(&2, U32, C.L4(w), U32.to_nat(a)), c)) : Nat}
207
208def pl(w, c, a, r, hc, hr, hlt):
209  match r:
210    case 0n:
211      %Equal.sym(U32, a, 0, U.to_nat_inj(a, 0, hr)) :
212        {P0(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(_, 3n)))))) == Nat.add(U32.to_nat(_), D.run_len(List.drop(&2, U32, C.L4(w), U32.to_nat(_)), c)) : Nat}
213      plk0(w, c, hc)
214    case 1n+r1:
215      match r1:
216        case 0n:
217          %Equal.sym(U32, a, 1, U.to_nat_inj(a, 1, hr)) :
218            {P0(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(_, 3n)))))) == Nat.add(U32.to_nat(_), D.run_len(List.drop(&2, U32, C.L4(w), U32.to_nat(_)), c)) : Nat}
219          plk1(w, c, hc)
220        case 1n+r2:
221          match r2:
222            case 0n:
223              %Equal.sym(U32, a, 2, U.to_nat_inj(a, 2, hr)) :
224                {P0(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(_, 3n)))))) == Nat.add(U32.to_nat(_), D.run_len(List.drop(&2, U32, C.L4(w), U32.to_nat(_)), c)) : Nat}
225              plk2(w, c, hc)
226            case 1n+r3:
227              match r3:
228                case 0n:
229                  %Equal.sym(U32, a, 3, U.to_nat_inj(a, 3, hr)) :
230                    {P0(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(_, 3n)))))) == Nat.add(U32.to_nat(_), D.run_len(List.drop(&2, U32, C.L4(w), U32.to_nat(_)), c)) : Nat}
231                  plk3(w, c, hc)
232                case 1n+r4:
233                  Empty.absurd({P0(U32.or(U32.xor(w, FA.rep(c)), U32.not(U32.shln(4294967295, U32.to_nat(U32.shln(a, 3n)))))) == Nat.add(U32.to_nat(a), D.run_len(List.drop(&2, U32, C.L4(w), U32.to_nat(a)), c)) : Nat}, AB.lt_zero_absurd(r4, hlt))
234
235# The first word of a search: the bytes below i's place are set to 0xFF, so
236# the first zero byte is the first c at or above that place.
237law p0_low:
238  for +w: U32
239  for +c: U32
240  for +i: U32
241  for +hc: {U32.is_lt(c, 256) == True{} : Bool}
242  {P0(U32.or(U32.xor(w, FA.rep(c)), U32.not(FA.low(i)))) == Nat.add(U32.to_nat((i .&. 3 : U32)), D.run_len(List.drop(&2, U32, C.L4(w), U32.to_nat((i .&. 3 : U32))), c)) : Nat}
243
244def p0_low(w, c, i, hc):
245  +a = (i .&. 3 : U32)
246  pl(w, c, a, U32.to_nat(a), hc, {==},
247    AB.subst(Nat, y => {Nat.is_lt(y, 4n) == True{} : Bool}, Nat.mod(U32.to_nat(i), Nat.pow(2n, 2n)), U32.to_nat(a),
248      Equal.sym(Nat, U32.to_nat(a), Nat.mod(U32.to_nat(i), Nat.pow(2n, 2n)), U.to_nat_and_mask(i, 3, 2n, {==})),
249      N.mod_lt(U32.to_nat(i), Nat.pow(2n, 2n), {==})))