Evaluate a Leo literal.
(eval-literal lit curve) → 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
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.
Function:
(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:
(defthm value-optionp-of-eval-literal (b* ((result (eval-literal lit curve))) (value-optionp result)) :rule-classes :rewrite)
Theorem:
(defthm eval-literal-of-literal-fix-lit (equal (eval-literal (literal-fix lit) curve) (eval-literal lit curve)))
Theorem:
(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:
(defthm eval-literal-of-curve-fix-curve (equal (eval-literal lit (curve-fix curve)) (eval-literal lit curve)))
Theorem:
(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)