def tb.gas_a

bend-osdev-acpi@0.1.1.0 · PROOF_tables.bend:42

import Base
import bend-osdev-word64@0.1.1.0/word64.bend as W
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
import bend-osdev-bytes@0.1.1.0/LAWS.bend as BL

42def tb.gas_a(+a: B.Octets, +s: U32, +w: U32, +off: U32, +acc: U32, +addr: W.W64, +b: B.Octets) -> {Some{addr} == B.Octets.le64_at(B.Octets.append(a, B.Octets.append(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b))), Nat.add(B.Octets.len(a), 4n)) : Maybe<&2, W.W64>}:
43  Equal.sym(Maybe<&2, W.W64>, B.Octets.le64_at(B.Octets.append(a, B.Octets.append(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b))), Nat.add(B.Octets.len(a), 4n)), Some{addr}, Equal.trans(Maybe<&2, W.W64>, B.Octets.le64_at(B.Octets.append(a, B.Octets.append(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b))), Nat.add(B.Octets.len(a), 4n)), B.Octets.le64_at(B.Octets.append(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b)), 4n), Some{addr}, BL.octets_le64_at_append_add(a, B.Octets.append(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b)), 4n), Equal.trans(Maybe<&2, W.W64>, B.Octets.le64_at(B.Octets.append(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b)), 4n), B.Octets.le64_at(B.Octets.append(B.Octets.le64(addr), b), 0n), Some{addr}, BL.octets_le64_at_append_add(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b), 0n), Equal.trans(Maybe<&2, W.W64>, B.Octets.le64_at(B.Octets.append(B.Octets.le64(addr), b), 0n), B.Octets.le64_at(B.Octets.le64(addr), 0n), Some{addr}, BL.octets_le64_at_append_le(B.Octets.le64(addr), b, 0n, tb.l64(addr)), BL.octets_le64_round_trip(addr)))))