• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Set
      • Soft
      • C
      • Bv
      • Imp-language
      • Event-macros
      • Java
      • Bitcoin
      • Ethereum
        • Mmp-trees
        • Semaphore
        • Database
        • Cryptography
        • Rlp
          • Rlp-tree
          • Rlp-decoding-executable
            • Rlp-error
            • Rlp-parse-tree
            • Rlp-decodex-tree
            • Maybe-rlp-error
            • Rlp-decodex-bytes
            • Rlp-decodex-scalar
          • Rlp-decodability
          • Rlp-encoding
          • Rlp-decoding-declarative
          • Rlp-big-endian-representations
        • Transactions
        • Hex-prefix
        • Basics
        • Addresses
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Lists-light
      • Axe
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Rlp-decoding-executable

Rlp-decodex-scalar

Executable RLP decoding of a scalar.

Signature

(rlp-decodex-scalar encoding) → (mv error? scalar)

Arguments

encoding — Guard (byte-listp encoding).

Returns

error? — Type (maybe-rlp-error-p error?).

scalar — Type (natp scalar).

This has the same form as the alternative definition rule of rlp-decode-scalar in terms of rlp-decode-bytes. As such, it is immediate to prove equal (i.e. correct with respect) to rlp-decode-scalar, using the correctness theorem of rlp-decodex-bytes.

Definitions and Theorems

Function: rlp-decodex-scalar

(defun rlp-decodex-scalar (encoding)
  (declare (xargs :guard (byte-listp encoding)))
  (let ((__function__ 'rlp-decodex-scalar))
    (declare (ignorable __function__))
    (b* (((mv error? bytes)
          (rlp-decodex-bytes encoding))
         ((when error?) (mv error? 0))
         ((unless (equal (trim-bendian* bytes) bytes))
          (mv (rlp-error-leading-zeros-in-scalar bytes)
              0))
         (scalar (bebytes=>nat bytes)))
      (mv nil scalar))))

Theorem: maybe-rlp-error-p-of-rlp-decodex-scalar.error?

(defthm maybe-rlp-error-p-of-rlp-decodex-scalar.error?
  (b* (((mv ?error? ?scalar)
        (rlp-decodex-scalar encoding)))
    (maybe-rlp-error-p error?))
  :rule-classes :rewrite)

Theorem: natp-of-rlp-decodex-scalar.scalar

(defthm natp-of-rlp-decodex-scalar.scalar
  (b* (((mv ?error? ?scalar)
        (rlp-decodex-scalar encoding)))
    (natp scalar))
  :rule-classes :rewrite)

Theorem: rlp-decode-scalar-is-rlp-decodex-scalar

(defthm rlp-decode-scalar-is-rlp-decodex-scalar
  (and (iff (mv-nth 0 (rlp-decode-scalar encoding))
            (mv-nth 0 (rlp-decodex-scalar encoding)))
       (equal (mv-nth 1 (rlp-decode-scalar encoding))
              (mv-nth 1 (rlp-decodex-scalar encoding)))))

Theorem: rlp-decodex-scalar-of-byte-list-fix-encoding

(defthm rlp-decodex-scalar-of-byte-list-fix-encoding
  (equal (rlp-decodex-scalar (byte-list-fix encoding))
         (rlp-decodex-scalar encoding)))

Theorem: rlp-decodex-scalar-byte-list-equiv-congruence-on-encoding

(defthm rlp-decodex-scalar-byte-list-equiv-congruence-on-encoding
  (implies (byte-list-equiv encoding encoding-equiv)
           (equal (rlp-decodex-scalar encoding)
                  (rlp-decodex-scalar encoding-equiv)))
  :rule-classes :congruence)