law bytes_le_to

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

import Base
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

509# bytes_le with the target value rewritten, for any n (so that the
510# rewrite does not unfold le_bytes n levels on both sides).
511law bytes_le_to:
512  for +n: Nat
513  for +ds: List<&2, U32>
514  for +k: Nat
515  for +t: Nat
516  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>}
517  for +ht: {Nat.add(V.ev(ds), V.pos(n, k)) == t : Nat}
518  {Li.bytes(n, ds, 0) == R.le_bytes(n, t) : List<&2, U32>}