PROOF.hdr_rt: def of bend-osdev-acpi@0.1.1.0
Import: import bend-osdev-acpi@0.1.1.0/PROOF.bend as PROOF
Lines 2298-2323 of bend-osdev-acpi@0.1.1.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&start_line=2298&end_line=2323

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

def hdr_rt(+s: B.Octets, +l: U32, +r: U32, +c: U32, +o: B.Octets, +t: B.Octets, +orv: U32, +ci: B.Octets, +cr: U32, +sig4: {B.Octets.len(s) == 4n : Nat}, +oem6: {B.Octets.len(o) == 6n : Nat}, +tid8: {B.Octets.len(t) == 8n : Nat}, +cid4: {B.Octets.len(ci) == 4n : Nat}, +rev8: {B.byte(r) == r : U32}, +ck8: {B.byte(c) == c : U32}) -> {H.AcpiHeader.decode(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr})) == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}:
  %sig4 : {H.hd.d1(B.Octets.split_at(_, B.Octets.append(s, B.Octets.append(B.Octets.le32(l), B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))))))))), H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr})) == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
  %Equal.sym(Maybe<&2, B.OctetsSplit>, B.Octets.split_at(B.Octets.len(s), B.Octets.append(s, B.Octets.append(B.Octets.le32(l), B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))))))))), Some{B.OctetsSplit{s, B.Octets.append(B.Octets.le32(l), B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr))))))))}}, BL.octets_split_at_append(s, B.Octets.append(B.Octets.le32(l), B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))))))))) : {H.hd.d1(_, H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr})) == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
  %le32_len(l) : {H.hd.d2(B.Octets.split_at(_, B.Octets.append(B.Octets.le32(l), B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr))))))))), H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), s) == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
  %Equal.sym(Maybe<&2, B.OctetsSplit>, B.Octets.split_at(B.Octets.len(B.Octets.le32(l)), B.Octets.append(B.Octets.le32(l), B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr))))))))), Some{B.OctetsSplit{B.Octets.le32(l), B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))))))}}, BL.octets_split_at_append(B.Octets.le32(l), B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr))))))))) : {H.hd.d2(_, H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), s) == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
  %byte_len(r) : {H.hd.d3(B.Octets.split_at(_, B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))))))), H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), s, H.hd.u32(B.Octets.le32(l))) == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
  %Equal.sym(Maybe<&2, B.OctetsSplit>, B.Octets.split_at(B.Octets.len(H.hd.byte(r)), B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))))))), Some{B.OctetsSplit{H.hd.byte(r), B.Octets.append(H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr))))))}}, BL.octets_split_at_append(H.hd.byte(r), B.Octets.append(H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))))))) : {H.hd.d3(_, H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), s, H.hd.u32(B.Octets.le32(l))) == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
  %byte_len(c) : {H.hd.d4(B.Octets.split_at(_, B.Octets.append(H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr))))))), H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), s, H.hd.u32(B.Octets.le32(l)), H.hd.u8(H.hd.byte(r))) == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
  %Equal.sym(Maybe<&2, B.OctetsSplit>, B.Octets.split_at(B.Octets.len(H.hd.byte(c)), B.Octets.append(H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr))))))), Some{B.OctetsSplit{H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))))}}, BL.octets_split_at_append(H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr))))))) : {H.hd.d4(_, H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), s, H.hd.u32(B.Octets.le32(l)), H.hd.u8(H.hd.byte(r))) == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
  %oem6 : {H.hd.d5(B.Octets.split_at(_, B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))))), H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), s, H.hd.u32(B.Octets.le32(l)), H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c))) == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
  %Equal.sym(Maybe<&2, B.OctetsSplit>, B.Octets.split_at(B.Octets.len(o), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))))), Some{B.OctetsSplit{o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr))))}}, BL.octets_split_at_append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))))) : {H.hd.d5(_, H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), s, H.hd.u32(B.Octets.le32(l)), H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c))) == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
  %tid8 : {H.hd.d6(B.Octets.split_at(_, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr))))), H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), s, H.hd.u32(B.Octets.le32(l)), H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c)), o) == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
  %Equal.sym(Maybe<&2, B.OctetsSplit>, B.Octets.split_at(B.Octets.len(t), B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr))))), Some{B.OctetsSplit{t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))}}, BL.octets_split_at_append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr))))) : {H.hd.d6(_, H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), s, H.hd.u32(B.Octets.le32(l)), H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c)), o) == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
  %le32_len(orv) : {H.hd.d7(B.Octets.split_at(_, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))), H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), s, H.hd.u32(B.Octets.le32(l)), H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c)), o, t) == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
  %Equal.sym(Maybe<&2, B.OctetsSplit>, B.Octets.split_at(B.Octets.len(B.Octets.le32(orv)), B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))), Some{B.OctetsSplit{B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr))}}, BL.octets_split_at_append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))) : {H.hd.d7(_, H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), s, H.hd.u32(B.Octets.le32(l)), H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c)), o, t) == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
  %cid4 : {H.hd.d8(B.Octets.split_at(_, B.Octets.append(ci, B.Octets.le32(cr))), H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), s, H.hd.u32(B.Octets.le32(l)), H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c)), o, t, H.hd.u32(B.Octets.le32(orv))) == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
  %Equal.sym(Maybe<&2, B.OctetsSplit>, B.Octets.split_at(B.Octets.len(ci), B.Octets.append(ci, B.Octets.le32(cr))), Some{B.OctetsSplit{ci, B.Octets.le32(cr)}}, BL.octets_split_at_append(ci, B.Octets.le32(cr))) : {H.hd.d8(_, H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), s, H.hd.u32(B.Octets.le32(l)), H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c)), o, t, H.hd.u32(B.Octets.le32(orv))) == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
  %Equal.sym(Nat, B.Octets.len(B.Octets.le32(cr)), 4n, le32_len(cr)) : {H.hd.d9(Nat.is_le(4n, _), H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), s, H.hd.u32(B.Octets.le32(l)), H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c)), o, t, H.hd.u32(B.Octets.le32(orv)), ci, B.Octets.le32(cr)) == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
  %Equal.sym(Maybe<&2, U32>, B.Octets.le32_at(B.Octets.le32(l), 0n), Some{l}, BL.octets_le32_round_trip(l)) : {Done{H.AcpiHeader{s, Maybe.default(&2, U32, _, 0), H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c)), o, t, H.hd.u32(B.Octets.le32(orv)), ci, H.hd.u32(B.Octets.le32(cr))}} == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
  %Equal.sym(Maybe<&2, U32>, B.Octets.le32_at(B.Octets.le32(orv), 0n), Some{orv}, BL.octets_le32_round_trip(orv)) : {Done{H.AcpiHeader{s, l, H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c)), o, t, Maybe.default(&2, U32, _, 0), ci, H.hd.u32(B.Octets.le32(cr))}} == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
  %Equal.sym(Maybe<&2, U32>, B.Octets.le32_at(B.Octets.le32(cr), 0n), Some{cr}, BL.octets_le32_round_trip(cr)) : {Done{H.AcpiHeader{s, l, H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c)), o, t, orv, ci, Maybe.default(&2, U32, _, 0)}} == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
  %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.of_list([r])), B.mask([r]), BL.octets_to_of([r])) : {Done{H.AcpiHeader{s, l, H.hd.u8.list(_), H.hd.u8(H.hd.byte(c)), o, t, orv, ci, cr}} == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
  %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.of_list([c])), B.mask([c]), BL.octets_to_of([c])) : {Done{H.AcpiHeader{s, l, B.byte(r), H.hd.u8.list(_), o, t, orv, ci, cr}} == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
  %rev8 : {Done{H.AcpiHeader{s, l, B.byte(r), B.byte(c), o, t, orv, ci, cr}} == Done{H.AcpiHeader{s, l, _, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
  %ck8 : {Done{H.AcpiHeader{s, l, B.byte(r), B.byte(c), o, t, orv, ci, cr}} == Done{H.AcpiHeader{s, l, B.byte(r), _, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
  {==}

Uses (41):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe.default
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=byte_len
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=le32_len
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/error.bend&name=AcpiError
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/header.bend&name=AcpiHeader
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/header.bend&name=AcpiHeader.decode
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/header.bend&name=AcpiHeader.encode
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/header.bend&name=hd.byte
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/header.bend&name=hd.d1
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/header.bend&name=hd.d2
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/header.bend&name=hd.d3
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/header.bend&name=hd.d4
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/header.bend&name=hd.d5
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/header.bend&name=hd.d6
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/header.bend&name=hd.d7
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/header.bend&name=hd.d8
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/header.bend&name=hd.d9
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/header.bend&name=hd.u32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/header.bend&name=hd.u8
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/header.bend&name=hd.u8.list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_le32_round_trip
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_split_at_append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_to_of
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.le32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.le32_at
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.len
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.of_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.split_at
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.to_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=OctetsSplit
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=byte
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=mask