• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Riscv
        • Specification
        • Executable
        • Specialized
          • Specialized-features
          • Rv64im
            • Semantics64
            • States64
              • Write64-xreg
              • Write64-xreg-32
              • Write64-mem-ubyte64-lendian
                • Write64-mem-ubyte16-lendian
                • Xregfile64
                • State64
                • Memory64
                • Write64-mem-ubyte32-lendian
                • Write64-pc
                • Read64-mem-ubyte64-lendian
                • Read64-mem-ubyte16-lendian
                • Write64-mem-ubyte8
                • Read64-xreg-unsigned
                • Read64-mem-ubyte32-lendian
                • Read64-mem-ubyte8
                • Read64-xreg-unsigned32
                • Read64-xreg-signed32
                • Read64-xreg-signed
                • Inc64-pc
                • Read64-pc
                • Error64p
                • Error64
                • *mem64-size*
              • Execution64
            • Rv32im
            • Specialized-states
          • Optimized
        • Taspi
        • Bitcoin
        • Des
        • Ethereum
        • X86isa
        • Sha-2
        • Yul
        • Zcash
        • Proof-checker-itp13
        • Regex
        • ACL2-programming-language
        • Json
        • Jfkr
        • Equational
        • Cryptography
        • Poseidon
        • Where-do-i-place-my-book
        • Axe
        • Aleo
        • Bigmems
        • Builtins
        • Execloader
        • Solidity
        • Paco
        • Concurrent-programs
        • Bls12-377-curves
      • Debugging
      • Std
      • Community
      • Proof-automation
      • ACL2
      • Macro-libraries
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • States64

    Write64-mem-ubyte64-lendian

    Write an unsigned 64-bit little endian integer to memory.

    Signature
    (write64-mem-ubyte64-lendian addr val stat) → new-stat
    Arguments
    addr — Guard (integerp addr).
    val — Guard (ubyte64p val).
    stat — Guard (state64p stat).
    Returns
    new-stat — Type (state64p new-stat).

    This is similar to write64-mem-ubyte16-lendian and write64-mem-ubyte32-lendian, but with 8 bytes instead of 2 or 4.

    Definitions and Theorems

    Function: write64-mem-ubyte64-lendian

    (defun write64-mem-ubyte64-lendian (addr val stat)
      (declare (xargs :guard (and (integerp addr)
                                  (ubyte64p val)
                                  (state64p stat))))
      (let ((__function__ 'write64-mem-ubyte64-lendian))
        (declare (ignorable __function__))
        (b* ((val (ubyte64-fix val))
             (b0 (logand val 255))
             (b1 (logand (ash val -8) 255))
             (b2 (logand (ash val -16) 255))
             (b3 (logand (ash val -24) 255))
             (b4 (logand (ash val -32) 255))
             (b5 (logand (ash val -40) 255))
             (b6 (logand (ash val -48) 255))
             (b7 (ash val -56))
             (stat (write64-mem-ubyte8 addr b0 stat))
             (stat (write64-mem-ubyte8 (+ 1 (ifix addr))
                                       b1 stat))
             (stat (write64-mem-ubyte8 (+ 2 (ifix addr))
                                       b2 stat))
             (stat (write64-mem-ubyte8 (+ 3 (ifix addr))
                                       b3 stat))
             (stat (write64-mem-ubyte8 (+ 4 (ifix addr))
                                       b4 stat))
             (stat (write64-mem-ubyte8 (+ 5 (ifix addr))
                                       b5 stat))
             (stat (write64-mem-ubyte8 (+ 6 (ifix addr))
                                       b6 stat))
             (stat (write64-mem-ubyte8 (+ 7 (ifix addr))
                                       b7 stat)))
          stat)))

    Theorem: state64p-of-write64-mem-ubyte64-lendian

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

    Theorem: write64-mem-ubyte64-lendian-of-ifix-addr

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

    Theorem: write64-mem-ubyte64-lendian-int-equiv-congruence-on-addr

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

    Theorem: write64-mem-ubyte64-lendian-of-ubyte64-fix-val

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

    Theorem: write64-mem-ubyte64-lendian-ubyte64-equiv-congruence-on-val

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

    Theorem: write64-mem-ubyte64-lendian-of-state64-fix-stat

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

    Theorem: write64-mem-ubyte64-lendian-state64-equiv-congruence-on-stat

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