def w8be_len

bend-osdev-hashes@0.1.0.0 · PROOF.bend:92

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-hashes@0.1.0.0/hashes.bend as Hs

92def w8be_len(x: Hs.HsW8) -> {B.Octets.len(Hs.HsW8.be(x)) == 32n : Nat}:
93  match x:
94    case Hs.HsW8{+a0, +a1, +a2, +a3, +a4, +a5, +a6, +a7}:
95      %Equal.sym(Nat, B.Octets.len(B.Octets.of_list(B.append(B.be32(a0), B.append(B.be32(a1), B.append(B.be32(a2), B.append(B.be32(a3), B.append(B.be32(a4), B.append(B.be32(a5), B.append(B.be32(a6), B.be32(a7)))))))))), B.len(B.append(B.be32(a0), B.append(B.be32(a1), B.append(B.be32(a2), B.append(B.be32(a3), B.append(B.be32(a4), B.append(B.be32(a5), B.append(B.be32(a6), B.be32(a7))))))))), octets_len_of(B.append(B.be32(a0), B.append(B.be32(a1), B.append(B.be32(a2), B.append(B.be32(a3), B.append(B.be32(a4), B.append(B.be32(a5), B.append(B.be32(a6), B.be32(a7)))))))))) : {_ == 32n : Nat}
96      w8be_len_list(a0, a1, a2, a3, a4, a5, a6, a7)