law bytes_le

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/final.bend:462

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/poly1305.bend as R
import bend-collections-laws-crypto@1.0.0.0/src/crypto/poly1305/limbs.bend as Li
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/value.bend as V

462law bytes_le:
463  for +n: Nat
464  for +ds: List<&2, U32>
465  for +u: U32
466  for +k: Nat
467  for +j: Nat
468  for +hj: {Nat.is_le(Nat.add(9n, j), 32n) == True{} : Bool}
469  for +hd: {V.fit_all(ds, Nat.add(8n, j)) == True{} : Bool}
470  for +hu: {C.fits(Nat.add(8n, j), V.v(u)) == True{} : Bool}
471  {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>}