		Search-engine friendly clone of the ACL2 documentation.

Semantics-shallowly-embedded

Sesem-definition

Shallowly embedded semantics of a definition.

Signature
(sesem-definition def prime state) → event
Arguments: def — Guard (definitionp def).; 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: sesem-definition

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

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

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