law absorb_ok

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/mac.bend:207

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/poly1305.bend as P
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/value.bend as V
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/step.bend as ST

207law absorb_ok:
208  for +one: Nat
209  for +h1: {one == 1n : Nat}
210  for +bp: Nat
211  for +h5: {Nat.add(1n+bp, 5n) == C.shift(130n, one) : Nat}
212  for +fuel: Nat
213  for +msg: List<&2, U32>
214  for +r: List<&2, U32>
215  for +h: List<&2, U32>
216  for +a: Nat
217  for +hrl: {V.len(r) == 16n : Nat}
218  for +hrf: {V.fit_all(r, 8n) == True{} : Bool}
219  for +hh: {ST.inv(h) == True{} : Bool}
220  for +ha: {Nat.mod(V.ev(h), 1n+bp) == a : Nat}
221  {Nat.mod(V.ev(P.absorb(fuel, msg, r, h)), 1n+bp) == R.absorb(R.blocks(fuel, msg), V.ev(r), a) : Nat}