• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • Acre
    • Milawa
    • Smtlink
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • C
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • Java
    • Riscv
    • Taspi
    • Bitcoin
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
    • Where-do-i-place-my-book
    • Axe
    • Aleo
      • Aleobft
      • Aleovm
      • Leo
        • Grammar
        • Early-version
          • Json2ast
          • Testing
          • Definition
            • Flattening
            • Abstract-syntax
            • Dynamic-semantics
              • Execution
              • Values
              • Dynamic-environments
              • Arithmetic-operations
                • Integer-arithmetic-operations
                • Field-arithmetic-operations
                • Scalar-field-arithmetic-operations
                  • Op-scalar-add
                  • Op-scalar-neg
                • Group-arithmetic-operations
                • Op-mul
                • Op-add
                • Op-sub-wrapped
                • Op-sub
                • Op-rem-wrapped
                • Op-pow-wrapped
                • Op-pow
                • Op-mul-wrapped
                • Op-div-wrapped
                • Op-div
                • Op-add-wrapped
                • Op-rem
                • Op-square-root
                • Op-square
                • Op-neg
                • Op-inv
                • Op-double
                • Op-abs-wrapped
                • Op-abs
              • Curve-parameterization
              • Shift-operations
              • Errors
              • Value-expressions
              • Locations
              • Input-execution
              • Edwards-bls12-generator
              • Equality-operations
              • Logical-operations
              • Program-execution
              • Ordering-operations
              • Bitwise-operations
              • Literal-evaluation
              • Type-maps-for-struct-components
              • Output-execution
              • Tuple-operations
              • Struct-operations
            • Compilation
            • Static-semantics
            • Concrete-syntax
    • Bigmems
    • Builtins
    • Execloader
    • Solidity
    • Paco
    • Concurrent-programs
    • Bls12-377-curves
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Scalar-field-arithmetic-operations

Op-scalar-add

Leo scalar field value addition operation.

Signature

(op-scalar-add left right curve) → result

Arguments

left — Guard (valuep left).

right — Guard (valuep right).

curve — Guard (curvep curve).

Returns

result — Type (value-resultp result).

Definitions and Theorems

Function: op-scalar-add

(defun op-scalar-add (left right curve)
  (declare (xargs :guard (and (valuep left)
                              (valuep right)
                              (curvep curve))))
  (declare (xargs :guard (and (value-case left :scalar)
                              (value-case right :scalar))))
  (let ((__function__ 'op-scalar-add))
    (declare (ignorable __function__))
    (b* ((r (curve-scalar-prime curve))
         (err (list :op-scalar-add (value-fix left)
                    (value-fix right)))
         (x (value-scalar->get left))
         (y (value-scalar->get right))
         ((unless (pfield::fep x r))
          (reserrf err))
         ((unless (pfield::fep y r))
          (reserrf err)))
      (value-scalar (pfield::add x y r)))))

Theorem: value-resultp-of-op-scalar-add

(defthm value-resultp-of-op-scalar-add
  (b* ((result (op-scalar-add left right curve)))
    (value-resultp result))
  :rule-classes :rewrite)

Theorem: op-scalar-add-of-value-fix-left

(defthm op-scalar-add-of-value-fix-left
  (equal (op-scalar-add (value-fix left)
                        right curve)
         (op-scalar-add left right curve)))

Theorem: op-scalar-add-value-equiv-congruence-on-left

(defthm op-scalar-add-value-equiv-congruence-on-left
  (implies (value-equiv left left-equiv)
           (equal (op-scalar-add left right curve)
                  (op-scalar-add left-equiv right curve)))
  :rule-classes :congruence)

Theorem: op-scalar-add-of-value-fix-right

(defthm op-scalar-add-of-value-fix-right
  (equal (op-scalar-add left (value-fix right)
                        curve)
         (op-scalar-add left right curve)))

Theorem: op-scalar-add-value-equiv-congruence-on-right

(defthm op-scalar-add-value-equiv-congruence-on-right
  (implies (value-equiv right right-equiv)
           (equal (op-scalar-add left right curve)
                  (op-scalar-add left right-equiv curve)))
  :rule-classes :congruence)

Theorem: op-scalar-add-of-curve-fix-curve

(defthm op-scalar-add-of-curve-fix-curve
  (equal (op-scalar-add left right (curve-fix curve))
         (op-scalar-add left right curve)))

Theorem: op-scalar-add-curve-equiv-congruence-on-curve

(defthm op-scalar-add-curve-equiv-congruence-on-curve
  (implies (curve-equiv curve curve-equiv)
           (equal (op-scalar-add left right curve)
                  (op-scalar-add left right curve-equiv)))
  :rule-classes :congruence)