stobj-table

(local (progn (defstobj st1 fld1)
    (defun update-st1-in-tbl
      (val stobj-table)
      (declare (xargs :stobjs stobj-table))
      (stobj-let ((st1 (tbl-get 'st1 stobj-table (create-st1))))
        (st1)
        (update-fld1 val st1)
        stobj-table))
    (defun read-st1-in-tbl1
      (stobj-table)
      (declare (xargs :stobjs stobj-table))
      (stobj-let ((st1 (tbl-get 'st1 stobj-table (create-st1))))
        (val)
        (fld1 st1)
        val))
    (assert-event (let ((stobj-table (update-st1-in-tbl 3 stobj-table)))
        (mv (equal (read-st1-in-tbl1 stobj-table) 3) stobj-table))
      :stobjs-out '(nil stobj-table))
    (defthm read-over-write-st1-in-tbl
      (implies (stobj-tablep stobj-table)
        (let ((stobj-table (update-st1-in-tbl val stobj-table)))
          (equal (read-st1-in-tbl1 stobj-table) val))))
    (defstobj st2 fld2)
    (defun read-st2-in-tbl
      (stobj-table)
      (declare (xargs :stobjs stobj-table))
      (stobj-let ((st2 (tbl-get 'st2 stobj-table (create-st2))))
        (val)
        (fld2 st2)
        val))
    (defthm read-over-write-st2-in-tbl
      (implies (stobj-tablep stobj-table)
        (let ((stobj-table-2 (update-st1-in-tbl val stobj-table)))
          (equal (read-st2-in-tbl stobj-table-2)
            (read-st2-in-tbl stobj-table)))))))