		Search-engine friendly clone of the ACL2 documentation.

States

Write-memory-unsigned8

Write an unsigned 8-bit integer to memory.

Signature
(write-memory-unsigned8 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-memory-unsigned8

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

Theorem: statp-of-write-memory-unsigned8

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

Theorem: stat-validp-of-write-memory-unsigned8

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

Theorem: write-memory-unsigned8-of-ifix-addr

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

Theorem: write-memory-unsigned8-int-equiv-congruence-on-addr

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

Theorem: write-memory-unsigned8-of-ubyte8-fix-val

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

Theorem: write-memory-unsigned8-ubyte8-equiv-congruence-on-val

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

Theorem: write-memory-unsigned8-of-stat-fix-stat

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

Theorem: write-memory-unsigned8-stat-equiv-congruence-on-stat

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

Theorem: write-memory-unsigned8-of-feat-fix-feat

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

Theorem: write-memory-unsigned8-feat-equiv-congruence-on-feat

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