		Search-engine friendly clone of the ACL2 documentation.

State-stobj

Write1-memory-unsigned64

Refine write-memory-unsigned64 to use the stobj states.

Definitions and Theorems

Function: write1-memory-unsigned64

(defun write1-memory-unsigned64 (addr val stat feat)
 (declare (xargs :non-executable t))
 (declare
    (xargs :guard (non-exec (and (stat1p stat)
                                 (integerp addr)
                                 (ubyte64p val)
                                 (statp (stat-from-stat1 stat))
                                 (featp feat)
                                 (stat-validp (stat-from-stat1 stat)
                                              feat)))))
 (prog2$
  (acl2::throw-nonexec-error 'write1-memory-unsigned64
                             (list addr val stat feat))
  (if
   (acl2::mbt$ (stat1p stat))
   (let ((val (ubyte64-fix val))
         (stat (stat-from-stat1 stat)))
    (let* ((b0 (bitops::part-select-width-low val 8 0))
           (b1 (bitops::part-select-width-low val 8 8))
           (b2 (bitops::part-select-width-low val 8 16))
           (b3 (bitops::part-select-width-low val 8 24))
           (b4 (bitops::part-select-width-low val 8 32))
           (b5 (bitops::part-select-width-low val 8 40))
           (b6 (bitops::part-select-width-low val 8 48))
           (b7 (bitops::part-select-width-low val 8 56)))
     (mv-let (1st-byte 2nd-byte 3rd-byte 4th-byte
                       5th-byte 6th-byte 7th-byte 8th-byte)
             (if (feat-little-endianp feat)
                 (mv b0 b1 b2 b3 b4 b5 b6 b7)
               (mv b7 b6 b5 b4 b3 b2 b1 b0))
      (let* ((stat (write-memory-unsigned8 addr 1st-byte stat feat))
             (stat (write-memory-unsigned8 (+ (lifix addr) 1)
                                           2nd-byte stat feat))
             (stat (write-memory-unsigned8 (+ (lifix addr) 2)
                                           3rd-byte stat feat))
             (stat (write-memory-unsigned8 (+ (lifix addr) 3)
                                           4th-byte stat feat))
             (stat (write-memory-unsigned8 (+ (lifix addr) 4)
                                           5th-byte stat feat))
             (stat (write-memory-unsigned8 (+ (lifix addr) 5)
                                           6th-byte stat feat))
             (stat (write-memory-unsigned8 (+ (lifix addr) 6)
                                           7th-byte stat feat))
             (stat (write-memory-unsigned8 (+ (lifix addr) 7)
                                           8th-byte stat feat)))
        stat))))
   0)))

Theorem: write1-memory-unsigned64-to-write-memory-unsigned64

(defthm write1-memory-unsigned64-to-write-memory-unsigned64
 (implies
     (stat1p stat)
     (equal (write1-memory-unsigned64 addr val stat feat)
            (write-memory-unsigned64 addr val (stat-from-stat1 stat)
                                     feat)))
 :rule-classes :rewrite)

Theorem: write-memory-unsigned64-to-write1-memory-unsigned64

(defthm write-memory-unsigned64-to-write1-memory-unsigned64
 (implies
    (statp stat)
    (equal (write-memory-unsigned64 addr val stat feat)
           (write1-memory-unsigned64 addr val (stat1-from-stat stat)
                                     feat)))
 :rule-classes :rewrite)