		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-hidstep-mark-interfaces

Signature
(vl-hidstep-mark-interfaces mtype step ss st ctx) → new-st
Arguments: mtype — Guard (member mtype '(:used :set)).; step — Guard (vl-hidstep-p step).; ss — Guard (vl-scopestack-p ss).; st — Guard (vl-lucidstate-p st).; ctx — Guard (vl-context1-p ctx).
Returns: new-st — Type (vl-lucidstate-p new-st).

Definitions and Theorems

Function: vl-hidstep-mark-interfaces

(defun vl-hidstep-mark-interfaces (mtype step ss st ctx)
 (declare (xargs :guard (and (member mtype '(:used :set))
                             (vl-hidstep-p step)
                             (vl-scopestack-p ss)
                             (vl-lucidstate-p st)
                             (vl-context1-p ctx))))
 (let ((__function__ 'vl-hidstep-mark-interfaces))
   (declare (ignorable __function__))
   (b*
    (((vl-hidstep step))
     ((when (eq (tag step.item) :vl-interfaceport))
      (b* ((key (make-vl-lucidkey
                     :item step.item
                     :scopestack (vl-normalize-scopestack step.ss)))
           (occ (make-vl-lucidocc-solo :ctx ctx
                                       :ss ss)))
        (vl-lucidstate-mark mtype key occ st ctx))))
    (vl-lucidstate-fix st))))

Theorem: vl-lucidstate-p-of-vl-hidstep-mark-interfaces

(defthm vl-lucidstate-p-of-vl-hidstep-mark-interfaces
  (b* ((new-st (vl-hidstep-mark-interfaces mtype step ss st ctx)))
    (vl-lucidstate-p new-st))
  :rule-classes :rewrite)

Theorem: vl-hidstep-mark-interfaces-of-vl-hidstep-fix-step

(defthm vl-hidstep-mark-interfaces-of-vl-hidstep-fix-step
  (equal (vl-hidstep-mark-interfaces mtype (vl-hidstep-fix step)
                                     ss st ctx)
         (vl-hidstep-mark-interfaces mtype step ss st ctx)))

Theorem: vl-hidstep-mark-interfaces-vl-hidstep-equiv-congruence-on-step

(defthm
     vl-hidstep-mark-interfaces-vl-hidstep-equiv-congruence-on-step
 (implies
    (vl-hidstep-equiv step step-equiv)
    (equal (vl-hidstep-mark-interfaces mtype step ss st ctx)
           (vl-hidstep-mark-interfaces mtype step-equiv ss st ctx)))
 :rule-classes :congruence)

Theorem: vl-hidstep-mark-interfaces-of-vl-scopestack-fix-ss

(defthm vl-hidstep-mark-interfaces-of-vl-scopestack-fix-ss
  (equal
       (vl-hidstep-mark-interfaces mtype step (vl-scopestack-fix ss)
                                   st ctx)
       (vl-hidstep-mark-interfaces mtype step ss st ctx)))

Theorem: vl-hidstep-mark-interfaces-vl-scopestack-equiv-congruence-on-ss

(defthm
    vl-hidstep-mark-interfaces-vl-scopestack-equiv-congruence-on-ss
 (implies
    (vl-scopestack-equiv ss ss-equiv)
    (equal (vl-hidstep-mark-interfaces mtype step ss st ctx)
           (vl-hidstep-mark-interfaces mtype step ss-equiv st ctx)))
 :rule-classes :congruence)

Theorem: vl-hidstep-mark-interfaces-of-vl-lucidstate-fix-st

(defthm vl-hidstep-mark-interfaces-of-vl-lucidstate-fix-st
 (equal
    (vl-hidstep-mark-interfaces mtype step ss (vl-lucidstate-fix st)
                                ctx)
    (vl-hidstep-mark-interfaces mtype step ss st ctx)))

Theorem: vl-hidstep-mark-interfaces-vl-lucidstate-equiv-congruence-on-st

(defthm
    vl-hidstep-mark-interfaces-vl-lucidstate-equiv-congruence-on-st
 (implies
    (vl-lucidstate-equiv st st-equiv)
    (equal (vl-hidstep-mark-interfaces mtype step ss st ctx)
           (vl-hidstep-mark-interfaces mtype step ss st-equiv ctx)))
 :rule-classes :congruence)

Theorem: vl-hidstep-mark-interfaces-of-vl-context1-fix-ctx

(defthm vl-hidstep-mark-interfaces-of-vl-context1-fix-ctx
  (equal (vl-hidstep-mark-interfaces
              mtype step ss st (vl-context1-fix ctx))
         (vl-hidstep-mark-interfaces mtype step ss st ctx)))

Theorem: vl-hidstep-mark-interfaces-vl-context1-equiv-congruence-on-ctx

(defthm
     vl-hidstep-mark-interfaces-vl-context1-equiv-congruence-on-ctx
 (implies
    (vl-context1-equiv ctx ctx-equiv)
    (equal (vl-hidstep-mark-interfaces mtype step ss st ctx)
           (vl-hidstep-mark-interfaces mtype step ss st ctx-equiv)))
 :rule-classes :congruence)