def hdr_rt

bend-osdev-acpi@0.1.1.0 · PROOF.bend:2298
import bend-osdev-acpi@0.1.1.0/PROOF.bend as PROOF
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

2298def 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>}:
2299  %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>}
2300  %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>}
2301  %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>}
2302  %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>}
2303  %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>}
2304  %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>}
2305  %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>}
2306  %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>}
2307  %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>}
2308  %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>}
2309  %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>}
2310  %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>}
2311  %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>}
2312  %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>}
2313  %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>}
2314  %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>}
2315  %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>}
2316  %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>}
2317  %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>}
2318  %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>}
2319  %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>}
2320  %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>}
2321  %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>}
2322  %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>}
2323  {==}
Uses (41)

Used by (1)

bend-osdev-acpi@0.1.1.0/LAWS:header_round_trip