proofs/crypto/poly1305/final.bend source
proofs/crypto/poly1305/final.bend on the hub · documented module
import Baseimport ../../../spec/lib/common.bend as Cimport ../../../spec/crypto/poly1305.bend as Rimport ../../../src/crypto/poly1305/limbs.bend as Liimport ../../lib/nat.bend as Nimport ../../lib/logic.bend as Limport ../../lib/arith.bend as ARimport ../../lib/u32.bend as U3import ../../lib/u32alg.bend as UAimport ../../lib/lemmas/proofs/nat_algebra.bend as NAimport ../../math/typed/width.bend as WWimport ../../math/typed/w64mul.bend as WMimport ../../math/typed/w64sh.bend as SHimport ../../math/typed/shrn.bend as SHNimport ../../math/typed/f64bits.bend as FBimport ../../math/natural/arith.bend as NRimport ./arith.bend as Aimport ./value.bend as Vimport ./step.bend as ST# The last steps: freeze (the canonical value mod p, by a masked choice) and# the 16 tag bytes (h + s mod 2^128, little-endian).# ---- words ----def wones(n: Nat) -> Word(n): match n: case 0n: WNil{} case 1n+p: WCon{True{}, wones(p)}law wand0: for +n: Nat for +w: Word(n) {Word.and(n, Word.zero(n), w) == Word.zero(n) : Word(n)}def wand0(n, w): match n: case 0n: match w: case WNil{}: {==} case 1n+p: match w: case WCon{b, t}: Equal.cong(Word(p), Word(1n+p), x => WCon{False{}, x}, Word.and(p, Word.zero(p), t), Word.zero(p), wand0(p, t))law wand1: for +n: Nat for +w: Word(n) {Word.and(n, wones(n), w) == w : Word(n)}def wand1(n, w): match n: case 0n: match w: case WNil{}: {==} case 1n+p: match w: case WCon{b, t}: Equal.cong(Word(p), Word(1n+p), x => WCon{b, x}, Word.and(p, wones(p), t), t, wand1(p, t))law wxor0: for +n: Nat for +w: Word(n) {Word.xor(n, w, Word.zero(n)) == w : Word(n)}def wxor0(n, w): match n: case 0n: match w: case WNil{}: {==} case 1n+p: match w: case WCon{b, t}: match b: case False{}: Equal.cong(Word(p), Word(1n+p), x => WCon{False{}, x}, Word.xor(p, t, Word.zero(p)), t, wxor0(p, t)) case True{}: Equal.cong(Word(p), Word(1n+p), x => WCon{True{}, x}, Word.xor(p, t, Word.zero(p)), t, wxor0(p, t))law wxor2: for +n: Nat for +x: Word(n) for +y: Word(n) {Word.xor(n, x, Word.xor(n, x, y)) == y : Word(n)}def wxor2(n, x, y): match n: case 0n: match x y: case WNil{} WNil{}: {==} case 1n+p: match x y: case WCon{False{}, s} WCon{False{}, t}: Equal.cong(Word(p), Word(1n+p), z => WCon{False{}, z}, Word.xor(p, s, Word.xor(p, s, t)), t, wxor2(p, s, t)) case WCon{False{}, s} WCon{True{}, t}: Equal.cong(Word(p), Word(1n+p), z => WCon{True{}, z}, Word.xor(p, s, Word.xor(p, s, t)), t, wxor2(p, s, t)) case WCon{True{}, s} WCon{False{}, t}: Equal.cong(Word(p), Word(1n+p), z => WCon{False{}, z}, Word.xor(p, s, Word.xor(p, s, t)), t, wxor2(p, s, t)) case WCon{True{}, s} WCon{True{}, t}: Equal.cong(Word(p), Word(1n+p), z => WCon{True{}, z}, Word.xor(p, s, Word.xor(p, s, t)), t, wxor2(p, s, t))def pick0(+x: U32, +y: U32) -> {Li.pick(0, x, y) == x : U32}: match x y: case U32{a} U32{b}: Equal.trans(U32, U32{Word.xor(32n, a, Word.and(32n, Word.zero(32n), Word.xor(32n, a, b)))}, U32{Word.xor(32n, a, Word.zero(32n))}, U32{a}, Equal.cong(Word(32n), U32, w => U32{Word.xor(32n, a, w)}, Word.and(32n, Word.zero(32n), Word.xor(32n, a, b)), Word.zero(32n), wand0(32n, Word.xor(32n, a, b))), Equal.cong(Word(32n), U32, w => U32{w}, Word.xor(32n, a, Word.zero(32n)), a, wxor0(32n, a)))def pick1(+x: U32, +y: U32) -> {Li.pick(4294967295, x, y) == y : U32}: match x y: case U32{a} U32{b}: Equal.trans(U32, U32{Word.xor(32n, a, Word.and(32n, wones(32n), Word.xor(32n, a, b)))}, U32{Word.xor(32n, a, Word.xor(32n, a, b))}, U32{b}, Equal.cong(Word(32n), U32, w => U32{Word.xor(32n, a, w)}, Word.and(32n, wones(32n), Word.xor(32n, a, b)), Word.xor(32n, a, b), wand1(32n, Word.xor(32n, a, b))), Equal.cong(Word(32n), U32, w => U32{w}, Word.xor(32n, a, Word.xor(32n, a, b)), b, wxor2(32n, a, b)))law sel0: for +a: List<&2, U32> for +b: List<&2, U32> for +h: {V.len(a) == V.len(b) : Nat} {Li.select(0, a, b) == a : List<&2, U32>}def sel0(a, b, h): match a b: case Nil{} Nil{}: {==} case Nil{} y <> bt: Empty.absurd({Li.select(0, [], y <> bt) == [] : List<&2, U32>}, N.zero_succ(V.len(bt), h)) case x <> at Nil{}: Empty.absurd({Li.select(0, x <> at, []) == x <> at : List<&2, U32>}, N.succ_zero(V.len(at), h)) case x <> at y <> bt: Equal.trans(List<&2, U32>, Li.pick(0, x, y) <> Li.select(0, at, bt), x <> Li.select(0, at, bt), x <> at, Equal.cong(U32, List<&2, U32>, z => z <> Li.select(0, at, bt), Li.pick(0, x, y), x, pick0(x, y)), Equal.cong(List<&2, U32>, List<&2, U32>, z => x <> z, Li.select(0, at, bt), at, sel0(at, bt, N.succ_inj(V.len(at), V.len(bt), h))))law sel1: for +a: List<&2, U32> for +b: List<&2, U32> for +h: {V.len(a) == V.len(b) : Nat} {Li.select(4294967295, a, b) == b : List<&2, U32>}def sel1(a, b, h): match a b: case Nil{} Nil{}: {==} case Nil{} y <> bt: Empty.absurd({Li.select(4294967295, [], y <> bt) == y <> bt : List<&2, U32>}, N.zero_succ(V.len(bt), h)) case x <> at Nil{}: Empty.absurd({Li.select(4294967295, x <> at, []) == [] : List<&2, U32>}, N.succ_zero(V.len(at), h)) case x <> at y <> bt: Equal.trans(List<&2, U32>, Li.pick(4294967295, x, y) <> Li.select(4294967295, at, bt), y <> Li.select(4294967295, at, bt), y <> bt, Equal.cong(U32, List<&2, U32>, z => z <> Li.select(4294967295, at, bt), Li.pick(4294967295, x, y), y, pick1(x, y)), Equal.cong(List<&2, U32>, List<&2, U32>, z => y <> z, Li.select(4294967295, at, bt), bt, sel1(at, bt, N.succ_inj(V.len(at), V.len(bt), h))))law len_take_eq: for +n: Nat for +xs: List<&2, U32> for +h: {Nat.is_le(n, V.len(xs)) == True{} : Bool} {V.len(Li.take(n, xs)) == n : Nat}def len_take_eq(n, xs, h): match n xs: case 0n _: {==} case 1n+k Nil{}: Empty.absurd({V.len(Li.take(1n+k, [])) == 1n+k : Nat}, L.false_true(h)) case 1n+k x <> t: Equal.cong(Nat, Nat, z => 1n+z, V.len(Li.take(k, t)), k, len_take_eq(k, t, h))# ---- freeze ----# x < 2x for x >= 1def lt_dbl(+x: Nat, +h: {Nat.is_le(1n, x) == True{} : Bool}) -> {Nat.is_lt(x, Nat.double(x)) == True{} : Bool}: A.lt_subst(x, Nat.add(x, x), Nat.double(x), A.sy(Nat.double(x), Nat.add(x, x), NA.double_self(x)), A.lt_substl(Nat.add(x, 0n), x, Nat.add(x, x), N.add_zero(x), N.lt_add_left(0n, x, x, N.succ_le_lt(0n, x, h))))# the facts about h, g = carry(h + 5) and the choice bit shared by both casesdef hval(+h: List<&2, U32>) -> Nat: V.ev(h)def gg(+h: List<&2, U32>) -> List<&2, U32>: Li.carry(16n, Li.add(h, [5]), 0)def qq(+h: List<&2, U32>) -> Nat: C.high(130n, Nat.add(V.ev(h), 5n))law g_ev: for +one: Nat for +h1: {one == 1n : Nat} for +h: List<&2, U32> for +hh: {ST.inv(h) == True{} : Bool} {V.ev(gg(h)) == Nat.add(V.ev(h), 5n) : Nat}def g_ev(one, h1, h, hh): +s8 = C.shift(8n, one) +hl = N.eq_from_is_eq(V.len(h), 17n, L.and_left(Nat.is_eq(V.len(h), 17n), Bool.and(V.fit_all(h, 8n), Nat.is_le(V.v(Li.hd0(Li.skip(16n, h))), 4n)), hh)) +hr2 = L.and_right(Nat.is_eq(V.len(h), 17n), Bool.and(V.fit_all(h, 8n), Nat.is_le(V.v(Li.hd0(Li.skip(16n, h))), 4n)), hh) +hf = L.and_left(V.fit_all(h, 8n), Nat.is_le(V.v(Li.hd0(Li.skip(16n, h))), 4n), hr2) +a = Li.add(h, [5]) +h5 = V.cons_le(5, [], s8, L.subst(Nat, z => {Nat.is_le(5n, C.shift(8n, z)) == True{} : Bool}, 1n, one, A.sy(one, 1n, h1), {==}), {==}) +hf1 = ST.s8fit(one, h1) +ea = V.add_ev(h, [5], s8, s8, V.fit_le(h, 8n, one, h1, hf), h5, hf1) +s9 = C.shift(9n, one) +l10 = A.lt_substl(s9, Nat.add(s8, s8), Nat.double(s9), NA.double_self(s8), lt_dbl(s9, A.one_le_shift(9n, one, h1))) +ha = V.le_fit(a, Nat.add(s8, s8), 10n, one, h1, l10, V.add_le(h, [5], s8, s8, V.fit_le(h, 8n, one, h1, hf), h5, hf1)) +hal = V.len_add(h, [5], 17n, N.eq_le(V.len(h), 17n, hl), {==}) +ce = V.carry_ev(16n, a, 0, 2n, {==}, ha, {==}) +sk = V.skip_long(17n, a, hal) A.tr(V.ev(gg(h)), Nat.add(V.ev(gg(h)), V.pos(17n, V.ev(Li.skip(17n, a)))), Nat.add(V.ev(h), 5n), A.tr(V.ev(gg(h)), Nat.add(V.ev(gg(h)), 0n), Nat.add(V.ev(gg(h)), V.pos(17n, V.ev(Li.skip(17n, a)))), A.sy(Nat.add(V.ev(gg(h)), 0n), V.ev(gg(h)), N.add_zero(V.ev(gg(h)))), Equal.cong(List<&2, U32>, Nat, l => Nat.add(V.ev(gg(h)), V.pos(17n, V.ev(l))), [], Li.skip(17n, a), Equal.sym(List<&2, U32>, Li.skip(17n, a), [], sk))), A.tr(Nat.add(V.ev(gg(h)), V.pos(17n, V.ev(Li.skip(17n, a)))), V.ev(a), Nat.add(V.ev(h), 5n), ce, ea))def lenh(+h: List<&2, U32>, +hh: {ST.inv(h) == True{} : Bool}) -> {V.len(h) == 17n : Nat}: N.eq_from_is_eq(V.len(h), 17n, L.and_left(Nat.is_eq(V.len(h), 17n), Bool.and(V.fit_all(h, 8n), Nat.is_le(V.v(Li.hd0(Li.skip(16n, h))), 4n)), hh))def fith(+h: List<&2, U32>, +hh: {ST.inv(h) == True{} : Bool}) -> {V.fit_all(h, 8n) == True{} : Bool}: L.and_left(V.fit_all(h, 8n), Nat.is_le(V.v(Li.hd0(Li.skip(16n, h))), 4n), L.and_right(Nat.is_eq(V.len(h), 17n), Bool.and(V.fit_all(h, 8n), Nat.is_le(V.v(Li.hd0(Li.skip(16n, h))), 4n)), hh))def toph(+h: List<&2, U32>, +hh: {ST.inv(h) == True{} : Bool}) -> {Nat.is_le(V.v(Li.hd0(Li.skip(16n, h))), 4n) == True{} : Bool}: L.and_right(V.fit_all(h, 8n), Nat.is_le(V.v(Li.hd0(Li.skip(16n, h))), 4n), L.and_right(Nat.is_eq(V.len(h), 17n), Bool.and(V.fit_all(h, 8n), Nat.is_le(V.v(Li.hd0(Li.skip(16n, h))), 4n)), hh))def len16(+h: List<&2, U32>, +hh: {ST.inv(h) == True{} : Bool}) -> {V.len(Li.take(16n, h)) == 16n : Nat}: len_take_eq(16n, h, A.le_subst(16n, 17n, V.len(h), A.sy(V.len(h), 17n, lenh(h, hh)), {==}))law hsplit: for +h: List<&2, U32> for +hh: {ST.inv(h) == True{} : Bool} {V.ev(h) == Nat.add(V.ev(Li.take(16n, h)), V.pos(16n, V.v(Li.hd0(Li.skip(16n, h))))) : Nat}def hsplit(h, hh): +sk = Li.skip(16n, h) A.tr(V.ev(h), Nat.add(V.ev(Li.take(16n, h)), V.pos(16n, V.ev(sk))), Nat.add(V.ev(Li.take(16n, h)), V.pos(16n, V.v(Li.hd0(sk)))), V.ts_ev(16n, h), WM.cong_r(V.ev(Li.take(16n, h)), V.pos(16n, V.ev(sk)), V.pos(16n, V.v(Li.hd0(sk))), Equal.cong(Nat, Nat, z => V.pos(16n, z), V.ev(sk), V.v(Li.hd0(sk)), V.ev_one(sk, V.len_skip(16n, h, 1n, N.eq_le(V.len(h), 17n, lenh(h, hh)))))))# ev(h) < 2^128 + 2^130law hlt: for +one: Nat for +h1: {one == 1n : Nat} for +h: List<&2, U32> for +hh: {ST.inv(h) == True{} : Bool} {Nat.is_lt(V.ev(h), Nat.add(V.pos(16n, one), C.shift(130n, one))) == True{} : Bool}def hlt(one, h1, h, hh): +lh = V.ev(Li.take(16n, h)) +vt = V.v(Li.hd0(Li.skip(16n, h))) +u = V.pos(16n, one) +l1 = A.lt_subst(lh, V.pos(V.len(Li.take(16n, h)), one), u, Equal.cong(Nat, Nat, z => V.pos(z, one), V.len(Li.take(16n, h)), 16n, len16(h, hh)), V.ev_lt(Li.take(16n, h), one, h1, V.fit_take(16n, h, 8n, fith(h, hh)))) +e4 = A.sy(C.shift(2n, one), 4n, Equal.cong(Nat, Nat, z => C.shift(2n, z), one, 1n, h1)) +l2 = WW.shift_mono(128n, vt, C.shift(2n, one), A.le_subst(vt, 4n, C.shift(2n, one), e4, toph(h, hh))) A.lt_substl(Nat.add(lh, V.pos(16n, vt)), V.ev(h), Nat.add(u, C.shift(130n, one)), A.sy(V.ev(h), Nat.add(lh, V.pos(16n, vt)), hsplit(h, hh)), A.lt_le_add(lh, V.pos(16n, vt), u, C.shift(130n, one), l1, l2))def lg(+h: List<&2, U32>) -> Nat: V.ev(Li.take(16n, gg(h)))def tg(+h: List<&2, U32>) -> Nat: Nat.add(V.v(Li.hd0(Li.skip(16n, gg(h)))), 0n)law gsplit: for +one: Nat for +h1: {one == 1n : Nat} for +h: List<&2, U32> for +hh: {ST.inv(h) == True{} : Bool} {Nat.add(V.ev(h), 5n) == Nat.add(lg(h), C.shift(128n, tg(h))) : Nat}def gsplit(one, h1, h, hh): A.tr(Nat.add(V.ev(h), 5n), V.ev(gg(h)), Nat.add(lg(h), C.shift(128n, tg(h))), A.sy(V.ev(gg(h)), Nat.add(V.ev(h), 5n), g_ev(one, h1, h, hh)), V.ts_ev(16n, gg(h)))def flg(+one: Nat, +h1: {one == 1n : Nat}, +h: List<&2, U32>) -> {C.fits(128n, lg(h)) == True{} : Bool}: WW.fits_one(128n, one, h1, lg(h), V.ev_lt(Li.take(16n, gg(h)), one, h1, V.carry_lo(16n, Li.add(h, [5]), 0)))def bb(+h: List<&2, U32>) -> U32: U32.shrn(Li.hd0(Li.skip(16n, gg(h))), 2n)law bval: for +one: Nat for +h1: {one == 1n : Nat} for +h: List<&2, U32> for +hh: {ST.inv(h) == True{} : Bool} {V.v(bb(h)) == qq(h) : Nat}def bval(one, h1, h, hh): +x = Nat.add(V.ev(h), 5n) +tp = V.v(Li.hd0(Li.skip(16n, gg(h)))) +ehi = A.tr(C.high(128n, x), C.high(128n, Nat.add(lg(h), C.shift(128n, tg(h)))), tg(h), Equal.cong(Nat, Nat, z => C.high(128n, z), x, Nat.add(lg(h), C.shift(128n, tg(h))), gsplit(one, h1, h, hh)), WW.high_u(128n, lg(h), tg(h), flg(one, h1, h))) A.tr(V.v(bb(h)), C.high(2n, tp), qq(h), SHN.shrn_high(Li.hd0(Li.skip(16n, gg(h))), 2n), A.tr(C.high(2n, tp), C.high(2n, C.high(128n, x)), qq(h), Equal.cong(Nat, Nat, z => C.high(2n, z), tp, C.high(128n, x), A.tr(tp, tg(h), C.high(128n, x), A.sy(tg(h), tp, N.add_zero(tp)), A.sy(C.high(128n, x), tg(h), ehi))), A.sy(qq(h), C.high(2n, C.high(128n, x)), WW.high_comp(2n, 128n, x))))# 2^128 + 5 <= 2^130, 16 <= 2^128def u16(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(16n, V.pos(16n, one)) == True{} : Bool}: N.le_trans(16n, C.shift(4n, one), V.pos(16n, one), L.subst(Nat, z => {Nat.is_le(16n, C.shift(4n, z)) == True{} : Bool}, 1n, one, A.sy(one, 1n, h1), {==}), WW.shift_ge(124n, C.shift(4n, one)))def uu(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(Nat.add(V.pos(16n, one), V.pos(16n, one)), C.shift(130n, one)) == True{} : Bool}: +u = V.pos(16n, one) A.le_substl(Nat.double(u), Nat.add(u, u), C.shift(130n, one), NA.double_self(u), WW.shift_ge(1n, Nat.double(u)))law qlt2: for +one: Nat for +h1: {one == 1n : Nat} for +h: List<&2, U32> for +hh: {ST.inv(h) == True{} : Bool} {Nat.is_lt(qq(h), 2n) == True{} : Bool}def qlt2(one, h1, h, hh): +u = V.pos(16n, one) +s = C.shift(130n, one) +x = Nat.add(V.ev(h), 5n) +l1 = N.lt_add_r2(V.ev(h), Nat.add(u, s), 5n, hlt(one, h1, h, hh)) +e1 = A.tr(Nat.add(Nat.add(u, s), 5n), Nat.add(u, Nat.add(s, 5n)), Nat.add(s, Nat.add(u, 5n)), N.add_assoc(u, s, 5n), A.tr(Nat.add(u, Nat.add(s, 5n)), Nat.add(u, Nat.add(5n, s)), Nat.add(s, Nat.add(u, 5n)), WM.cong_r(u, Nat.add(s, 5n), Nat.add(5n, s), N.add_comm(s, 5n)), A.tr(Nat.add(u, Nat.add(5n, s)), Nat.add(Nat.add(u, 5n), s), Nat.add(s, Nat.add(u, 5n)), A.sy(Nat.add(Nat.add(u, 5n), s), Nat.add(u, Nat.add(5n, s)), N.add_assoc(u, 5n, s)), N.add_comm(Nat.add(u, 5n), s)))) +l2 = N.le_add_left(Nat.add(u, 5n), s, s, N.le_trans(Nat.add(u, 5n), Nat.add(u, u), s, N.le_add_left(5n, u, u, N.le_trans(5n, 16n, u, {==}, u16(one, h1))), uu(one, h1))) +l3 = N.lt_le_trans(x, Nat.add(s, Nat.add(u, 5n)), Nat.add(s, s), A.lt_subst(x, Nat.add(Nat.add(u, s), 5n), Nat.add(s, Nat.add(u, 5n)), e1, l1), l2) +f131 = WW.fits_one(131n, one, h1, x, A.lt_subst(x, Nat.add(s, s), Nat.double(s), A.sy(Nat.double(s), Nat.add(s, s), NA.double_self(s)), l3)) WW.lt_of_fits(1n, qq(h), SH.fits_high(130n, 1n, x, f131))def heqlen(+h: List<&2, U32>, +hh: {ST.inv(h) == True{} : Bool}) -> {V.len(Li.take(16n, h)) == V.len(Li.take(16n, gg(h))) : Nat}: A.tr(V.len(Li.take(16n, h)), 16n, V.len(Li.take(16n, gg(h))), len16(h, hh), {==})def qone(+one: Nat, +h1: {one == 1n : Nat}, +h: List<&2, U32>, +hh: {ST.inv(h) == True{} : Bool}, +hc: {Nat.is_eq(qq(h), 0n) == False{} : Bool}) -> {qq(h) == 1n : Nat}: N.le_antisym(qq(h), 1n, N.lt_succ_le(qq(h), 1n, qlt2(one, h1, h, hh)), N.lt_succ_le_succ(0n, qq(h), N.lt_or_eq(0n, qq(h), N.zero_le(qq(h)), N.is_eq_sym_false(qq(h), 0n, hc))))def which0(+one: Nat, +h1: {one == 1n : Nat}, +h: List<&2, U32>, +hh: {ST.inv(h) == True{} : Bool}, +hc: {Nat.is_eq(qq(h), 0n) == True{} : Bool}) -> {Li.freeze(h) == Li.take(16n, h) : List<&2, U32>}: +eb = U3.injective(bb(h), 0, A.tr(V.v(bb(h)), qq(h), 0n, bval(one, h1, h, hh), N.eq_from_is_eq(qq(h), 0n, hc))) Equal.trans(List<&2, U32>, Li.freeze(h), Li.select(U32.sub(0, 0), Li.take(16n, h), Li.take(16n, gg(h))), Li.take(16n, h), Equal.cong(U32, List<&2, U32>, w => Li.select(U32.sub(0, w), Li.take(16n, h), Li.take(16n, gg(h))), bb(h), 0, eb), sel0(Li.take(16n, h), Li.take(16n, gg(h)), heqlen(h, hh)))def which1(+one: Nat, +h1: {one == 1n : Nat}, +h: List<&2, U32>, +hh: {ST.inv(h) == True{} : Bool}, +hc: {Nat.is_eq(qq(h), 0n) == False{} : Bool}) -> {Li.freeze(h) == Li.take(16n, gg(h)) : List<&2, U32>}: +eb = U3.injective(bb(h), 1, A.tr(V.v(bb(h)), qq(h), 1n, bval(one, h1, h, hh), qone(one, h1, h, hh, hc))) Equal.trans(List<&2, U32>, Li.freeze(h), Li.select(U32.sub(0, 1), Li.take(16n, h), Li.take(16n, gg(h))), Li.take(16n, gg(h)), Equal.cong(U32, List<&2, U32>, w => Li.select(U32.sub(0, w), Li.take(16n, h), Li.take(16n, gg(h))), bb(h), 1, eb), sel1(Li.take(16n, h), Li.take(16n, gg(h)), heqlen(h, hh)))def which_c(+one: Nat, +h1: {one == 1n : Nat}, +h: List<&2, U32>, +hh: {ST.inv(h) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(qq(h), 0n) == c : Bool}) -> Or({Li.freeze(h) == Li.take(16n, h) : List<&2, U32>}, {Li.freeze(h) == Li.take(16n, gg(h)) : List<&2, U32>}): match c: case True{}: Inl{which0(one, h1, h, hh, hc)} case False{}: Inr{which1(one, h1, h, hh, hc)}def fz_fit_o(+h: List<&2, U32>, +hh: {ST.inv(h) == True{} : Bool}, o: Or({Li.freeze(h) == Li.take(16n, h) : List<&2, U32>}, {Li.freeze(h) == Li.take(16n, gg(h)) : List<&2, U32>})) -> {V.fit_all(Li.freeze(h), 8n) == True{} : Bool}: match o: case Inl{e}: L.subst(List<&2, U32>, l => {V.fit_all(l, 8n) == True{} : Bool}, Li.take(16n, h), Li.freeze(h), Equal.sym(List<&2, U32>, Li.freeze(h), Li.take(16n, h), e), V.fit_take(16n, h, 8n, fith(h, hh))) case Inr{e}: L.subst(List<&2, U32>, l => {V.fit_all(l, 8n) == True{} : Bool}, Li.take(16n, gg(h)), Li.freeze(h), Equal.sym(List<&2, U32>, Li.freeze(h), Li.take(16n, gg(h)), e), V.carry_lo(16n, Li.add(h, [5]), 0))law freeze_fit: for +one: Nat for +h1: {one == 1n : Nat} for +h: List<&2, U32> for +hh: {ST.inv(h) == True{} : Bool} {V.fit_all(Li.freeze(h), 8n) == True{} : Bool}def freeze_fit(one, h1, h, hh): fz_fit_o(h, hh, which_c(one, h1, h, hh, Nat.is_eq(qq(h), 0n), {==}))law freeze_len: for +one: Nat for +h1: {one == 1n : Nat} for +h: List<&2, U32> for +hh: {ST.inv(h) == True{} : Bool} {Nat.is_le(V.len(Li.freeze(h)), 16n) == True{} : Bool}def fz_len_o(+h: List<&2, U32>, o: Or({Li.freeze(h) == Li.take(16n, h) : List<&2, U32>}, {Li.freeze(h) == Li.take(16n, gg(h)) : List<&2, U32>})) -> {Nat.is_le(V.len(Li.freeze(h)), 16n) == True{} : Bool}: match o: case Inl{e}: L.subst(List<&2, U32>, l => {Nat.is_le(V.len(l), 16n) == True{} : Bool}, Li.take(16n, h), Li.freeze(h), Equal.sym(List<&2, U32>, Li.freeze(h), Li.take(16n, h), e), V.len_take(16n, h)) case Inr{e}: L.subst(List<&2, U32>, l => {Nat.is_le(V.len(l), 16n) == True{} : Bool}, Li.take(16n, gg(h)), Li.freeze(h), Equal.sym(List<&2, U32>, Li.freeze(h), Li.take(16n, gg(h)), e), V.len_take(16n, gg(h)))def freeze_len(one, h1, h, hh): fz_len_o(h, which_c(one, h1, h, hh, Nat.is_eq(qq(h), 0n), {==}))# the value: the low 128 bits of h mod p# lgv == low(k, d) when x = lgv + 2^k tgv with lgv < 2^k and x = d + 2^k s2,# for a symbolic k (so that no check unfolds low(128, _) level by level).law elg_k: for +k: Nat for +x: Nat for +lgv: Nat for +tgv: Nat for +d: Nat for +s2: Nat for +hs: {x == Nat.add(lgv, C.shift(k, tgv)) : Nat} for +hf: {C.fits(k, lgv) == True{} : Bool} for +hx: {x == Nat.add(d, C.shift(k, s2)) : Nat} {lgv == C.low(k, d) : Nat}def elg_k(k, x, lgv, tgv, d, s2, hs, hf, hx): A.tr(lgv, C.low(k, x), C.low(k, d), A.sy(C.low(k, x), lgv, A.tr(C.low(k, x), C.low(k, Nat.add(lgv, C.shift(k, tgv))), lgv, Equal.cong(Nat, Nat, z => C.low(k, z), x, Nat.add(lgv, C.shift(k, tgv)), hs), WW.low_u(k, lgv, tgv, hf))), A.tr(C.low(k, x), C.low(k, Nat.add(d, C.shift(k, s2))), C.low(k, d), Equal.cong(Nat, Nat, z => C.low(k, z), x, Nat.add(d, C.shift(k, s2)), hx), WW.low_add_shift(k, d, s2)))law fin_k: for +k: Nat for +a: Nat for +b: Nat for +c: Nat for +m: Nat for +e1: {a == b : Nat} for +e2: {b == C.low(k, c) : Nat} for +e3: {m == c : Nat} {a == C.low(k, m) : Nat}def fin_k(k, a, b, c, m, e1, e2, e3): A.tr(a, b, C.low(k, m), e1, A.tr(b, C.low(k, c), C.low(k, m), e2, Equal.cong(Nat, Nat, z => C.low(k, z), c, m, A.sy(m, c, e3))))law fe_k: for +k: Nat for +x: Nat for +lgv: Nat for +tgv: Nat for +d: Nat for +s2: Nat for +a: Nat for +m: Nat for +hs: {x == Nat.add(lgv, C.shift(k, tgv)) : Nat} for +hf: {C.fits(k, lgv) == True{} : Bool} for +hx: {x == Nat.add(d, C.shift(k, s2)) : Nat} for +e1: {a == lgv : Nat} for +e3: {m == d : Nat} {a == C.low(k, m) : Nat}def fe_k(k, x, lgv, tgv, d, s2, a, m, hs, hf, hx, e1, e3): fin_k(k, a, lgv, d, m, e1, elg_k(k, x, lgv, tgv, d, s2, hs, hf, hx), e3)def frz_c(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +h5: {Nat.add(1n+bp, 5n) == C.shift(130n, one) : Nat}, +h: List<&2, U32>, +hh: {ST.inv(h) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(qq(h), 0n) == c : Bool}) -> {V.ev(Li.freeze(h)) == C.low(128n, Nat.mod(V.ev(h), 1n+bp)) : Nat}: match c: case True{}: +pp = {1n+bp : Nat} +x = Nat.add(V.ev(h), 5n) +lh = V.ev(Li.take(16n, h)) +vt = V.v(Li.hd0(Li.skip(16n, h))) +ef = Equal.cong(List<&2, U32>, Nat, l => V.ev(l), Li.freeze(h), Li.take(16n, h), which0(one, h1, h, hh, hc)) +lx = A.lt_subst(x, C.shift(130n, one), Nat.add(pp, 5n), A.sy(Nat.add(pp, 5n), C.shift(130n, one), h5), WW.lt_one(130n, one, h1, x, hc)) +lp = A.btrue(Nat.is_lt(V.ev(h), pp), Nat.is_lt(x, Nat.add(pp, 5n)), Equal.sym(Bool, Nat.is_lt(x, Nat.add(pp, 5n)), Nat.is_lt(V.ev(h), pp), WW.lt_cancel_r(V.ev(h), pp, 5n)), lx) +em = NR.mod_of(0n, bp, V.ev(h), lp) +flh = WW.fits_one(128n, one, h1, lh, A.lt_subst(lh, V.pos(V.len(Li.take(16n, h)), one), V.pos(16n, one), Equal.cong(Nat, Nat, z => V.pos(z, one), V.len(Li.take(16n, h)), 16n, len16(h, hh)), V.ev_lt(Li.take(16n, h), one, h1, V.fit_take(16n, h, 8n, fith(h, hh))))) +el = A.tr(C.low(128n, V.ev(h)), C.low(128n, Nat.add(lh, V.pos(16n, vt))), lh, Equal.cong(Nat, Nat, z => C.low(128n, z), V.ev(h), Nat.add(lh, V.pos(16n, vt)), hsplit(h, hh)), WW.low_u(128n, lh, vt, flh)) A.tr(V.ev(Li.freeze(h)), lh, C.low(128n, Nat.mod(V.ev(h), pp)), ef, A.sy(C.low(128n, Nat.mod(V.ev(h), pp)), lh, A.tr(C.low(128n, Nat.mod(V.ev(h), pp)), C.low(128n, V.ev(h)), lh, Equal.cong(Nat, Nat, z => C.low(128n, z), Nat.mod(V.ev(h), pp), V.ev(h), em), el))) case False{}: +pp = {1n+bp : Nat} +s = C.shift(130n, one) +u = V.pos(16n, one) +x = Nat.add(V.ev(h), 5n) +d = C.low(130n, x) +q = qq(h) +ef = Equal.cong(List<&2, U32>, Nat, l => V.ev(l), Li.freeze(h), Li.take(16n, gg(h)), which1(one, h1, h, hh, hc)) +eq1 = qone(one, h1, h, hh, hc) +es = A.tr(C.shift(130n, q), Nat.mul(q, s), s, WW.shift_mul_one(130n, one, h1, q), A.tr(Nat.mul(q, s), Nat.mul(1n, s), s, Equal.cong(Nat, Nat, z => Nat.mul(z, s), q, 1n, eq1), AR.one_mul(s))) +ex = A.tr(x, Nat.add(d, C.shift(130n, q)), Nat.add(d, s), WW.low_high(130n, x), WM.cong_r(d, C.shift(130n, q), s, es)) +ex2 = A.tr(Nat.add(V.ev(h), 5n), Nat.add(d, Nat.add(pp, 5n)), Nat.add(Nat.add(d, pp), 5n), A.tr(x, Nat.add(d, s), Nat.add(d, Nat.add(pp, 5n)), ex, WM.cong_r(d, s, Nat.add(pp, 5n), A.sy(Nat.add(pp, 5n), s, h5))), A.sy(Nat.add(Nat.add(d, pp), 5n), Nat.add(d, Nat.add(pp, 5n)), N.add_assoc(d, pp, 5n))) +eh = UA.add_cancel_r(V.ev(h), Nat.add(d, pp), 5n, ex2) # d < 2^128 + 5 <= p +l1 = N.lt_add_r2(V.ev(h), Nat.add(u, s), 5n, hlt(one, h1, h, hh)) +e1 = A.tr(Nat.add(Nat.add(u, s), 5n), Nat.add(u, Nat.add(s, 5n)), Nat.add(Nat.add(u, 5n), s), N.add_assoc(u, s, 5n), A.tr(Nat.add(u, Nat.add(s, 5n)), Nat.add(u, Nat.add(5n, s)), Nat.add(Nat.add(u, 5n), s), WM.cong_r(u, Nat.add(s, 5n), Nat.add(5n, s), N.add_comm(s, 5n)), A.sy(Nat.add(Nat.add(u, 5n), s), Nat.add(u, Nat.add(5n, s)), N.add_assoc(u, 5n, s)))) +l2 = A.lt_substl(x, Nat.add(d, s), Nat.add(Nat.add(u, 5n), s), ex, A.lt_subst(x, Nat.add(Nat.add(u, s), 5n), Nat.add(Nat.add(u, 5n), s), e1, l1)) +ld = A.btrue(Nat.is_lt(d, Nat.add(u, 5n)), Nat.is_lt(Nat.add(d, s), Nat.add(Nat.add(u, 5n), s)), Equal.sym(Bool, Nat.is_lt(Nat.add(d, s), Nat.add(Nat.add(u, 5n), s)), Nat.is_lt(d, Nat.add(u, 5n)), WW.lt_cancel_r(d, Nat.add(u, 5n), s)), l2) +l9 = N.lt_le_trans(Nat.add(u, 9n), Nat.add(u, u), s, N.lt_add_left(9n, u, u, N.lt_le_trans(9n, 16n, u, {==}, u16(one, h1))), uu(one, h1)) +l9b = A.lt_substl(Nat.add(u, 9n), Nat.add(Nat.add(u, 4n), 5n), Nat.add(pp, 5n), A.sy(Nat.add(Nat.add(u, 4n), 5n), Nat.add(u, 9n), N.add_assoc(u, 4n, 5n)), A.lt_subst(Nat.add(u, 9n), s, Nat.add(pp, 5n), A.sy(Nat.add(pp, 5n), s, h5), l9)) +l4 = A.btrue(Nat.is_lt(Nat.add(u, 4n), pp), Nat.is_lt(Nat.add(Nat.add(u, 4n), 5n), Nat.add(pp, 5n)), Equal.sym(Bool, Nat.is_lt(Nat.add(Nat.add(u, 4n), 5n), Nat.add(pp, 5n)), Nat.is_lt(Nat.add(u, 4n), pp), WW.lt_cancel_r(Nat.add(u, 4n), pp, 5n)), l9b) +l5 = A.le_substl(1n+Nat.add(u, 4n), Nat.add(u, 5n), pp, A.sy(Nat.add(u, 5n), 1n+Nat.add(u, 4n), N.add_succ(u, 4n)), N.lt_succ_le_succ(Nat.add(u, 4n), pp, l4)) +ldp = N.lt_le_trans(d, Nat.add(u, 5n), pp, ld, l5) +em = A.tr(Nat.mod(V.ev(h), pp), Nat.mod(Nat.add(Nat.mul(1n, pp), d), pp), d, Equal.cong(Nat, Nat, z => Nat.mod(z, pp), V.ev(h), Nat.add(Nat.mul(1n, pp), d), A.tr(V.ev(h), Nat.add(d, pp), Nat.add(Nat.mul(1n, pp), d), eh, A.tr(Nat.add(d, pp), Nat.add(pp, d), Nat.add(Nat.mul(1n, pp), d), N.add_comm(d, pp), WM.cong_l(pp, Nat.mul(1n, pp), d, A.sy(Nat.mul(1n, pp), pp, AR.one_mul(pp)))))), NR.mod_of(1n, bp, d, ldp)) fe_k(128n, x, lg(h), tg(h), d, C.shift(2n, one), V.ev(Li.freeze(h)), Nat.mod(V.ev(h), pp), gsplit(one, h1, h, hh), flg(one, h1, h), ex, ef, em)law freeze_ev: for +one: Nat for +h1: {one == 1n : Nat} for +bp: Nat for +h5: {Nat.add(1n+bp, 5n) == C.shift(130n, one) : Nat} for +h: List<&2, U32> for +hh: {ST.inv(h) == True{} : Bool} {V.ev(Li.freeze(h)) == C.low(128n, Nat.mod(V.ev(h), 1n+bp)) : Nat}def freeze_ev(one, h1, bp, h5, h, hh): frz_c(one, h1, bp, h5, h, hh, Nat.is_eq(qq(h), 0n), {==})# ---- the tag bytes ----law bytes_le: for +n: Nat for +ds: List<&2, U32> for +u: U32 for +k: Nat for +j: Nat for +hj: {Nat.is_le(Nat.add(9n, j), 32n) == True{} : Bool} for +hd: {V.fit_all(ds, Nat.add(8n, j)) == True{} : Bool} for +hu: {C.fits(Nat.add(8n, j), V.v(u)) == True{} : Bool} {Li.bytes(n, ds, u) == R.le_bytes(n, Nat.add(Nat.add(V.v(u), V.ev(ds)), V.pos(n, k))) : List<&2, U32>}def bytes_le(n, ds, u, k, j, hj, hd, hu): match n: case 0n: {==} case 1n+m: +h = Li.hd0(ds) +s = U32.add(u, h) +vs = V.v(s) +u2 = U32.shrn(s, 8n) +et = V.ev(Li.tl(ds)) +pk = V.pos(m, k) +y = Nat.add(Nat.add(V.v(u), V.ev(ds)), C.shift(8n, pk)) +y2 = Nat.add(vs, C.shift(8n, Nat.add(et, pk))) +es = V.step_ev(ds, u, j, hj, hd, hu) +ey = A.tr(y, Nat.add(Nat.add(V.v(u), Nat.add(V.v(h), C.shift(8n, et))), C.shift(8n, pk)), y2, WM.cong_l(Nat.add(V.v(u), V.ev(ds)), Nat.add(V.v(u), Nat.add(V.v(h), C.shift(8n, et))), C.shift(8n, pk), WM.cong_r(V.v(u), V.ev(ds), Nat.add(V.v(h), C.shift(8n, et)), V.hd_tl_ev(ds))), A.tr(Nat.add(Nat.add(V.v(u), Nat.add(V.v(h), C.shift(8n, et))), C.shift(8n, pk)), Nat.add(Nat.add(Nat.add(V.v(u), V.v(h)), C.shift(8n, et)), C.shift(8n, pk)), y2, WM.cong_l(Nat.add(V.v(u), Nat.add(V.v(h), C.shift(8n, et))), Nat.add(Nat.add(V.v(u), V.v(h)), C.shift(8n, et)), C.shift(8n, pk), A.sy(Nat.add(Nat.add(V.v(u), V.v(h)), C.shift(8n, et)), Nat.add(V.v(u), Nat.add(V.v(h), C.shift(8n, et))), N.add_assoc(V.v(u), V.v(h), C.shift(8n, et)))), A.tr(Nat.add(Nat.add(Nat.add(V.v(u), V.v(h)), C.shift(8n, et)), C.shift(8n, pk)), Nat.add(Nat.add(V.v(u), V.v(h)), C.shift(8n, Nat.add(et, pk))), y2, V.sh3(Nat.add(V.v(u), V.v(h)), et, pk), WM.cong_l(Nat.add(V.v(u), V.v(h)), vs, C.shift(8n, Nat.add(et, pk)), A.sy(vs, Nat.add(V.v(u), V.v(h)), es))))) +elo = WW.low_add_shift(8n, vs, Nat.add(et, pk)) +ehi = A.tr(C.high(8n, y2), Nat.add(C.high(8n, vs), Nat.add(et, pk)), Nat.add(Nat.add(V.v(u2), et), pk), WW.high_add_shift(8n, vs, Nat.add(et, pk)), A.tr(Nat.add(C.high(8n, vs), Nat.add(et, pk)), Nat.add(V.v(u2), Nat.add(et, pk)), Nat.add(Nat.add(V.v(u2), et), pk), WM.cong_l(C.high(8n, vs), V.v(u2), Nat.add(et, pk), A.sy(V.v(u2), C.high(8n, vs), SHN.shrn_high(s, 8n))), A.sy(Nat.add(Nat.add(V.v(u2), et), pk), Nat.add(V.v(u2), Nat.add(et, pk)), N.add_assoc(V.v(u2), et, pk)))) +lo8 = C.low(8n, vs) +eb = U3.injective(U32.and(s, 255), U32.from_nat(lo8), A.tr(V.v(U32.and(s, 255)), lo8, V.v(U32.from_nat(lo8)), FB.andm(s, 8n, 255, {==}), A.sy(V.v(U32.from_nat(lo8)), lo8, U3.to_nat_from_nat(lo8, 8n, {==}, WW.low_lt(8n, vs))))) +ih = bytes_le(m, Li.tl(ds), u2, k, j, hj, V.tl_fit(ds, Nat.add(8n, j), hd), V.next_fit(ds, u, j, hj, hd, hu)) Equal.trans(List<&2, U32>, U32.and(s, 255) <> Li.bytes(m, Li.tl(ds), u2), R.le_bytes(1n+m, y2), R.le_bytes(1n+m, y), Equal.trans(List<&2, U32>, U32.and(s, 255) <> Li.bytes(m, Li.tl(ds), u2), U32.from_nat(lo8) <> R.le_bytes(m, Nat.add(Nat.add(V.v(u2), et), pk)), R.le_bytes(1n+m, y2), Equal.trans(List<&2, U32>, U32.and(s, 255) <> Li.bytes(m, Li.tl(ds), u2), U32.from_nat(lo8) <> Li.bytes(m, Li.tl(ds), u2), U32.from_nat(lo8) <> R.le_bytes(m, Nat.add(Nat.add(V.v(u2), et), pk)), Equal.cong(U32, List<&2, U32>, z => z <> Li.bytes(m, Li.tl(ds), u2), U32.and(s, 255), U32.from_nat(lo8), eb), Equal.cong(List<&2, U32>, List<&2, U32>, z => U32.from_nat(lo8) <> z, Li.bytes(m, Li.tl(ds), u2), R.le_bytes(m, Nat.add(Nat.add(V.v(u2), et), pk)), ih)), Equal.trans(List<&2, U32>, U32.from_nat(lo8) <> R.le_bytes(m, Nat.add(Nat.add(V.v(u2), et), pk)), U32.from_nat(C.low(8n, y2)) <> R.le_bytes(m, Nat.add(Nat.add(V.v(u2), et), pk)), R.le_bytes(1n+m, y2), Equal.cong(Nat, List<&2, U32>, z => U32.from_nat(z) <> R.le_bytes(m, Nat.add(Nat.add(V.v(u2), et), pk)), lo8, C.low(8n, y2), A.sy(C.low(8n, y2), lo8, elo)), Equal.cong(Nat, List<&2, U32>, z => U32.from_nat(C.low(8n, y2)) <> R.le_bytes(m, z), Nat.add(Nat.add(V.v(u2), et), pk), C.high(8n, y2), A.sy(C.high(8n, y2), Nat.add(Nat.add(V.v(u2), et), pk), ehi)))), Equal.cong(Nat, List<&2, U32>, z => R.le_bytes(1n+m, z), y2, y, A.sy(y, y2, ey)))# bytes_le with the target value rewritten, for any n (so that the# rewrite does not unfold le_bytes n levels on both sides).law bytes_le_to: for +n: Nat for +ds: List<&2, U32> for +k: Nat for +t: Nat for +hb: {Li.bytes(n, ds, 0) == R.le_bytes(n, Nat.add(Nat.add(V.v(0), V.ev(ds)), V.pos(n, k))) : List<&2, U32>} for +ht: {Nat.add(V.ev(ds), V.pos(n, k)) == t : Nat} {Li.bytes(n, ds, 0) == R.le_bytes(n, t) : List<&2, U32>}def bytes_le_to(n, ds, k, t, hb, ht): Equal.trans(List<&2, U32>, Li.bytes(n, ds, 0), R.le_bytes(n, Nat.add(V.ev(ds), V.pos(n, k))), R.le_bytes(n, t), hb, Equal.cong(Nat, List<&2, U32>, z => R.le_bytes(n, z), Nat.add(V.ev(ds), V.pos(n, k)), t, ht))# the tag: (h mod p + s) mod 2^128 as 16 byteslaw tag_eq: for +one: Nat for +h1: {one == 1n : Nat} for +bp: Nat for +h5: {Nat.add(1n+bp, 5n) == C.shift(130n, one) : Nat} for +h: List<&2, U32> for +hh: {ST.inv(h) == True{} : Bool} for +s: List<&2, U32> for +hs: {V.fit_all(s, 8n) == True{} : Bool} {Li.bytes(16n, Li.add(Li.freeze(h), s), 0) == R.le_bytes(16n, Nat.add(Nat.mod(V.ev(h), 1n+bp), V.ev(s))) : List<&2, U32>}def tag_eq(one, h1, bp, h5, h, hh, s, hs): +s8 = C.shift(8n, one) +s9 = C.shift(9n, one) +fz = Li.freeze(h) +a = Nat.mod(V.ev(h), 1n+bp) +lo = C.low(128n, a) +kk = C.high(128n, a) +ds = Li.add(fz, s) +hf = freeze_fit(one, h1, h, hh) +hf1 = ST.s8fit(one, h1) +ed = V.add_ev(fz, s, s8, s8, V.fit_le(fz, 8n, one, h1, hf), V.fit_le(s, 8n, one, h1, hs), hf1) +l10 = A.lt_substl(s9, Nat.add(s8, s8), Nat.double(s9), NA.double_self(s8), lt_dbl(s9, A.one_le_shift(9n, one, h1))) +hd = V.le_fit(ds, Nat.add(s8, s8), 10n, one, h1, l10, V.add_le(fz, s, s8, s8, V.fit_le(fz, 8n, one, h1, hf), V.fit_le(s, 8n, one, h1, hs), hf1)) +bl = bytes_le(16n, ds, 0, kk, 2n, {==}, hd, {==}) # ev ds + 2^128 kk == a + ev s +e1 = A.tr(Nat.add(V.ev(ds), V.pos(16n, kk)), Nat.add(Nat.add(lo, V.ev(s)), V.pos(16n, kk)), Nat.add(a, V.ev(s)), WM.cong_l(V.ev(ds), Nat.add(lo, V.ev(s)), V.pos(16n, kk), A.tr(V.ev(ds), Nat.add(V.ev(fz), V.ev(s)), Nat.add(lo, V.ev(s)), ed, WM.cong_l(V.ev(fz), lo, V.ev(s), freeze_ev(one, h1, bp, h5, h, hh)))), A.tr(Nat.add(Nat.add(lo, V.ev(s)), V.pos(16n, kk)), Nat.add(Nat.add(lo, V.pos(16n, kk)), V.ev(s)), Nat.add(a, V.ev(s)), A.tr(Nat.add(Nat.add(lo, V.ev(s)), V.pos(16n, kk)), Nat.add(lo, Nat.add(V.ev(s), V.pos(16n, kk))), Nat.add(Nat.add(lo, V.pos(16n, kk)), V.ev(s)), N.add_assoc(lo, V.ev(s), V.pos(16n, kk)), ST.rot(lo, V.ev(s), V.pos(16n, kk))), WM.cong_l(Nat.add(lo, V.pos(16n, kk)), a, V.ev(s), A.sy(a, Nat.add(lo, V.pos(16n, kk)), WW.low_high(128n, a))))) bytes_le_to(16n, ds, kk, Nat.add(a, V.ev(s)), bl, e1)# tag_eq through Li.fin (the implementation's entry point).law fin_eq: for +one: Nat for +h1: {one == 1n : Nat} for +bp: Nat for +h5: {Nat.add(1n+bp, 5n) == C.shift(130n, one) : Nat} for +h: List<&2, U32> for +hh: {ST.inv(h) == True{} : Bool} for +s: List<&2, U32> for +hs: {V.fit_all(s, 8n) == True{} : Bool} {Li.fin(h, s) == R.le_bytes(16n, Nat.add(Nat.mod(V.ev(h), 1n+bp), V.ev(s))) : List<&2, U32>}def fin_eq(one, h1, bp, h5, h, hh, s, hs): match s: case Nil{}: tag_eq(one, h1, bp, h5, h, hh, Nil{}, hs) case y <> ys: tag_eq(one, h1, bp, h5, h, hh, y <> ys, hs)