		Search-engine friendly clone of the ACL2 documentation.

Parse-yul-json

Json-to-irs

Extracts Yul IR surface syntax strings from a JSON fty structure.

Signature
(json-to-irs yul-object-json) → (mv erp irs-pair)
Arguments: yul-object-json — Guard (json::valuep yul-object-json).
Returns: erp — Type (booleanp erp).; irs-pair — Type (consp irs-pair).

Definitions and Theorems

Function: json-to-irs

(defun json-to-irs (yul-object-json)
 (declare (xargs :guard (json::valuep yul-object-json)))
 (let ((__function__ 'json-to-irs))
  (declare (ignorable __function__))
  (b*
   (((unless (and (json::valuep yul-object-json)
                  (json::value-case yul-object-json :object)))
     (mv t '("" . "")))
    ((json::pattern
      (:object
       (:member
        "contracts"
        (:object
         (:member
          _
          (:object
           (:member
               "object"
               (:object (:member "evm" _)
                        (:member "ir" (:string ir-string))
                        (:member "irOptimized"
                                 (:string iroptimized-string))))))))
       *..))
     yul-object-json)
    ((unless (and json::match? (stringp ir-string)
                  (stringp iroptimized-string)))
     (mv t '("" . ""))))
   (mv nil
       (cons ir-string iroptimized-string)))))

Theorem: booleanp-of-json-to-irs.erp

(defthm booleanp-of-json-to-irs.erp
  (b* (((mv ?erp ?irs-pair)
        (json-to-irs yul-object-json)))
    (booleanp erp))
  :rule-classes :rewrite)

Theorem: consp-of-json-to-irs.irs-pair

(defthm consp-of-json-to-irs.irs-pair
  (b* (((mv ?erp ?irs-pair)
        (json-to-irs yul-object-json)))
    (consp irs-pair))
  :rule-classes :rewrite)