		Search-engine friendly clone of the ACL2 documentation.

States

Write-mem8

Write an unsigned 8-bit integer to memory.

Signature
(write-mem8 addr val stat feat) → new-stat
Arguments: addr — Guard (integerp addr).; val — Guard (ubyte8p val).; stat — Guard (statp stat).; feat — Guard (featp feat).
Returns: new-stat — Type (statp new-stat).

The address is an integer of arbitrary size, of which we consider only the low XLEN bits, as an unsigned address. Allowing any integer is convenient for callers. We write the byte at that address.

Since we write a single byte, there is no difference between little and big endian.

Definitions and Theorems

Function: write-mem8

(defun write-mem8 (addr val stat feat)
  (declare (xargs :guard (and (integerp addr)
                              (ubyte8p val)
                              (statp stat)
                              (featp feat))))
  (declare (xargs :guard (stat-validp stat feat)))
  (b* ((addr (loghead (feat->xlen feat) addr)))
    (change-stat stat
                 :memory (update-nth addr (ubyte8-fix val)
                                     (stat->memory stat)))))

Theorem: statp-of-write-mem8

(defthm statp-of-write-mem8
  (b* ((new-stat (write-mem8 addr val stat feat)))
    (statp new-stat))
  :rule-classes :rewrite)

Theorem: stat-validp-of-write-mem8

(defthm stat-validp-of-write-mem8
  (implies (stat-validp stat feat)
           (b* ((?new-stat (write-mem8 addr val stat feat)))
             (stat-validp new-stat feat))))

Theorem: write-mem8-of-ifix-addr

(defthm write-mem8-of-ifix-addr
  (equal (write-mem8 (ifix addr) val stat feat)
         (write-mem8 addr val stat feat)))

Theorem: write-mem8-int-equiv-congruence-on-addr

(defthm write-mem8-int-equiv-congruence-on-addr
  (implies (acl2::int-equiv addr addr-equiv)
           (equal (write-mem8 addr val stat feat)
                  (write-mem8 addr-equiv val stat feat)))
  :rule-classes :congruence)

Theorem: write-mem8-of-ubyte8-fix-val

(defthm write-mem8-of-ubyte8-fix-val
  (equal (write-mem8 addr (ubyte8-fix val)
                     stat feat)
         (write-mem8 addr val stat feat)))

Theorem: write-mem8-ubyte8-equiv-congruence-on-val

(defthm write-mem8-ubyte8-equiv-congruence-on-val
  (implies (acl2::ubyte8-equiv val val-equiv)
           (equal (write-mem8 addr val stat feat)
                  (write-mem8 addr val-equiv stat feat)))
  :rule-classes :congruence)

Theorem: write-mem8-of-stat-fix-stat

(defthm write-mem8-of-stat-fix-stat
  (equal (write-mem8 addr val (stat-fix stat)
                     feat)
         (write-mem8 addr val stat feat)))

Theorem: write-mem8-stat-equiv-congruence-on-stat

(defthm write-mem8-stat-equiv-congruence-on-stat
  (implies (stat-equiv stat stat-equiv)
           (equal (write-mem8 addr val stat feat)
                  (write-mem8 addr val stat-equiv feat)))
  :rule-classes :congruence)

Theorem: write-mem8-of-feat-fix-feat

(defthm write-mem8-of-feat-fix-feat
  (equal (write-mem8 addr val stat (feat-fix feat))
         (write-mem8 addr val stat feat)))

Theorem: write-mem8-feat-equiv-congruence-on-feat

(defthm write-mem8-feat-equiv-congruence-on-feat
  (implies (feat-equiv feat feat-equiv)
           (equal (write-mem8 addr val stat feat)
                  (write-mem8 addr val stat feat-equiv)))
  :rule-classes :congruence)