• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Soft
      • Bv
      • Imp-language
      • C
        • Syntax-for-tools
        • Atc
        • Language
          • Abstract-syntax
          • Integer-ranges
          • Dynamic-semantics
          • Static-semantics
          • Grammar
          • Integer-formats
          • Types
          • Portable-ascii-identifiers
          • Values
          • Integer-operations
          • Computation-states
          • Object-designators
          • Implementation-environments
          • Operations
          • Errors
          • Tag-environments
          • Function-environments
          • Character-sets
          • Flexible-array-member-removal
          • Arithmetic-operations
          • Pointer-operations
          • Bytes
          • Keywords
          • Real-operations
          • Array-operations
          • Scalar-operations
          • Structure-operations
            • Value-struct-write
            • Value-struct-read
        • Representation
        • Transformation-tools
        • Pack
      • Event-macros
      • Java
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Number-theory
      • Cryptography
      • Lists-light
      • Builtins
      • Axe
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Structure-operations

Value-struct-write

Write a member of a structure.

Signature

(value-struct-write name val struct) → new-struct

Arguments

name — Guard (identp name).

val — Guard (valuep val).

struct — Guard (valuep struct).

Returns

new-struct — Type (value-resultp new-struct).

We look up the members in order; given that the members have distinct names (see value), the search order is immaterial. The new value must have the same type as the old value.

Prior to storing the value, we remove its flexible array member, if any. See remove-flexible-array-member.

Definitions and Theorems

Function: value-struct-write-aux

