def ckw.gfix

bend-osdev-acpi@0.1.2.0 · PROOF_whole.bend:141
import bend-osdev-acpi@0.1.2.0/PROOF_whole.bend as PROOFWhole
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
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL
import bend-osdev-acpi@0.1.2.0/checksum.bend as C

141def ckw.gfix(+i: Nat, +p: B.Octets, +q: U32, +rest: B.Octets, +hp: {B.Octets.len(p) == i : Nat}) -> {C.AcpiChecksum.fix(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))) == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}:
142  %Equal.sym(Bool, Nat.is_lt(i, B.Octets.len(B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))), True{}, ckw.glt(i, p, q, rest, hp)) : {C.ck.fix.pick(_, i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))) == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}
143  %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.take(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), [B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]}), B.Octets.append(B.Octets.take(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), B.Octets.concat([B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))])), BL.octets_concat_cons(B.Octets.take(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), [B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))])) : {_ == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}
144  %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), [B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]}), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), B.Octets.concat([B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))])), BL.octets_concat_cons(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), [B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))])) : {B.Octets.append(B.Octets.take(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), _) == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}
145  %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), Nil{}}), B.Octets.append(B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), B.Octets.concat(Nil{})), BL.octets_concat_cons(B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), Nil{})) : {B.Octets.append(B.Octets.take(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), _)) == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}
146  %Equal.sym(B.Octets, B.Octets.concat(Nil{}), B.Octets.empty(), BL.octets_concat_nil()) : {B.Octets.append(B.Octets.take(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), B.Octets.append(B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), _))) == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}
147  %Equal.sym(B.Octets, B.Octets.append(B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), B.Octets.empty()), B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), BL.octets_append_empty_r(B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))))) : {B.Octets.append(B.Octets.take(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), _)) == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}
148  %hp : {B.Octets.append(B.Octets.take(_, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))))) == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}
149  %Equal.sym(B.Octets, B.Octets.take(B.Octets.len(p), B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), p, BL.octets_take_append(p, B.Octets.append(B.Octets.of_list([q]), rest))) : {B.Octets.append(_, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))))) == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}
150  %Equal.trans(Nat, Nat.add(B.Octets.len(p), 1n), Nat.add(i, 1n), Nat.add(1n, i), Equal.cong(Nat, Nat, z => Nat.add(z, 1n), B.Octets.len(p), i, hp), UL.nat_add_comm(i, 1n)) : {B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), B.Octets.drop(_, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))))) == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}
151  %Equal.sym(B.Octets, B.Octets.drop(Nat.add(B.Octets.len(p), 1n), B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), B.Octets.drop(1n, B.Octets.append(B.Octets.of_list([q]), rest)), BL.octets_drop_append_add(p, 1n, B.Octets.append(B.Octets.of_list([q]), rest))) : {B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), _)) == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}
152  %BL.octets_len_of_list([q]) : {B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), B.Octets.drop(_, B.Octets.append(B.Octets.of_list([q]), rest)))) == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}
153  %Equal.sym(B.Octets, B.Octets.drop(B.Octets.len(B.Octets.of_list([q])), B.Octets.append(B.Octets.of_list([q]), rest)), rest, BL.octets_drop_append(B.Octets.of_list([q]), rest)) : {B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), _)) == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}
154  {==}
def ckw.gfix

Uses (29)

Used by (3)
