~/jendhub

def off.llen_be64

bend-osdev-bytes@0.1.1.0 · PROOF.bend:1078

import bend-osdev-bytes@0.1.1.0/PROOF.bend as PROOF
import Base
import bend-osdev-word64@0.1.1.0/word64.bend as W
import bend-osdev-bytes@0.1.1.0/bytes.bend as B

1078def off.llen_be64(+v: W.W64) -> {B.len(B.be64(v)) == 8n : Nat}:
1079  Equal.trans(Nat, B.len(B.be64(v)), Nat.add(B.len(B.be32(W.W64.hi(v))), B.len(B.be32(W.W64.lo(v)))), 8n, off.llen_app(B.be32(W.W64.hi(v)), B.be32(W.W64.lo(v))), off.add_be32(W.W64.hi(v), W.W64.lo(v)))

Uses (11)

Used by (1)