Extracts Yul IR surface syntax strings from the file named by
Function:
(defun solc-json-file-to-irs (json-filename state) (declare (xargs :stobjs (state))) (declare (xargs :guard (stringp json-filename))) (let ((__function__ 'solc-json-file-to-irs)) (declare (ignorable __function__)) (b* (((mv erp j state) (acl2::parse-file-as-json json-filename state)) ((when erp) (mv t '("" . "") state)) ((mv erp tj) (json::parsed-to-value j)) ((when erp) (mv t '("" . "") state)) ((mv erp ir-pair) (json-to-irs tj)) ((when (or erp (not (consp ir-pair)))) (mv t '("" . "") state))) (mv nil ir-pair state))))
Theorem:
(defthm booleanp-of-solc-json-file-to-irs.erp (b* (((mv ?erp ?irs-pair acl2::?state) (solc-json-file-to-irs json-filename state))) (booleanp erp)) :rule-classes :rewrite)
Theorem:
(defthm consp-of-solc-json-file-to-irs.irs-pair (b* (((mv ?erp ?irs-pair acl2::?state) (solc-json-file-to-irs json-filename state))) (consp irs-pair)) :rule-classes :rewrite)