def ckp.hdd

bend-osdev-acpi@0.1.2.0 · PROOF_checksum.bend:213

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

213def ckp.hdd(+i: Nat, +o: B.Octets, +h: {Nat.is_lt(i, B.Octets.len(o)) == True{} : Bool}) -> {Nat.is_le(1n, B.Octets.len(B.Octets.drop(i, o))) == True{} : Bool}:
214  %Equal.sym(Nat, B.Octets.len(B.Octets.drop(i, o)), Nat.sub(B.Octets.len(o), i), BL.octets_len_drop(i, o)) : {Nat.is_le(1n, _) == True{} : Bool}
215  ckp.lt_sub(i, B.Octets.len(o), h)