law fe_k

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

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C

386law fe_k:
387  for +k: Nat
388  for +x: Nat
389  for +lgv: Nat
390  for +tgv: Nat
391  for +d: Nat
392  for +s2: Nat
393  for +a: Nat
394  for +m: Nat
395  for +hs: {x == Nat.add(lgv, C.shift(k, tgv)) : Nat}
396  for +hf: {C.fits(k, lgv) == True{} : Bool}
397  for +hx: {x == Nat.add(d, C.shift(k, s2)) : Nat}
398  for +e1: {a == lgv : Nat}
399  for +e3: {m == d : Nat}
400  {a == C.low(k, m) : Nat}