def ckw.l4

bend-osdev-acpi@0.1.2.0 · PROOF_whole.bend:59

import Base
import bend-osdev-bytes@0.1.1.1/bytes.bend as B
import bend-osdev-bytes@0.1.1.1/LAWS.bend as BL

59def ckw.l4(+v: U32) -> {Nat.is_le(Nat.add(0n, 4n), B.Octets.len(B.Octets.le32(v))) == True{} : Bool}:
60  %Equal.sym(Nat, B.Octets.len(B.Octets.le32(v)), 4n, BL.octets_len_le32(v)) : {Nat.is_le(Nat.add(0n, 4n), _) == True{} : Bool}
61  {==}