• 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
    • Taspi
    • Bitcoin
    • Riscv
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
      • R1cs
      • Interfaces
      • Sha-2
      • Keccak
      • Kdf
      • Mimc
      • Padding
      • Hmac
      • Elliptic-curves
      • Attachments
        • Secp256k1-attachment
        • Secp256k1-ecdsa-attachment
        • Pbkdf2-hmac-sha-512-attachment
        • Hmac-sha-512-attachment
        • Sha-256-attachment
        • Keccak-256-attachment
      • Elliptic-curve-digital-signature-algorithm
    • Poseidon
    • Where-do-i-place-my-book
    • Axe
    • Bigmems
    • Builtins
    • Execloader
    • Aleo
    • Solidity
    • Paco
    • Concurrent-programs
    • Bls12-377-curves
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Attachments
• Elliptic-curve-digital-signature-algorithm

Secp256k1-ecdsa-attachment

Executable attachment for the ECDSA interface for the curve secp256k1.

We define a wrapper of the secp256k1 deterministic signature definition with public key recovery, and attach the wrapper to the constrained function. The wrapper serves to use the fixtypes for byte lists and to fix all the inputs and convert bytes to bits as required by the signature definition.

Definitions and Theorems

Function: secp256k1-sign-det-rec-wrapper

(defun secp256k1-sign-det-rec-wrapper (hash key small-x? small-s?)
  (declare (xargs :guard (and (byte-listp hash)
                              (secp256k1-priv-key-p key)
                              (booleanp small-x?)
                              (booleanp small-s?))))
  (let ((acl2::__function__ 'secp256k1-sign-det-rec-wrapper))
    (declare (ignorable acl2::__function__))
    (b* ((key (mbe :logic (secp256k1-priv-key-fix key)
                   :exec key))
         (small-x? (mbe :logic (bool-fix small-x?)
                        :exec small-x?))
         (small-s? (mbe :logic (bool-fix small-s?)
                        :exec small-s?))
         (hash-bits (bebytes=>bits hash))
         ((mv error? x-index y-even? r s)
          (ecdsa-sign-deterministic-prehashed
               hash-bits key small-x? small-s?))
         ((when error?) (mv t 0 nil 0 0)))
      (mv nil x-index y-even? r s))))

Theorem: booleanp-of-secp256k1-sign-det-rec-wrapper.error?

(defthm booleanp-of-secp256k1-sign-det-rec-wrapper.error?
 (b* (((mv ?error? ?x-index ?y-even? ?r ?s)
       (secp256k1-sign-det-rec-wrapper hash key small-x? small-s?)))
   (booleanp error?))
 :rule-classes :rewrite)

Theorem: natp-of-secp256k1-sign-det-rec-wrapper.x-index

(defthm natp-of-secp256k1-sign-det-rec-wrapper.x-index
 (b* (((mv ?error? ?x-index ?y-even? ?r ?s)
       (secp256k1-sign-det-rec-wrapper hash key small-x? small-s?)))
   (natp x-index))
 :rule-classes :rewrite)

Theorem: booleanp-of-secp256k1-sign-det-rec-wrapper.y-even?

(defthm booleanp-of-secp256k1-sign-det-rec-wrapper.y-even?
 (b* (((mv ?error? ?x-index ?y-even? ?r ?s)
       (secp256k1-sign-det-rec-wrapper hash key small-x? small-s?)))
   (booleanp y-even?))
 :rule-classes :rewrite)

Theorem: secp256k1-fieldp-of-secp256k1-sign-det-rec-wrapper.r

(defthm secp256k1-fieldp-of-secp256k1-sign-det-rec-wrapper.r
 (b* (((mv ?error? ?x-index ?y-even? ?r ?s)
       (secp256k1-sign-det-rec-wrapper hash key small-x? small-s?)))
   (secp256k1-fieldp r))
 :rule-classes :rewrite)

Theorem: secp256k1-fieldp-of-secp256k1-sign-det-rec-wrapper.s

(defthm secp256k1-fieldp-of-secp256k1-sign-det-rec-wrapper.s
 (b* (((mv ?error? ?x-index ?y-even? ?r ?s)
       (secp256k1-sign-det-rec-wrapper hash key small-x? small-s?)))
   (secp256k1-fieldp s))
 :rule-classes :rewrite)

Theorem: secp256k1-sign-det-rec-wrapper-of-byte-list-fix-hash

(defthm secp256k1-sign-det-rec-wrapper-of-byte-list-fix-hash
  (equal
       (secp256k1-sign-det-rec-wrapper (byte-list-fix hash)
                                       key small-x? small-s?)
       (secp256k1-sign-det-rec-wrapper hash key small-x? small-s?)))

Theorem: secp256k1-sign-det-rec-wrapper-byte-list-equiv-congruence-on-hash

(defthm
  secp256k1-sign-det-rec-wrapper-byte-list-equiv-congruence-on-hash
 (implies
  (byte-list-equiv hash hash-equiv)
  (equal (secp256k1-sign-det-rec-wrapper hash key small-x? small-s?)
         (secp256k1-sign-det-rec-wrapper
              hash-equiv key small-x? small-s?)))
 :rule-classes :congruence)

Theorem: secp256k1-sign-det-rec-wrapper-of-secp256k1-priv-key-fix-key

(defthm secp256k1-sign-det-rec-wrapper-of-secp256k1-priv-key-fix-key
 (equal
   (secp256k1-sign-det-rec-wrapper hash (secp256k1-priv-key-fix key)
                                   small-x? small-s?)
   (secp256k1-sign-det-rec-wrapper hash key small-x? small-s?)))

Theorem: secp256k1-sign-det-rec-wrapper-secp256k1-priv-key-equiv-congruence-on-key

(defthm
 secp256k1-sign-det-rec-wrapper-secp256k1-priv-key-equiv-congruence-on-key
 (implies
  (secp256k1-priv-key-equiv key key-equiv)
  (equal (secp256k1-sign-det-rec-wrapper hash key small-x? small-s?)
         (secp256k1-sign-det-rec-wrapper
              hash key-equiv small-x? small-s?)))
 :rule-classes :congruence)

Theorem: secp256k1-sign-det-rec-wrapper-of-bool-fix-small-x?

(defthm secp256k1-sign-det-rec-wrapper-of-bool-fix-small-x?
  (equal
       (secp256k1-sign-det-rec-wrapper hash key (bool-fix small-x?)
                                       small-s?)
       (secp256k1-sign-det-rec-wrapper hash key small-x? small-s?)))

Theorem: secp256k1-sign-det-rec-wrapper-iff-congruence-on-small-x?

(defthm secp256k1-sign-det-rec-wrapper-iff-congruence-on-small-x?
 (implies
  (iff small-x? small-x?-equiv)
  (equal (secp256k1-sign-det-rec-wrapper hash key small-x? small-s?)
         (secp256k1-sign-det-rec-wrapper
              hash key small-x?-equiv small-s?)))
 :rule-classes :congruence)

Theorem: secp256k1-sign-det-rec-wrapper-of-bool-fix-small-s?

(defthm secp256k1-sign-det-rec-wrapper-of-bool-fix-small-s?
  (equal
       (secp256k1-sign-det-rec-wrapper
            hash key small-x? (bool-fix small-s?))
       (secp256k1-sign-det-rec-wrapper hash key small-x? small-s?)))

Theorem: secp256k1-sign-det-rec-wrapper-iff-congruence-on-small-s?

(defthm secp256k1-sign-det-rec-wrapper-iff-congruence-on-small-s?
 (implies
  (iff small-s? small-s?-equiv)
  (equal (secp256k1-sign-det-rec-wrapper hash key small-x? small-s?)
         (secp256k1-sign-det-rec-wrapper
              hash key small-x? small-s?-equiv)))
 :rule-classes :congruence)