(defun value-struct-write-aux (name val members)
 (declare (xargs :guard (and (identp name)
                             (valuep val)
                             (member-value-listp members))))
 (let ((__function__ 'value-struct-write-aux))
  (declare (ignorable __function__))
  (b*
   (((when (endp members))
     (error (list :member-not-found (ident-fix name))))
    ((member-value member) (car members))
    ((when (equal member.name (ident-fix name)))
     (if
      (equal (type-of-value member.value)
             (type-of-value val))
      (cons
       (make-member-value :name name
                          :value (remove-flexible-array-member val))
       (member-value-list-fix (cdr members)))
      (error (list :mistype-member (ident-fix name)
                   :old-value member.value
                   :new-value (value-fix val)))))
    (new-cdr-members
         (value-struct-write-aux name val (cdr members)))
    ((when (errorp new-cdr-members))
     new-cdr-members))
   (cons (member-value-fix (car members))
         new-cdr-members))))

Theorem: member-value-list-resultp-of-value-struct-write-aux

(defthm member-value-list-resultp-of-value-struct-write-aux
  (b* ((new-members (value-struct-write-aux name val members)))
    (member-value-list-resultp new-members))
  :rule-classes :rewrite)

Theorem: member-value-listp-of-value-struct-write-aux

(defthm member-value-listp-of-value-struct-write-aux
  (b* ((old (value-struct-read-aux name memvals))
       (memvals1 (value-struct-write-aux name new memvals)))
    (implies (and (valuep old)
                  (equal (type-of-value new)
                         (type-of-value old)))
             (member-value-listp memvals1))))

Theorem: member-value-list->name-list-of-struct-write-aux

(defthm member-value-list->name-list-of-struct-write-aux
  (b* ((old (value-struct-read-aux name memvals))
       (memvals1 (value-struct-write-aux name new memvals)))
    (implies (and (valuep old)
                  (equal (type-of-value new)
                         (type-of-value old)))
             (equal (member-value-list->name-list memvals1)
                    (member-value-list->name-list memvals)))))

Theorem: value-struct-read-aux-of-value-struct-write-aux

(defthm value-struct-read-aux-of-value-struct-write-aux
  (b* ((old (value-struct-read-aux name memvals))
       (memvals1 (value-struct-write-aux name new memvals)))
    (implies (and (valuep old)
                  (equal (type-of-value new)
                         (type-of-value old)))
             (equal (value-struct-read-aux name1 memvals1)
                    (if (ident-equiv name1 name)
                        (remove-flexible-array-member new)
                      (value-struct-read-aux name1 memvals))))))

Theorem: value-struct-write-aux-when-member-type-lookup

(defthm value-struct-write-aux-when-member-type-lookup
 (implies
  (equal memtypes
         (member-types-of-member-values memvals))
  (b* ((type (member-type-lookup name memtypes))
       (new-memvals (value-struct-write-aux name val memvals)))
    (implies (and (typep type)
                  (valuep val)
                  (equal (type-of-value val) type))
             (and (member-value-listp new-memvals)
                  (equal (member-types-of-member-values new-memvals)
                         memtypes))))))

Theorem: value-struct-write-aux-of-ident-fix-name

(defthm value-struct-write-aux-of-ident-fix-name
  (equal (value-struct-write-aux (ident-fix name)
                                 val members)
         (value-struct-write-aux name val members)))

Theorem: value-struct-write-aux-ident-equiv-congruence-on-name

(defthm value-struct-write-aux-ident-equiv-congruence-on-name
  (implies (ident-equiv name name-equiv)
           (equal (value-struct-write-aux name val members)
                  (value-struct-write-aux name-equiv val members)))
  :rule-classes :congruence)

Theorem: value-struct-write-aux-of-value-fix-val

(defthm value-struct-write-aux-of-value-fix-val
  (equal (value-struct-write-aux name (value-fix val)
                                 members)
         (value-struct-write-aux name val members)))

Theorem: value-struct-write-aux-value-equiv-congruence-on-val

(defthm value-struct-write-aux-value-equiv-congruence-on-val
  (implies (value-equiv val val-equiv)
           (equal (value-struct-write-aux name val members)
                  (value-struct-write-aux name val-equiv members)))
  :rule-classes :congruence)

Theorem: value-struct-write-aux-of-member-value-list-fix-members

(defthm value-struct-write-aux-of-member-value-list-fix-members
 (equal (value-struct-write-aux name
                                val (member-value-list-fix members))
        (value-struct-write-aux name val members)))

Theorem: value-struct-write-aux-member-value-list-equiv-congruence-on-members

(defthm
 value-struct-write-aux-member-value-list-equiv-congruence-on-members
 (implies (member-value-list-equiv members members-equiv)
          (equal (value-struct-write-aux name val members)
                 (value-struct-write-aux name val members-equiv)))
 :rule-classes :congruence)

Function: value-struct-write

(defun value-struct-write (name val struct)
 (declare (xargs :guard (and (identp name)
                             (valuep val)
                             (valuep struct))))
 (declare (xargs :guard (value-case struct :struct)))
 (let ((__function__ 'value-struct-write))
  (declare (ignorable __function__))
  (b*
   ((new-members
        (value-struct-write-aux name
                                val (value-struct->members struct)))
    ((when (errorp new-members))
     new-members))
   (change-value-struct struct
                        :members new-members))))

Theorem: value-resultp-of-value-struct-write

(defthm value-resultp-of-value-struct-write
  (b* ((new-struct (value-struct-write name val struct)))
    (value-resultp new-struct))
  :rule-classes :rewrite)

Theorem: value-kind-of-value-struct-write

(defthm value-kind-of-value-struct-write
  (b* ((?new-struct (value-struct-write name val struct)))
    (implies (not (errorp new-struct))
             (equal (value-kind new-struct)
                    :struct))))

Theorem: valuep-of-value-struct-write

(defthm valuep-of-value-struct-write
  (b* ((old (value-struct-read name struct))
       (struct1 (value-struct-write name new struct)))
    (implies (and (valuep old)
                  (equal (type-of-value new)
                         (type-of-value old)))
             (valuep struct1))))

Theorem: value-struct-read-of-value-struct-write

(defthm value-struct-read-of-value-struct-write
  (b* ((old (value-struct-read name struct))
       (struct1 (value-struct-write name new struct)))
    (implies (and (valuep old)
                  (equal (type-of-value new)
                         (type-of-value old)))
             (equal (value-struct-read name1 struct1)
                    (if (ident-equiv name1 name)
                        (remove-flexible-array-member new)
                      (value-struct-read name1 struct))))))

Theorem: value-struct-write-of-ident-fix-name

(defthm value-struct-write-of-ident-fix-name
  (equal (value-struct-write (ident-fix name)
                             val struct)
         (value-struct-write name val struct)))

Theorem: value-struct-write-ident-equiv-congruence-on-name

(defthm value-struct-write-ident-equiv-congruence-on-name
  (implies (ident-equiv name name-equiv)
           (equal (value-struct-write name val struct)
                  (value-struct-write name-equiv val struct)))
  :rule-classes :congruence)

Theorem: value-struct-write-of-value-fix-val

(defthm value-struct-write-of-value-fix-val
  (equal (value-struct-write name (value-fix val)
                             struct)
         (value-struct-write name val struct)))

Theorem: value-struct-write-value-equiv-congruence-on-val

(defthm value-struct-write-value-equiv-congruence-on-val
  (implies (value-equiv val val-equiv)
           (equal (value-struct-write name val struct)
                  (value-struct-write name val-equiv struct)))
  :rule-classes :congruence)

Theorem: value-struct-write-of-value-fix-struct

(defthm value-struct-write-of-value-fix-struct
  (equal (value-struct-write name val (value-fix struct))
         (value-struct-write name val struct)))

Theorem: value-struct-write-value-equiv-congruence-on-struct

(defthm value-struct-write-value-equiv-congruence-on-struct
  (implies (value-equiv struct struct-equiv)
           (equal (value-struct-write name val struct)
                  (value-struct-write name val struct-equiv)))
  :rule-classes :congruence)