		Search-engine friendly clone of the ACL2 documentation.

Lifting

Lift-definition

Shallowly embedded semantics of a definition.

Signature
(lift-definition def pred prime state) → event
Arguments: def — Guard (definitionp def).; pred — Guard (symbolp pred).; prime — Guard (symbolp prime).
Returns: event — Type (pseudo-event-formp event).

We turn the definition into an ACL2 function definition that defines a predicate that holds exactly on the values that satisfy all the constraints. If the definition has no free variables, we generate a defun. Otherwise, we generate a defun-sk with those free variables existentially quantified. (More precisely, we generate defund or defund-sk).

The existential quantification is the right semantics for the free variables in a relation's definition, based on the intended use of these constraints in zero-knowledge proofs. However, the quantification is avoided if all the variables in the body are treated as parameters.

Definitions and Theorems

Function: lift-definition

(defun lift-definition (def pred prime state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (definitionp def)
                             (symbolp pred)
                             (symbolp prime))))
 (let ((__function__ 'lift-definition))
  (declare (ignorable __function__))
  (b* (((definition def) def)
       (free (definition-free-vars def))
       (quant (lift-var-name-set-to-list free state))
       (para (lift-var-name-list def.para state))
       (body (cons 'and
                   (lift-constraint-list def.body prime state))))
   (if free
    (cons
     'defund-sk
     (cons
      pred
      (cons
       (append para (cons prime 'nil))
       (cons
        (cons
          'exists
          (cons quant
                (cons (cons 'and
                            (append (lift-gen-fep-terms quant prime)
                                    (cons body 'nil)))
                      'nil)))
        'nil))))
    (cons 'defund
          (cons pred
                (cons (append para (cons prime 'nil))
                      (cons body 'nil))))))))

Theorem: pseudo-event-formp-of-lift-definition

(defthm pseudo-event-formp-of-lift-definition
  (b* ((event (lift-definition def pred prime state)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)