		Search-engine friendly clone of the ACL2 documentation.

Static-safety-checking

Check-safe-path

Check if a path is safe.

Signature
(check-safe-path path varset) → _
Arguments: path — Guard (pathp path).; varset — Guard (identifier-setp varset).
Returns: _ — Type (reserr-optionp _).

As a structural condition, a path must consists of one or more identifiers. More importantly, it must refer to an existing variable. It is not yet clear how paths with more than one identifier come about in generic Yul: variable declarations are for single identifiers (whether one single identifier, or two or more single identifiers), so it seems that singleton paths would always suffice to reference them in expressions and statements. For now we only regard singleton paths as safe, provided they are part of the accessible variables.

We may move the non-emptiness requirement into an invariant of path, but for now we state it as part of the static semantics.

Definitions and Theorems

Function: check-safe-path

(defun check-safe-path (path varset)
  (declare (xargs :guard (and (pathp path)
                              (identifier-setp varset))))
  (let ((__function__ 'check-safe-path))
    (declare (ignorable __function__))
    (b* ((idens (path->get path))
         ((unless (consp idens))
          (reserrf (list :empty-path (path-fix path))))
         ((unless (endp (cdr idens)))
          (reserrf (list :non-singleton-path (path-fix path))))
         (var (car idens))
         ((unless (check-var var varset))
          (reserrf (list :variable-not-found var))))
      nil)))

Theorem: reserr-optionp-of-check-safe-path

(defthm reserr-optionp-of-check-safe-path
  (b* ((_ (check-safe-path path varset)))
    (reserr-optionp _))
  :rule-classes :rewrite)

Theorem: check-safe-path-of-path-fix-path

(defthm check-safe-path-of-path-fix-path
  (equal (check-safe-path (path-fix path) varset)
         (check-safe-path path varset)))

Theorem: check-safe-path-path-equiv-congruence-on-path

(defthm check-safe-path-path-equiv-congruence-on-path
  (implies (path-equiv path path-equiv)
           (equal (check-safe-path path varset)
                  (check-safe-path path-equiv varset)))
  :rule-classes :congruence)

Theorem: check-safe-path-of-identifier-set-fix-varset

(defthm check-safe-path-of-identifier-set-fix-varset
  (equal (check-safe-path path (identifier-set-fix varset))
         (check-safe-path path varset)))

Theorem: check-safe-path-identifier-set-equiv-congruence-on-varset

(defthm check-safe-path-identifier-set-equiv-congruence-on-varset
  (implies (identifier-set-equiv varset varset-equiv)
           (equal (check-safe-path path varset)
                  (check-safe-path path varset-equiv)))
  :rule-classes :congruence)