		Search-engine friendly clone of the ACL2 documentation.

Literal-evaluation

Eval-literal

Evaluate a Leo literal.

Signature
(eval-literal lit curve) → result
Arguments: lit — Guard (literalp lit).; curve — Guard (curvep curve).
Returns: result — Type (value-optionp result).

Evaluating a boolean literal is straighforward.

Evaluating an unsigned or signed integer literal involves checking that the number is representable in the bit size, returning nil (to indicate error) if not.

Evaluating a string literal is straightforward.

Evaluating an address literal is straightforward.

Evaluating a field element literal is with respect to a prime number that defines the prime field, in the same way that the field arithmetic operations are defined with respect to a prime. Any integer (including negative ones) is allowed in a field element literal: it is coerced into an element of the prime field via modular reduction.

The evaluation of group element literals is formalized by eval-group-literal.

Evaluating a scalar literal is similar to a field literal in that both are modular reduced to a field, but the modulus is different.

Definitions and Theorems

Function: eval-literal

(defun eval-literal (lit curve)
  (declare (xargs :guard (and (literalp lit) (curvep curve))))
  (let ((__function__ 'eval-literal))
    (declare (ignorable __function__))
    (literal-case
         lit
         :bool (value-bool lit.val)
         :unsigned (bitsize-case lit.size
                                 :|8| (and (ubyte8p lit.val)
                                           (value-u8 lit.val))
                                 :|16| (and (ubyte16p lit.val)
                                            (value-u16 lit.val))
                                 :|32| (and (ubyte32p lit.val)
                                            (value-u32 lit.val))
                                 :|64| (and (ubyte64p lit.val)
                                            (value-u64 lit.val))
                                 :|128| (and (ubyte128p lit.val)
                                             (value-u128 lit.val)))
         :signed (bitsize-case lit.size
                               :|8| (and (sbyte8p lit.val)
                                         (value-i8 lit.val))
                               :|16| (and (sbyte16p lit.val)
                                          (value-i16 lit.val))
                               :|32| (and (sbyte32p lit.val)
                                          (value-i32 lit.val))
                               :|64| (and (sbyte64p lit.val)
                                          (value-i64 lit.val))
                               :|128| (and (sbyte128p lit.val)
                                           (value-i128 lit.val)))
         :string (value-string lit.get)
         :address (value-address lit.get)
         :field (value-field (mod lit.val (curve-base-prime curve)))
         :group (eval-group-literal lit.get curve)
         :scalar
         (value-scalar (mod lit.val (curve-scalar-prime curve))))))

Theorem: value-optionp-of-eval-literal

(defthm value-optionp-of-eval-literal
  (b* ((result (eval-literal lit curve)))
    (value-optionp result))
  :rule-classes :rewrite)

Theorem: eval-literal-of-literal-fix-lit

(defthm eval-literal-of-literal-fix-lit
  (equal (eval-literal (literal-fix lit) curve)
         (eval-literal lit curve)))

Theorem: eval-literal-literal-equiv-congruence-on-lit

(defthm eval-literal-literal-equiv-congruence-on-lit
  (implies (literal-equiv lit lit-equiv)
           (equal (eval-literal lit curve)
                  (eval-literal lit-equiv curve)))
  :rule-classes :congruence)

Theorem: eval-literal-of-curve-fix-curve

(defthm eval-literal-of-curve-fix-curve
  (equal (eval-literal lit (curve-fix curve))
         (eval-literal lit curve)))

Theorem: eval-literal-curve-equiv-congruence-on-curve

(defthm eval-literal-curve-equiv-congruence-on-curve
  (implies (curve-equiv curve curve-equiv)
           (equal (eval-literal lit curve)
                  (eval-literal lit curve-equiv)))
  :rule-classes :congruence)