~/jendhub

def off.llen_le64

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

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

1075def off.llen_le64(+v: W.W64) -> {B.len(B.le64(v)) == 8n : Nat}:
1076  Equal.trans(Nat, B.len(B.le64(v)), Nat.add(B.len(B.le32(W.W64.lo(v))), B.len(B.le32(W.W64.hi(v)))), 8n, off.llen_app(B.le32(W.W64.lo(v)), B.le32(W.W64.hi(v))), off.add_le32(W.W64.lo(v), W.W64.hi(v)))

Uses (11)

Used by (1)