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