law fin_eq

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

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

558# tag_eq through Li.fin (the implementation's entry point).
559law fin_eq:
560  for +one: Nat
561  for +h1: {one == 1n : Nat}
562  for +bp: Nat
563  for +h5: {Nat.add(1n+bp, 5n) == C.shift(130n, one) : Nat}
564  for +h: List<&2, U32>
565  for +hh: {ST.inv(h) == True{} : Bool}
566  for +s: List<&2, U32>
567  for +hs: {V.fit_all(s, 8n) == True{} : Bool}
568  {Li.fin(h, s) == R.le_bytes(16n, Nat.add(Nat.mod(V.ev(h), 1n+bp), V.ev(s))) : List<&2, U32>}