def pk.fill_len

bend-osdev-pkcs7@0.1.0.0 · PROOF.bend:179

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
import bend-osdev-pkcs7@0.1.0.0/pkcs7.bend as P

179def pk.fill_len(+n: Nat, +v: U32) -> {B.len(P.pkcs7.fill(n, v)) == n : Nat}:
180  match n:
181    case 0n:
182      {==}
183    case 1n+p:
184      %pk.fill_len(p, v) : {1n+B.len(P.pkcs7.fill(p, v)) == 1n+_ : Nat}
185      {==}