def c1_d

bend-osdev-acpi@0.1.1.0 · PROOF.bend:2392

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
import bend-osdev-acpi@0.1.1.0/error.bend as E
import bend-osdev-acpi@0.1.1.0/header.bend as H
import bend-osdev-acpi@0.1.1.0/checksum.bend as C

2392def c1_d(+m: Maybe<&2, U32>, +o: B.Octets, +e: {Result.is_done(&2, &2, E.AcpiError, B.Octets, H.sdt.c1(m, o)) == True{} : Bool}) -> {C.AcpiChecksum.ok(B.Octets.take(U32.to_nat(Maybe.default(&2, U32, m, 4294967295)), o)) == True{} : Bool}:
2393  match m:
2394    case None{}:
2395      Empty.absurd({C.AcpiChecksum.ok(B.Octets.take(U32.to_nat(Maybe.default(&2, U32, None{}, 4294967295)), o)) == True{} : Bool}, ft_absurd(e))
2396    case Some{l}:
2397      c2_d(Bool.and(Nat.is_le(36n, U32.to_nat(l)), Nat.is_le(U32.to_nat(l), B.Octets.len(o))), l, o, e)