law absorb_inv

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

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

223law absorb_inv:
224  for +one: Nat
225  for +h1: {one == 1n : Nat}
226  for +fuel: Nat
227  for +msg: List<&2, U32>
228  for +r: List<&2, U32>
229  for +h: List<&2, U32>
230  for +hrl: {V.len(r) == 16n : Nat}
231  for +hrf: {V.fit_all(r, 8n) == True{} : Bool}
232  for +hh: {ST.inv(h) == True{} : Bool}
233  {ST.inv(P.absorb(fuel, msg, r, h)) == True{} : Bool}