def mask_nil

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/mac/hmac.bend:40

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/mac.bend as MAC
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/hmac.bend as Spec

40# Past the end of the key, mask emits 0 XOR pad.
41def mask_nil(+n: Nat, +pad: U32, +hp: {U32.xor(0, pad) == pad : U32}) -> {MAC.mask(Nil{}, n, pad) == Spec.xor_pad(List.replicate(U32, n, 0), pad) : List<&2, U32>}:
42  match n:
43    case 0n:
44      {==}
45    case 1n+ +p:
46      %hp : {_ <> MAC.mask(Nil{}, p, pad) == U32.xor(0, pad) <> Spec.xor_pad(List.replicate(U32, p, 0), pad) : List<&2, U32>}
47      %mask_nil(p, pad, hp) : {U32.xor(0, pad) <> MAC.mask(Nil{}, p, pad) == U32.xor(0, pad) <> _ : List<&2, U32>}
48      {==}