1 import Base 2 import lawful-words@0.1.0.0/defs.bend as W 3 import ./defs.bend as D 4 import ./fast.bend as FA 5 import ./proof_core.bend as C 6 import lawful-words@0.1.0.0/proof_nat.bend as N 7 import lawful-words@0.1.0.0/proof_u32.bend as U 8 import lawful-words@0.1.0.0/proof_zb.bend as Z 9 import lawful-arrays@0.1.0.0/proof_base.bend as AB 10 import ./proof_fast_w1.bend as W1 11 import ./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). 18 def 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. 22 law 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 27 def 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. 35 law 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 40 def 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. 48 law 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 53 def 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. 61 law zb_none: 62 for +v: U32 63 {U32.is_zero(FA.zb(v)) == Nat.is_eq(P0(v), 4n) : Bool} 64 65 def 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. 71 law 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 76 def 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). 84 law 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 89 def 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 97 law 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 103 def 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. 112 law 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 118 def 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 129 law 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 135 def 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 146 law 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 152 def 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 163 law 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 169 def 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 180 law 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 186 def 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). 198 law 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 208 def 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. 237 law 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 244 def 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), {==})))