		Search-engine friendly clone of the ACL2 documentation.

States64

Write64-mem-ubyte8

Write an unsigned 8-bit integer to memory.

Signature
(write64-mem-ubyte8 addr val stat) → new-stat
Arguments: addr — Guard (integerp addr).; val — Guard (ubyte8p val).; stat — Guard (state64p stat).
Returns: new-stat — Type (state64p new-stat).

The address is any integer, which we turn into a 64-bit unsigned address.

Definitions and Theorems

Function: write64-mem-ubyte8

(defun write64-mem-ubyte8 (addr val stat)
  (declare (xargs :guard (and (integerp addr)
                              (ubyte8p val)
                              (state64p stat))))
  (let ((__function__ 'write64-mem-ubyte8))
    (declare (ignorable __function__))
    (b* ((addr (loghead 64 addr)))
      (change-state64 stat
                      :mem (update-nth (loghead 64 addr)
                                       (ubyte8-fix val)
                                       (state64->mem stat))))))

Theorem: state64p-of-write64-mem-ubyte8

(defthm state64p-of-write64-mem-ubyte8
  (b* ((new-stat (write64-mem-ubyte8 addr val stat)))
    (state64p new-stat))
  :rule-classes :rewrite)

Theorem: write64-mem-ubyte8-of-ifix-addr

(defthm write64-mem-ubyte8-of-ifix-addr
  (equal (write64-mem-ubyte8 (ifix addr)
                             val stat)
         (write64-mem-ubyte8 addr val stat)))

Theorem: write64-mem-ubyte8-int-equiv-congruence-on-addr

(defthm write64-mem-ubyte8-int-equiv-congruence-on-addr
  (implies (acl2::int-equiv addr addr-equiv)
           (equal (write64-mem-ubyte8 addr val stat)
                  (write64-mem-ubyte8 addr-equiv val stat)))
  :rule-classes :congruence)

Theorem: write64-mem-ubyte8-of-ubyte8-fix-val

(defthm write64-mem-ubyte8-of-ubyte8-fix-val
  (equal (write64-mem-ubyte8 addr (ubyte8-fix val)
                             stat)
         (write64-mem-ubyte8 addr val stat)))

Theorem: write64-mem-ubyte8-ubyte8-equiv-congruence-on-val

(defthm write64-mem-ubyte8-ubyte8-equiv-congruence-on-val
  (implies (acl2::ubyte8-equiv val val-equiv)
           (equal (write64-mem-ubyte8 addr val stat)
                  (write64-mem-ubyte8 addr val-equiv stat)))
  :rule-classes :congruence)

Theorem: write64-mem-ubyte8-of-state64-fix-stat

(defthm write64-mem-ubyte8-of-state64-fix-stat
  (equal (write64-mem-ubyte8 addr val (state64-fix stat))
         (write64-mem-ubyte8 addr val stat)))

Theorem: write64-mem-ubyte8-state64-equiv-congruence-on-stat

(defthm write64-mem-ubyte8-state64-equiv-congruence-on-stat
  (implies (state64-equiv stat stat-equiv)
           (equal (write64-mem-ubyte8 addr val stat)
                  (write64-mem-ubyte8 addr val stat-equiv)))
  :rule-classes :congruence)