Field-div-checked-spec
Specification of the circuit.
- Signature
(field-div-checked-spec x y z prime) → yes/no
- Arguments
- x — Guard (pfield::fep x prime).
- y — Guard (pfield::fep y prime).
- z — Guard (pfield::fep z prime).
- prime — Guard (primep prime).
- Returns
- yes/no — Type (booleanp yes/no).
The specificaton includes the fact that y is not 0.
This is consistent with a functional specification of this operation
that returns an error if y is 0:
saying that z is equal to that function
involves saying that the function does not return an error
(imagine that pfield::div below is such a function,
even though it does not return an error,
but has a guard instead.
Definitions and Theorems
Function: field-div-checked-spec
(defun field-div-checked-spec (x y z prime)
(declare (xargs :guard (and (primep prime)
(pfield::fep x prime)
(pfield::fep y prime)
(pfield::fep z prime))))
(let ((__function__ 'field-div-checked-spec))
(declare (ignorable __function__))
(and (not (equal y 0))
(equal z (pfield::div x y prime)))))
Theorem: booleanp-of-field-div-checked-spec
(defthm booleanp-of-field-div-checked-spec
(b* ((yes/no (field-div-checked-spec x y z prime)))
(booleanp yes/no))
:rule-classes :rewrite)
