• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Abnf
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Soft
      • Bv
      • Imp-language
      • Event-macros
      • C
      • Java
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Number-theory
      • 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
      • Lists-light
      • Builtins
      • Axe
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Attachments

Hmac-sha-512-attachment

Executable attachment for the HMAC-SHA-512 interface.

We define a wrapper of the executable definition and attach the wrapper to the constrained function. The wrapper serves to use the fixtypes for byte lists, to fix the inputs accordingly, and to convert the text input to bits as required by the executable definition (while the key is in bytes).

Definitions and Theorems

Function: hmac-sha-512-wrapper

(defun hmac-sha-512-wrapper (key text)
  (declare (xargs :guard (and (byte-listp key)
                              (byte-listp text))))
  (declare (xargs :guard (and (< (len key) (expt 2 125))
                              (< (len text) (- (expt 2 125) 128)))))
  (let ((__function__ 'hmac-sha-512-wrapper))
    (declare (ignorable __function__))
    (b* ((key (mbe :logic (byte-list-fix key)
                   :exec key))
         (text (mbe :logic (byte-list-fix text)
                    :exec text))
         (text-bits (bebytes=>bits text)))
      (hmac::hmac-sha-512 key text-bits))))

Theorem: byte-listp-of-hmac-sha-512-wrapper

(defthm byte-listp-of-hmac-sha-512-wrapper
  (b* ((result (hmac-sha-512-wrapper key text)))
    (byte-listp result))
  :rule-classes :rewrite)

Theorem: len-of-hmac-sha-512-wrapper

(defthm len-of-hmac-sha-512-wrapper
  (equal (len (hmac-sha-512-wrapper key text))
         64))

Theorem: hmac-sha-512-wrapper-of-byte-list-fix-key

(defthm hmac-sha-512-wrapper-of-byte-list-fix-key
  (equal (hmac-sha-512-wrapper (byte-list-fix key)
                               text)
         (hmac-sha-512-wrapper key text)))

Theorem: hmac-sha-512-wrapper-byte-list-equiv-congruence-on-key

(defthm hmac-sha-512-wrapper-byte-list-equiv-congruence-on-key
  (implies (byte-list-equiv key key-equiv)
           (equal (hmac-sha-512-wrapper key text)
                  (hmac-sha-512-wrapper key-equiv text)))
  :rule-classes :congruence)

Theorem: hmac-sha-512-wrapper-of-byte-list-fix-text

(defthm hmac-sha-512-wrapper-of-byte-list-fix-text
  (equal (hmac-sha-512-wrapper key (byte-list-fix text))
         (hmac-sha-512-wrapper key text)))

Theorem: hmac-sha-512-wrapper-byte-list-equiv-congruence-on-text

(defthm hmac-sha-512-wrapper-byte-list-equiv-congruence-on-text
  (implies (byte-list-equiv text text-equiv)
           (equal (hmac-sha-512-wrapper key text)
                  (hmac-sha-512-wrapper key text-equiv)))
  :rule-classes :congruence)