From 4ac800a2c1307c9f39e5b562498a974e84b38462 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 5 Dec 2024 16:59:28 +0700 Subject: [PATCH 1/4] feat: new scenario/CRATE_load_createe_account shorthand --- hub/constraints/scenario-rows/shorthands/create.lisp | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/hub/constraints/scenario-rows/shorthands/create.lisp b/hub/constraints/scenario-rows/shorthands/create.lisp index 886ad6a8..775fedd8 100644 --- a/hub/constraints/scenario-rows/shorthands/create.lisp +++ b/hub/constraints/scenario-rows/shorthands/create.lisp @@ -105,7 +105,14 @@ ;;  CREATE/compute_deployment_address (defun (scenario-shorthand---CREATE---compute-deployment-address) - (+ + (+ + (scenario-shorthand---CREATE---failure-condition) + (scenario-shorthand---CREATE---not-rebuffed) + )) + +;;  CREATE/load_createe_account +(defun (scenario-shorthand---CREATE---load-createe-account) + (+ (scenario-shorthand---CREATE---failure-condition) (scenario-shorthand---CREATE---not-rebuffed) )) From 4a74e38641822e790290343f45b20be358271a1d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 5 Dec 2024 17:00:10 +0700 Subject: [PATCH 2/4] feat: using that shorthand --- .../create/constraints/generalities.lisp | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/hub/constraints/instruction-handling/create/constraints/generalities.lisp b/hub/constraints/instruction-handling/create/constraints/generalities.lisp index 1b4d2cb3..44fa21a8 100644 --- a/hub/constraints/instruction-handling/create/constraints/generalities.lisp +++ b/hub/constraints/instruction-handling/create/constraints/generalities.lisp @@ -74,7 +74,9 @@ (create-instruction---MXP-gas) ;; memory expansion gas ))) -(defconstraint create-instruction---setting-the-out-of-gas-exception (:guard (create-instruction---generic-precondition)) +(defconstraint create-instruction---setting-the-out-of-gas-exception + (:guard (create-instruction---generic-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (if-zero (shift misc/STP_FLAG CREATE_miscellaneous_row___row_offset) ;; STP_FLAG ≡ 0 (vanishes! (create-instruction---STACK-oogx)) @@ -83,10 +85,9 @@ (create-instruction---STP-oogx)) )) -(defun (create-instruction---createe-nonce) (* (create-instruction---trigger_RLPADDR) (shift account/NONCE CREATE_first_createe_account_row___row_offset))) -(defun (create-instruction---createe-has-code) (* (create-instruction---trigger_RLPADDR) (shift account/HAS_CODE CREATE_first_createe_account_row___row_offset))) - -(defconstraint create-instruction---setting-the-OOB-instruction (:guard (create-instruction---generic-precondition)) +(defconstraint create-instruction---setting-the-OOB-instruction + (:guard (create-instruction---generic-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (if-not-zero (shift misc/OOB_FLAG CREATE_miscellaneous_row___row_offset) (set-OOB-instruction---create CREATE_miscellaneous_row___row_offset ;; offset (create-instruction---STACK-value-hi) ;; value (high part) @@ -98,6 +99,9 @@ (create-instruction---creator-nonce) ;; creator account nonce ))) +(defun (create-instruction---createe-nonce) (* (scenario-shorthand---CREATE---load-createe-account) (shift account/NONCE CREATE_first_createe_account_row___row_offset))) +(defun (create-instruction---createe-has-code) (* (scenario-shorthand---CREATE---load-createe-account) (shift account/HAS_CODE CREATE_first_createe_account_row___row_offset))) + (defconstraint create-instruction---setting-the-CREATE-scenario---exceptional (:guard (create-instruction---generic-precondition)) (eq! scenario/CREATE_EXCEPTION XAHOY)) From 83a51fc2af4b0e34488ace6058df49e5c446b4ae Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 5 Dec 2024 17:00:21 +0700 Subject: [PATCH 3/4] ras: removed some trailing white space --- .../scenario-rows/shorthands/create.lisp | 42 +++++++++---------- 1 file changed, 21 insertions(+), 21 deletions(-) diff --git a/hub/constraints/scenario-rows/shorthands/create.lisp b/hub/constraints/scenario-rows/shorthands/create.lisp index 775fedd8..2fb21775 100644 --- a/hub/constraints/scenario-rows/shorthands/create.lisp +++ b/hub/constraints/scenario-rows/shorthands/create.lisp @@ -13,7 +13,7 @@ ;;  CREATE/not_rebuffed_empty_init_code (defun (scenario-shorthand---CREATE---not-rebuffed-empty-init-code) - (+ + (+ ;; scenario/CREATE_EXCEPTION ;; scenario/CREATE_ABORT ;; scenario/CREATE_FAILURE_CONDITION_WILL_REVERT @@ -28,7 +28,7 @@ ;;  CREATE/not_rebuffed_nonempty_init_code (defun (scenario-shorthand---CREATE---not-rebuffed-nonempty-init-code) - (+ + (+ ;; scenario/CREATE_EXCEPTION ;; scenario/CREATE_ABORT ;; scenario/CREATE_FAILURE_CONDITION_WILL_REVERT @@ -64,7 +64,7 @@ ;;  CREATE/failure_condition (defun (scenario-shorthand---CREATE---failure-condition) - (+ + (+ ;; scenario/CREATE_EXCEPTION ;; scenario/CREATE_ABORT scenario/CREATE_FAILURE_CONDITION_WILL_REVERT @@ -79,7 +79,7 @@ ;;  CREATE/unexceptional (defun (scenario-shorthand---CREATE---unexceptional) - (+ + (+ scenario/CREATE_ABORT (scenario-shorthand---CREATE---failure-condition) (scenario-shorthand---CREATE---not-rebuffed) @@ -87,7 +87,7 @@ ;;  CREATE/sum (defun (scenario-shorthand---CREATE---sum) - (+ + (+ scenario/CREATE_EXCEPTION (scenario-shorthand---CREATE---unexceptional) )) @@ -119,7 +119,7 @@ ;;  CREATE/no_context_change (defun (scenario-shorthand---CREATE---no-context-change) - (+ + (+ scenario/CREATE_ABORT (scenario-shorthand---CREATE---failure-condition) (scenario-shorthand---CREATE---not-rebuffed-empty-init-code) @@ -139,7 +139,7 @@ ;;  CREATE/deployment-success (defun (scenario-shorthand---CREATE---deployment-success) - (+ + (+ ;; scenario/CREATE_EXCEPTION ;; scenario/CREATE_ABORT ;; scenario/CREATE_FAILURE_CONDITION_WILL_REVERT @@ -154,7 +154,7 @@ ;;  CREATE/deployment_failure (defun (scenario-shorthand---CREATE---deployment-failure) - (+ + (+ ;; scenario/CREATE_EXCEPTION ;; scenario/CREATE_ABORT ;; scenario/CREATE_FAILURE_CONDITION_WILL_REVERT @@ -180,7 +180,7 @@ ;;  CREATE/creator_state_change_will_revert (defun (scenario-shorthand---CREATE---creator-state-change-will-revert) - (+ + (+ ;; scenario/CREATE_EXCEPTION ;; scenario/CREATE_ABORT scenario/CREATE_FAILURE_CONDITION_WILL_REVERT @@ -195,7 +195,7 @@ ;;  CREATE/creator_state_change_wont_revert (defun (scenario-shorthand---CREATE---creator-state-change-wont-revert) - (+ + (+ ;; scenario/CREATE_EXCEPTION ;; scenario/CREATE_ABORT ;; scenario/CREATE_FAILURE_CONDITION_WILL_REVERT @@ -210,14 +210,14 @@ ;;  CREATE/creator_state_change (defun (scenario-shorthand---CREATE---creator-state-change) - (+ + (+ (scenario-shorthand---CREATE---failure-condition) (scenario-shorthand---CREATE---not-rebuffed) )) ;;  CREATE/no_creator_state_change (defun (scenario-shorthand---CREATE---no-creator-state-change) - (+ + (+ scenario/CREATE_EXCEPTION scenario/CREATE_ABORT )) @@ -235,7 +235,7 @@ ;;  CREATE/simple_revert (defun (scenario-shorthand---CREATE---simple-revert) - (+ + (+ ;; scenario/CREATE_EXCEPTION ;; scenario/CREATE_ABORT scenario/CREATE_FAILURE_CONDITION_WILL_REVERT @@ -251,7 +251,7 @@ ;; ;;  CREATE/execution_will_revert ;; (defun (scenario-shorthand---CREATE---execution-will-revert) -;; (+ +;; (+ ;; ;; scenario/CREATE_EXCEPTION ;; ;; scenario/CREATE_ABORT ;; ;; scenario/CREATE_FAILURE_CONDITION_WILL_REVERT @@ -266,7 +266,7 @@ ;; ;; ;;  CREATE/execution_wont_revert ;; (defun (scenario-shorthand---CREATE---execution-wont-revert) -;; (+ +;; (+ ;; ;; scenario/CREATE_EXCEPTION ;; ;; scenario/CREATE_ABORT ;; ;; scenario/CREATE_FAILURE_CONDITION_WILL_REVERT @@ -281,7 +281,7 @@ ;; ;; ;;  CREATE/empty_init_code ;; (defun (scenario-shorthand---CREATE---empty-init-code) -;; (+ +;; (+ ;; ;; scenario/CREATE_EXCEPTION ;; ;; scenario/CREATE_ABORT ;; ;; scenario/CREATE_FAILURE_CONDITION_WILL_REVERT @@ -296,7 +296,7 @@ ;; ;; ;;  CREATE/nonempty_init_code ;; (defun (scenario-shorthand---CREATE---nonempty-init-code) -;; (+ +;; (+ ;; ;; scenario/CREATE_EXCEPTION ;; ;; scenario/CREATE_ABORT ;; ;; scenario/CREATE_FAILURE_CONDITION_WILL_REVERT @@ -311,7 +311,7 @@ ;; ;; ;;  CREATE/execution ;; (defun (scenario-shorthand---CREATE---execution) -;; (+ +;; (+ ;; (scenario-shorthand---CREATE---nonempty-init-code) ;; (scenario-shorthand---CREATE---empty-init-code) ;; ;; scenario/CREATE_EXCEPTION @@ -328,7 +328,7 @@ ;; ;; ;;  CREATE/undo_account_operations ;; (defun (scenario-shorthand---CREATE---undo-account-operations) -;; (+ +;; (+ ;; ;; scenario/CREATE_EXCEPTION ;; ;; scenario/CREATE_ABORT ;; ;; scenario/CREATE_FAILURE_CONDITION_WILL_REVERT @@ -343,7 +343,7 @@ ;; ;; ;;  CREATE/deployment_success ;; (defun (scenario-shorthand---CREATE---deployment-success) -;; (+ +;; (+ ;; ;; scenario/CREATE_EXCEPTION ;; ;; scenario/CREATE_ABORT ;; ;; scenario/CREATE_FAILURE_CONDITION_WILL_REVERT @@ -359,7 +359,7 @@ ;; ;;  CREATE/ ;; (defun (scenario-shorthand---CREATE---) -;; (+ +;; (+ ;; scenario/CREATE_EXCEPTION ;; scenario/CREATE_ABORT ;; scenario/CREATE_FAILURE_CONDITION_WILL_REVERT From 708955f94e9008de87fd43c0aae8fe94ac3443ba Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 5 Dec 2024 17:26:53 +0700 Subject: [PATCH 4/4] ras: merged master --- alu/add/columns.lisp | 2 +- alu/add/constraints.lisp | 2 +- alu/ext/columns.lisp | 2 +- alu/ext/constraints.lisp | 4 +- alu/mod/columns.lisp | 2 +- alu/mod/constants.lisp | 2 +- alu/mul/constraints.lisp | 2 +- bin/columns.lisp | 4 +- bin/constraints.lisp | 6 +-- bin/lookups/bin_into_binreftable.lisp | 8 ++-- blake2fmodexpdata/columns.lisp | 2 +- blake2fmodexpdata/constants.lisp | 2 +- .../lookups/blakemodexp_into_wcp.lisp | 2 +- blockdata/columns.lisp | 2 +- blockdata/constants.lisp | 2 +- blockdata/constraints.lisp | 14 +++--- blockdata/lookups/blockdata_into_txndata.lisp | 2 +- blockdata/lookups/blockdata_into_wcp.lisp | 2 +- blockhash/columns.lisp | 2 +- .../lookups/blockhash_into_blockdata.lisp | 2 +- blockhash/lookups/blockhash_into_wcp_lex.lisp | 2 +- .../blockhash_into_wcp_lower_bound.lisp | 2 +- .../blockhash_into_wcp_upper_bound.lisp | 2 +- constants/constants.lisp | 4 +- ecdata/columns.lisp | 4 +- ecdata/constants.lisp | 2 +- ecdata/constraints.lisp | 2 +- ecdata/lookups/ecdata_into_ext.lisp | 2 +- ecdata/lookups/ecdata_into_wcp.lisp | 2 +- euc/columns.lisp | 2 +- euc/constraints.lisp | 2 +- euc/lookups/euc_into_wcp.lisp | 2 +- exp/columns.lisp | 2 +- exp/constants.lisp | 2 +- exp/constraints.lisp | 6 +-- exp/lookups/exp-into-wcp.lisp | 2 +- gas/columns.lisp | 4 +- gas/lookups/gas-into-wcp.lisp | 2 +- hub/columns/miscellaneous.lisp | 4 +- hub/columns/shared.lisp | 4 +- hub/columns/storage.lisp | 4 +- hub/columns/transaction.lisp | 2 +- hub/constraints/account.lisp | 12 ++--- hub/constraints/consistencies.lisp | 2 +- .../consistency/context/columns.lisp | 2 +- .../consistency/context/constraints.lisp | 2 +- .../execution_environment/constraints.lisp | 2 +- .../consistency/storage/columns.lisp | 2 +- hub/constraints/context-rows/specialized.lisp | 4 +- .../heartbeat/constancy_conditions.lisp | 2 +- .../add_bin_ext_mod_mul_shf_wcp.lisp | 6 +-- hub/constraints/instruction-handling/btc.lisp | 2 +- .../generalities/1st_set_of_account_rows.lisp | 2 +- .../call/generalities/universal.lisp | 4 +- .../call/precompiles/blake/success.lisp | 2 +- .../call/precompiles/common/constants.lisp | 2 +- .../call/precompiles/flag_sums_and_NSRs.lisp | 12 ++--- .../call/precompiles/modexp/common.lisp | 4 +- .../instruction-handling/halting/return.lisp | 2 +- .../halting/selfdestruct.lisp | 2 +- hub/constraints/instruction-handling/log.lisp | 2 +- hub/constraints/instruction-handling/sto.lisp | 2 +- .../scenario-rows/shorthands/call.lisp | 44 +++++++++---------- .../scenario-rows/shorthands/precompile.lisp | 16 +++---- .../scenario-rows/shorthands/return.lisp | 2 +- hub/constraints/storage-rows/specialized.lisp | 2 +- hub/constraints/tx_finl/constraints.lisp | 2 +- hub/constraints/tx_skip/constraints.lisp | 4 +- hub/lookups/hub_into_add.lisp | 2 +- hub/lookups/hub_into_block_hash.lisp | 2 +- hub/lookups/hub_into_exp.lisp | 4 +- hub/lookups/hub_into_instruction_decoder.lisp | 2 +- hub/lookups/hub_into_log_info.lisp | 2 +- hub/lookups/hub_into_mxp.lisp | 2 +- hub/lookups/hub_into_oob.lisp | 2 +- hub/lookups/hub_into_rlp_addr.lisp | 4 +- hub/lookups/hub_into_rlp_txn.lisp | 2 +- .../hub_into_rom_instruction_fetching.lisp | 2 +- ...hub_into_rom_jump_destination_vetting.lisp | 2 +- hub/lookups/hub_into_rom_lex.lisp | 4 +- hub/lookups/hub_into_stp.lisp | 2 +- hub/lookups/hub_into_trm.lisp | 2 +- hub/lookups/hub_into_wcp.lisp | 2 +- .../hub_into_wcp_for_stack_overflow.lisp | 2 +- logdata/columns.lisp | 2 +- logdata/lookups/logdata-to-rlprcpt.lisp | 2 +- loginfo/columns.lisp | 2 +- loginfo/lookups/loginfo-into-logdata.lisp | 2 +- loginfo/lookups/loginfo-into-rlprcpt.lisp | 2 +- mmio/columns.lisp | 6 +-- mmio/consistency.lisp | 12 ++--- mmio/lookups/mmio_into_blakemodexp.lisp | 2 +- mmio/lookups/mmio_into_ecdata.lisp | 2 +- mmio/lookups/mmio_into_kec.lisp | 2 +- mmio/lookups/mmio_into_logdata.lisp | 2 +- mmio/lookups/mmio_into_mmu.lisp | 2 +- mmio/lookups/mmio_into_ripsha.lisp | 4 +- mmio/lookups/mmio_into_rlptxn.lisp | 2 +- mmio/lookups/mmio_into_rom.lisp | 2 +- mmu/columns.lisp | 4 +- mmu/constants.lisp | 2 +- .../any_to_ram_with_padding/common.lisp | 2 +- mmu/instructions/exo_to_ram_transplant.lisp | 4 +- mmu/instructions/modexp_zero.lisp | 4 +- mmu/lookups/mmu_into_euc.lisp | 2 +- mmu/lookups/mmu_into_mmio.lisp | 2 +- mmu/lookups/mmu_into_wcp.lisp | 2 +- mxp/columns.lisp | 4 +- mxp/constants.lisp | 2 +- mxp/constraints.lisp | 24 +++++----- mxp/lookups/mxp_into_instdecoder.lisp | 12 ++--- oob/columns.lisp | 2 +- oob/constants.lisp | 2 +- oob/constraints.lisp | 2 +- oob/lookups/oob-into-add.lisp | 2 +- oob/lookups/oob-into-mod.lisp | 2 +- oob/lookups/oob-into-wcp.lisp | 2 +- reftables/bin_reftable.lisp | 2 +- reftables/shf_reftable.lisp | 2 +- rlpaddr/columns.lisp | 4 +- rlpaddr/constants.lisp | 2 +- rlpaddr/lookups/rlpaddr_into_trm.lisp | 2 +- rlptxn/columns.lisp | 4 +- rlptxn/constants.lisp | 2 +- rlptxn/lookups/rlptxn_into_rom.lisp | 2 +- rlptxrcpt/columns.lisp | 4 +- rlptxrcpt/constants.lisp | 2 +- rlptxrcpt/constraints.lisp | 2 +- rom/columns.lisp | 4 +- rom/lookups/rom_into_instdecoder.lisp | 2 +- romlex/columns.lisp | 4 +- romlex/lookups/romLex_into_rom.lisp | 2 +- shakiradata/columns.lisp | 2 +- shakiradata/constants.lisp | 2 +- .../shakira_into_wcp_increasing_id.lisp | 8 ++-- .../shakira_into_wcp_nonzero_last_nbytes.lisp | 2 +- .../shakira_into_wcp_small_last_nbytes.lisp | 2 +- shf/columns.lisp | 4 +- shf/lookups/shf_into_shfRT.lisp | 8 ++-- stp/columns.lisp | 4 +- stp/constraints.lisp | 4 +- stp/lookups/stp_into_mod.lisp | 2 +- stp/lookups/stp_into_wcp.lisp | 2 +- trm/columns.lisp | 2 +- txndata/columns.lisp | 4 +- txndata/constants.lisp | 2 +- txndata/lookups/txndata_into_blockdata.lisp | 2 +- txndata/lookups/txndata_into_euc.lisp | 2 +- txndata/lookups/txndata_into_rlpaddr.lisp | 2 +- txndata/lookups/txndata_into_rlptxn.lisp | 2 +- txndata/lookups/txndata_into_rlptxrcpt.lisp | 2 +- txndata/lookups/txndata_into_romlex.lisp | 2 +- txndata/lookups/txndata_into_wcp.lisp | 2 +- wcp/columns.lisp | 4 +- wcp/constraints.lisp | 2 +- 155 files changed, 267 insertions(+), 267 deletions(-) diff --git a/alu/add/columns.lisp b/alu/add/columns.lisp index a365d2bc..8c8dd867 100644 --- a/alu/add/columns.lisp +++ b/alu/add/columns.lisp @@ -1,6 +1,6 @@ (module add) -(defcolumns +(defcolumns (STAMP :i32) (CT_MAX :byte) (CT :byte) diff --git a/alu/add/constraints.lisp b/alu/add/constraints.lisp index d5b7e636..10c4712f 100644 --- a/alu/add/constraints.lisp +++ b/alu/add/constraints.lisp @@ -1,6 +1,6 @@ (module add) -(defconst +(defconst THETA 340282366920938463463374607431768211456) ;; note that 340282366920938463463374607431768211456 = 256^16 (defconstraint stamp-constancies () diff --git a/alu/ext/columns.lisp b/alu/ext/columns.lisp index c7a5bf3a..a7d9ff79 100644 --- a/alu/ext/columns.lisp +++ b/alu/ext/columns.lisp @@ -19,7 +19,7 @@ (OF_I :binary@prove) (OF_J :binary@prove) (OF_H :binary@prove) - (OF_RES :binary@prove) + (OF_RES :binary@prove) ; (BIT_1 :binary@prove) (BIT_2 :binary@prove) diff --git a/alu/ext/constraints.lisp b/alu/ext/constraints.lisp index 602b3708..469409ef 100644 --- a/alu/ext/constraints.lisp +++ b/alu/ext/constraints.lisp @@ -1,6 +1,6 @@ (module ext) -(defconst +(defconst THETA 18446744073709551616 ;18446744073709551616 = 256^8 THETA2 340282366920938463463374607431768211456) ;340282366920938463463374607431768211456 = 256^16 @@ -141,7 +141,7 @@ (defconstraint bit-3-constraints () (if-not-zero STAMP (begin - (if-not-zero ARG_3_HI + (if-not-zero ARG_3_HI ;; ARG_3_HI ≠ 0 (vanishes! BIT_3) ;; ARG_3_HI = 0 diff --git a/alu/mod/columns.lisp b/alu/mod/columns.lisp index da00622d..83515e3c 100644 --- a/alu/mod/columns.lisp +++ b/alu/mod/columns.lisp @@ -1,6 +1,6 @@ (module mod) -(defcolumns +(defcolumns (STAMP :i32) (OLI :binary@prove) (MLI :binary@prove) diff --git a/alu/mod/constants.lisp b/alu/mod/constants.lisp index 580e2a9b..fdea820a 100644 --- a/alu/mod/constants.lisp +++ b/alu/mod/constants.lisp @@ -1,6 +1,6 @@ (module mod) -(defconst +(defconst THETA 18446744073709551616 ;18446744073709551616 = 256^8 THETA2 340282366920938463463374607431768211456 ;340282366920938463463374607431768211456 = 256^16 THETA_SQUARED_OVER_TWO 170141183460469231731687303715884105728) ;170141183460469231731687303715884105728 = (1/2)*THETA2 diff --git a/alu/mul/constraints.lisp b/alu/mul/constraints.lisp index efddcfe6..90af1c53 100644 --- a/alu/mul/constraints.lisp +++ b/alu/mul/constraints.lisp @@ -1,6 +1,6 @@ (module mul) -(defconst +(defconst ONETWOEIGHT 128 ONETWOSEVEN 127 THETA 18446744073709551616 ;18446744073709551616 = 256^8 diff --git a/bin/columns.lisp b/bin/columns.lisp index 807b51eb..e97f1d56 100644 --- a/bin/columns.lisp +++ b/bin/columns.lisp @@ -1,6 +1,6 @@ (module bin) -(defcolumns +(defcolumns (STAMP :i32) (CT_MAX :byte) (COUNTER :byte) @@ -41,7 +41,7 @@ (XXX_BYTE_LO :byte)) ;; aliases -(defalias +(defalias CT COUNTER ARG_1_HI ARGUMENT_1_HI ARG_1_LO ARGUMENT_1_LO diff --git a/bin/constraints.lisp b/bin/constraints.lisp index 1ceedd5a..01c47c8e 100644 --- a/bin/constraints.lisp +++ b/bin/constraints.lisp @@ -71,7 +71,7 @@ (counter-constancy CT NEG) (counter-constancy CT SMALL))) -;; 2.6 byte decompositions +;; 2.6 byte decompositions (defconstraint byte_decompositions () (begin (byte-decomposition CT ACC_1 BYTE_1) (byte-decomposition CT ACC_2 BYTE_2) @@ -80,7 +80,7 @@ (byte-decomposition CT ACC_5 BYTE_5) (byte-decomposition CT ACC_6 BYTE_6))) -;; 2.7 target constraints +;; 2.7 target constraints (defun (requires-byte-decomposition) (+ IS_AND IS_OR @@ -148,7 +148,7 @@ (eq! SMALL 1) (vanishes! SMALL)))) -;; 2.9 pivot constraints +;; 2.9 pivot constraints (defconstraint pivot (:guard CT_MAX) (begin (if-eq IS_BYTE 1 (if-zero LOW_4 diff --git a/bin/lookups/bin_into_binreftable.lisp b/bin/lookups/bin_into_binreftable.lisp index da2230d6..5db4de47 100644 --- a/bin/lookups/bin_into_binreftable.lisp +++ b/bin/lookups/bin_into_binreftable.lisp @@ -1,7 +1,7 @@ (defpurefun (selector-bin-to-binreftable) (+ bin.IS_AND bin.IS_OR bin.IS_XOR bin.IS_NOT)) -(deflookup +(deflookup bin-into-binreftable-high ;reference columns ( @@ -10,7 +10,7 @@ binreftable.INPUT_BYTE_1 binreftable.INPUT_BYTE_2 ) - ;source columns + ;source columns ( (* bin.INST (selector-bin-to-binreftable)) (* bin.XXX_BYTE_HI (selector-bin-to-binreftable)) @@ -18,7 +18,7 @@ (* bin.BYTE_3 (selector-bin-to-binreftable)) )) -(deflookup +(deflookup bin-into-binreftable-low ;reference columns ( @@ -27,7 +27,7 @@ binreftable.INPUT_BYTE_1 binreftable.INPUT_BYTE_2 ) - ;source columns + ;source columns ( (* bin.INST (selector-bin-to-binreftable)) (* bin.XXX_BYTE_LO (selector-bin-to-binreftable)) diff --git a/blake2fmodexpdata/columns.lisp b/blake2fmodexpdata/columns.lisp index 11496e97..87bf291d 100644 --- a/blake2fmodexpdata/columns.lisp +++ b/blake2fmodexpdata/columns.lisp @@ -1,6 +1,6 @@ (module blake2fmodexpdata) -(defcolumns +(defcolumns (STAMP :i10) (ID :i32) (PHASE :byte) diff --git a/blake2fmodexpdata/constants.lisp b/blake2fmodexpdata/constants.lisp index 7250cf89..2cb3d59a 100644 --- a/blake2fmodexpdata/constants.lisp +++ b/blake2fmodexpdata/constants.lisp @@ -1,6 +1,6 @@ (module blake2fmodexpdata) -(defconst +(defconst INDEX_MAX_MODEXP 31 INDEX_MAX_MODEXP_BASE INDEX_MAX_MODEXP INDEX_MAX_MODEXP_EXPONENT INDEX_MAX_MODEXP diff --git a/blake2fmodexpdata/lookups/blakemodexp_into_wcp.lisp b/blake2fmodexpdata/lookups/blakemodexp_into_wcp.lisp index 2d154e75..f3a7d5c5 100644 --- a/blake2fmodexpdata/lookups/blakemodexp_into_wcp.lisp +++ b/blake2fmodexpdata/lookups/blakemodexp_into_wcp.lisp @@ -2,7 +2,7 @@ (force-bool (* (~ blake2fmodexpdata.STAMP) (- blake2fmodexpdata.STAMP (prev blake2fmodexpdata.STAMP))))) -(deflookup +(deflookup blake2fmodexpdata-into-wcp ; target colums (in WCP) ( diff --git a/blockdata/columns.lisp b/blockdata/columns.lisp index 81b926ba..76d7a4e4 100644 --- a/blockdata/columns.lisp +++ b/blockdata/columns.lisp @@ -1,6 +1,6 @@ (module blockdata) -(defcolumns +(defcolumns (FIRST_BLOCK_NUMBER :i48) (CT :i4) (REL_BLOCK :i10) diff --git a/blockdata/constants.lisp b/blockdata/constants.lisp index 5879c999..c7c5949d 100644 --- a/blockdata/constants.lisp +++ b/blockdata/constants.lisp @@ -1,6 +1,6 @@ (module blockdata) -(defconst +(defconst CT_MAX_FOR_BLOCKDATA 6 ;;need to update the lookup into wcp if changed ROW_SHIFT_COINBASE 0 ROW_SHIFT_TIMESTAMP 1 diff --git a/blockdata/constraints.lisp b/blockdata/constraints.lisp index 6d6be0fb..e15bf2a5 100644 --- a/blockdata/constraints.lisp +++ b/blockdata/constraints.lisp @@ -69,7 +69,7 @@ (defun (blockdata---first-row-of-new-block) (- REL_BLOCK (prev REL_BLOCK))) (defconstraint value-constraints---COINBASE (:guard (blockdata---first-row-of-new-block)) - (begin + (begin (eq! (shift INST ROW_SHIFT_COINBASE) EVM_INST_COINBASE) (eq! (shift DATA_HI ROW_SHIFT_COINBASE) COINBASE_HI) (eq! (shift DATA_LO ROW_SHIFT_COINBASE) COINBASE_LO) @@ -87,7 +87,7 @@ (* (^ 256 (- LLARGEMO 11)) (shift [BYTE_HI 11] ROW_SHIFT_COINBASE)))))) (defconstraint value-constraints---TIMESTAMP (:guard (blockdata---first-row-of-new-block)) - (begin + (begin (eq! (shift INST ROW_SHIFT_TIMESTAMP) EVM_INST_TIMESTAMP) (vanishes! (shift DATA_HI ROW_SHIFT_TIMESTAMP)) (vanishes! (+ (* (^ 256 (- LLARGEMO 0)) (shift [BYTE_LO 0] ROW_SHIFT_TIMESTAMP)) @@ -104,7 +104,7 @@ (eq! (shift WCP_FLAG ROW_SHIFT_TIMESTAMP) 1)))) (defconstraint value-constraints---NUMBER (:guard (blockdata---first-row-of-new-block)) - (begin + (begin (eq! (shift INST ROW_SHIFT_NUMBER) EVM_INST_NUMBER) (vanishes! (shift DATA_HI ROW_SHIFT_NUMBER)) (eq! (shift DATA_LO ROW_SHIFT_NUMBER) (+ FIRST_BLOCK_NUMBER (- REL_BLOCK 1))) @@ -120,27 +120,27 @@ (* (^ 256 (- LLARGEMO 9)) (shift [BYTE_LO 9] ROW_SHIFT_NUMBER)))))) (defconstraint value-constraints---DIFFICULTY (:guard (blockdata---first-row-of-new-block)) - (begin + (begin (eq! (shift INST ROW_SHIFT_DIFFICULTY) EVM_INST_DIFFICULTY) (vanishes! (shift DATA_HI ROW_SHIFT_DIFFICULTY)) (eq! (shift DATA_LO ROW_SHIFT_DIFFICULTY) LINEA_DIFFICULTY))) (defconstraint value-constraints---GASLIMIT (:guard (blockdata---first-row-of-new-block)) - (begin + (begin (eq! (shift INST ROW_SHIFT_GASLIMIT) EVM_INST_GASLIMIT) (vanishes! (shift DATA_HI ROW_SHIFT_GASLIMIT)) (eq! (shift DATA_LO ROW_SHIFT_GASLIMIT) LINEA_BLOCK_GAS_LIMIT) (eq! (shift DATA_LO ROW_SHIFT_GASLIMIT) BLOCK_GAS_LIMIT))) (defconstraint value-constraints---CHAINID (:guard (blockdata---first-row-of-new-block)) - (begin + (begin (eq! (shift INST ROW_SHIFT_CHAINID) EVM_INST_CHAINID) (vanishes! (shift DATA_HI ROW_SHIFT_CHAINID)) ;(eq! (shift DATA_LO ROW_SHIFT_CHAINID) LINEA_CHAIN_ID) ;; TODO: this needs some fixing )) (defconstraint value-constraints---BASEFEE (:guard (blockdata---first-row-of-new-block)) - (begin + (begin (eq! (shift INST ROW_SHIFT_BASEFEE) EVM_INST_BASEFEE) (vanishes! (shift DATA_HI ROW_SHIFT_BASEFEE)) (eq! (shift DATA_LO ROW_SHIFT_BASEFEE) LINEA_BASE_FEE) diff --git a/blockdata/lookups/blockdata_into_txndata.lisp b/blockdata/lookups/blockdata_into_txndata.lisp index b9eaf788..a5b6887e 100644 --- a/blockdata/lookups/blockdata_into_txndata.lisp +++ b/blockdata/lookups/blockdata_into_txndata.lisp @@ -1,4 +1,4 @@ -(deflookup +(deflookup blockdata-into-txndata ; target columns ( diff --git a/blockdata/lookups/blockdata_into_wcp.lisp b/blockdata/lookups/blockdata_into_wcp.lisp index 5d15da82..ad277023 100644 --- a/blockdata/lookups/blockdata_into_wcp.lisp +++ b/blockdata/lookups/blockdata_into_wcp.lisp @@ -1,4 +1,4 @@ -(deflookup +(deflookup blockdata-into-wcp ; target columns ( diff --git a/blockhash/columns.lisp b/blockhash/columns.lisp index 86cb1eda..dfa19a97 100644 --- a/blockhash/columns.lisp +++ b/blockhash/columns.lisp @@ -1,6 +1,6 @@ (module blockhash) -(defcolumns +(defcolumns (IOMF :binary) (BLOCK_NUMBER_HI :i128) (BLOCK_NUMBER_LO :i128) diff --git a/blockhash/lookups/blockhash_into_blockdata.lisp b/blockhash/lookups/blockhash_into_blockdata.lisp index 1ef8965a..6400f2bb 100644 --- a/blockhash/lookups/blockhash_into_blockdata.lisp +++ b/blockhash/lookups/blockhash_into_blockdata.lisp @@ -1,4 +1,4 @@ -(deflookup +(deflookup blockhash-into-blockdata ; target columns ( diff --git a/blockhash/lookups/blockhash_into_wcp_lex.lisp b/blockhash/lookups/blockhash_into_wcp_lex.lisp index 1a2fad97..13d6de3b 100644 --- a/blockhash/lookups/blockhash_into_wcp_lex.lisp +++ b/blockhash/lookups/blockhash_into_wcp_lex.lisp @@ -1,4 +1,4 @@ -(deflookup +(deflookup blockhash-into-wcp-lex ; target columns ( diff --git a/blockhash/lookups/blockhash_into_wcp_lower_bound.lisp b/blockhash/lookups/blockhash_into_wcp_lower_bound.lisp index 2dd58e9e..781c566f 100644 --- a/blockhash/lookups/blockhash_into_wcp_lower_bound.lisp +++ b/blockhash/lookups/blockhash_into_wcp_lower_bound.lisp @@ -1,4 +1,4 @@ -(deflookup +(deflookup blockhash-into-wcp-lower-bound ; target columns ( diff --git a/blockhash/lookups/blockhash_into_wcp_upper_bound.lisp b/blockhash/lookups/blockhash_into_wcp_upper_bound.lisp index 21944313..a35122ba 100644 --- a/blockhash/lookups/blockhash_into_wcp_upper_bound.lisp +++ b/blockhash/lookups/blockhash_into_wcp_upper_bound.lisp @@ -1,4 +1,4 @@ -(deflookup +(deflookup blockhash-into-wcp-upper-bound ; target columns ( diff --git a/constants/constants.lisp b/constants/constants.lisp index 5c2d5bb0..f4a09769 100644 --- a/constants/constants.lisp +++ b/constants/constants.lisp @@ -1,4 +1,4 @@ -(defconst +(defconst ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; EVM INSTRUCTIONS ;; @@ -419,7 +419,7 @@ RLP_RCPT_SUBPHASE_ID_DATA_SIZE 83 RLP_RCPT_SUBPHASE_ID_TOPIC_DELTA 96 ;; - ;; RLP_ADDR + ;; RLP_ADDR ;; RLP_ADDR_RECIPE_1 1 ;; for RlpAddr, used to discriminate between recipe for create RLP_ADDR_RECIPE_2 2 ;; for RlpAddr, used to discriminate between recipe for create diff --git a/ecdata/columns.lisp b/ecdata/columns.lisp index 3c6a53c7..672d8745 100644 --- a/ecdata/columns.lisp +++ b/ecdata/columns.lisp @@ -1,6 +1,6 @@ (module ecdata) -(defcolumns +(defcolumns (STAMP :i32) (ID :i32) (INDEX :i16) @@ -62,7 +62,7 @@ (EXT_INST :byte :display :opcode)) ;; aliases -(defalias +(defalias ICP INTERNAL_CHECKS_PASSED TRIVIAL_PAIRING OVERALL_TRIVIAL_PAIRING G2MTR G2_MEMBERSHIP_TEST_REQUIRED diff --git a/ecdata/constants.lisp b/ecdata/constants.lisp index 6c8324ae..0a7ef9cd 100644 --- a/ecdata/constants.lisp +++ b/ecdata/constants.lisp @@ -1,6 +1,6 @@ (module ecdata) -(defconst +(defconst P_BN_HI 0x30644e72e131a029b85045b68181585d P_BN_LO 0x97816a916871ca8d3c208c16d87cfd47 SECP256K1N_HI 0xffffffffffffffffffffffffffffffff diff --git a/ecdata/constraints.lisp b/ecdata/constraints.lisp index 105d7518..f79baef4 100644 --- a/ecdata/constraints.lisp +++ b/ecdata/constraints.lisp @@ -286,7 +286,7 @@ (vanishes! ID)))) (defconstraint stamp-increment-sanity-check () - (begin + (begin (debug (any! (will-remain-constant! STAMP) (will-inc! STAMP 1))))) ;; implied by the constraint below (defconstraint stamp-increment () diff --git a/ecdata/lookups/ecdata_into_ext.lisp b/ecdata/lookups/ecdata_into_ext.lisp index f497eb5d..1216145e 100644 --- a/ecdata/lookups/ecdata_into_ext.lisp +++ b/ecdata/lookups/ecdata_into_ext.lisp @@ -1,7 +1,7 @@ (defun (ec_data-into-ext-activation-flag) ecdata.EXT_FLAG) -(deflookup +(deflookup ecdata-into-ext ; target columns ( diff --git a/ecdata/lookups/ecdata_into_wcp.lisp b/ecdata/lookups/ecdata_into_wcp.lisp index 15c2d255..478a96c2 100644 --- a/ecdata/lookups/ecdata_into_wcp.lisp +++ b/ecdata/lookups/ecdata_into_wcp.lisp @@ -1,7 +1,7 @@ (defun (ec_data-into-wcp-activation-flag) ecdata.WCP_FLAG) -(deflookup +(deflookup ecdata-into-wcp ; target columns ( diff --git a/euc/columns.lisp b/euc/columns.lisp index cc36cbdb..9a7924b7 100644 --- a/euc/columns.lisp +++ b/euc/columns.lisp @@ -1,6 +1,6 @@ (module euc) -(defcolumns +(defcolumns (IOMF :binary@prove) (CT :i8) (CT_MAX :i8) diff --git a/euc/constraints.lisp b/euc/constraints.lisp index 376afca8..1d1b9fda 100644 --- a/euc/constraints.lisp +++ b/euc/constraints.lisp @@ -1,6 +1,6 @@ (module euc) -(defconst +(defconst MAX_INPUT_LENGTH MMEDIUM) (defconstraint first-row (:domain {0}) diff --git a/euc/lookups/euc_into_wcp.lisp b/euc/lookups/euc_into_wcp.lisp index ca0573b3..362b98da 100644 --- a/euc/lookups/euc_into_wcp.lisp +++ b/euc/lookups/euc_into_wcp.lisp @@ -1,4 +1,4 @@ -(deflookup +(deflookup euc-into-wcp ;reference columns ( diff --git a/exp/columns.lisp b/exp/columns.lisp index 6c259133..f3412cf9 100644 --- a/exp/columns.lisp +++ b/exp/columns.lisp @@ -1,6 +1,6 @@ (module exp) -(defcolumns +(defcolumns (CMPTN :binary@prove) (MACRO :binary@prove) (PRPRC :binary@prove) diff --git a/exp/constants.lisp b/exp/constants.lisp index 76725265..1c25bad9 100644 --- a/exp/constants.lisp +++ b/exp/constants.lisp @@ -1,6 +1,6 @@ (module exp) -(defconst +(defconst CT_MAX_CMPTN_EXP_LOG 15 CT_MAX_MACRO_EXP_LOG 0 CT_MAX_PRPRC_EXP_LOG 0 diff --git a/exp/constraints.lisp b/exp/constraints.lisp index 01af31d4..14090e4b 100644 --- a/exp/constraints.lisp +++ b/exp/constraints.lisp @@ -156,13 +156,13 @@ ;; constraints ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; non zero bit constraint +;; non zero bit constraint (defpurefun (non-zero-bit x nzb) (if-zero x (vanishes! nzb) (eq! nzb 1))) -;; counting nonzeroness constraint +;; counting nonzeroness constraint (defpurefun (counting-nonzeroness ct nzb_acc nzb) (if-zero ct (eq! nzb_acc nzb) @@ -305,7 +305,7 @@ ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;; -;; 1 +;; 1 (defconstraint modexp-log---preprocessing---cds-cutoff-less-than-ebs-cutoff (:perspective macro :guard IS_MODEXP_LOG) (callToLT 1 0 (cds_cutoff) 0 (ebs_cutoff))) diff --git a/exp/lookups/exp-into-wcp.lisp b/exp/lookups/exp-into-wcp.lisp index d15faa35..f15beeed 100644 --- a/exp/lookups/exp-into-wcp.lisp +++ b/exp/lookups/exp-into-wcp.lisp @@ -1,6 +1,6 @@ (defun (exp-into-wcp-activation-flag) (* exp.PRPRC exp.preprocessing/WCP_FLAG)) -(deflookup +(deflookup exp-into-wcp ;; target columns ( diff --git a/gas/columns.lisp b/gas/columns.lisp index 84e7ab3f..27df9115 100644 --- a/gas/columns.lisp +++ b/gas/columns.lisp @@ -1,6 +1,6 @@ (module gas) -(defcolumns +(defcolumns (INPUTS_AND_OUTPUTS_ARE_MEANINGFUL :binary@prove) (FIRST :binary@prove) (CT :i3) @@ -14,7 +14,7 @@ (WCP_INST :byte@prove :display :opcode) (WCP_RES :binary@prove)) -(defalias +(defalias IOMF INPUTS_AND_OUTPUTS_ARE_MEANINGFUL XAHOY EXCEPTIONS_AHOY OOGX OUT_OF_GAS_EXCEPTION) diff --git a/gas/lookups/gas-into-wcp.lisp b/gas/lookups/gas-into-wcp.lisp index 7ed9cb29..50512d0e 100644 --- a/gas/lookups/gas-into-wcp.lisp +++ b/gas/lookups/gas-into-wcp.lisp @@ -1,7 +1,7 @@ (defun (gas-into-wcp-activation-flag) gas.IOMF) -(deflookup +(deflookup gas-into-wcp ( wcp.ARG_1_HI diff --git a/hub/columns/miscellaneous.lisp b/hub/columns/miscellaneous.lisp index 1877a4da..a1913cd7 100644 --- a/hub/columns/miscellaneous.lisp +++ b/hub/columns/miscellaneous.lisp @@ -32,7 +32,7 @@ ( MMU_LIMB_2 :i128 ) ( MMU_PHASE :i32 ) ( MMU_EXO_SUM :i32 ) - + ;; MXP colummns (DONE ) ( MXP_INST :i32 ) ( MXP_MXPX :binary@prove ) ;; ;; TODO: demote to debug constraint, though truly useless @@ -71,5 +71,5 @@ ;; ``truly'' miscellaneous columns ( CCSR_FLAG :binary@prove) ;; Child Context Self Reverts Flag; ;; TODO: demote to debug constraint - ( CCRS_STAMP :i32 ) ;; Child Context Revert Stamp + ( CCRS_STAMP :i32 ) ;; Child Context Revert Stamp )) diff --git a/hub/columns/shared.lisp b/hub/columns/shared.lisp index 54a2ec94..1243ecfa 100644 --- a/hub/columns/shared.lisp +++ b/hub/columns/shared.lisp @@ -70,8 +70,8 @@ ;; ABS_TX_NUM ABSOLUTE_TRANSACTION_NUMBER REL_BLK_NUM RELATIVE_BLOCK_NUMBER - CMC CONTEXT_MAY_CHANGE - XAHOY EXCEPTION_AHOY + CMC CONTEXT_MAY_CHANGE + XAHOY EXCEPTION_AHOY TX_END_STAMP HUB_STAMP_TRANSACTION_END GAS_XPCT GAS_EXPECTED GAS_ACTL GAS_ACTUAL diff --git a/hub/columns/storage.lisp b/hub/columns/storage.lisp index f6ed29d8..35faa86b 100644 --- a/hub/columns/storage.lisp +++ b/hub/columns/storage.lisp @@ -1,10 +1,10 @@ (module hub) (defperspective storage - + ;; selector PEEK_AT_STORAGE - + ;; storage-row columns ( ( ADDRESS_HI :i32 ) diff --git a/hub/columns/transaction.lisp b/hub/columns/transaction.lisp index 7f2ee0c1..55bda053 100644 --- a/hub/columns/transaction.lisp +++ b/hub/columns/transaction.lisp @@ -38,7 +38,7 @@ ( GAS_LEFTOVER :i64 ) ( REFUND_COUNTER_INFINITY :i64 ) ( REFUND_EFFECTIVE :i64 ) - + ;; coinbase related ( COINBASE_ADDRESS_HI :i32 ) ( COINBASE_ADDRESS_LO :i128 ) diff --git a/hub/constraints/account.lisp b/hub/constraints/account.lisp index b1e26692..917ddd54 100644 --- a/hub/constraints/account.lisp +++ b/hub/constraints/account.lisp @@ -2,7 +2,7 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; -;; 6.1 Specialized-rows ;; +;; 6.1 Specialized-rows ;; ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -35,7 +35,7 @@ (begin (eq! BALANCE (prev BALANCE_NEW)) (eq! BALANCE_NEW (prev BALANCE)))) - + (defun (undo_previous_account_balance_update_v) (begin (eq! BALANCE (shift BALANCE_NEW -2)) @@ -188,7 +188,7 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; -;; 6.2 Code ownership ;; +;; 6.2 Code ownership ;; ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -198,18 +198,18 @@ (vanishes! HAS_CODE) (eq! HAS_CODE 1)) (eq! HAS_CODE 1))) - + (defconstraint hascode_new_emptyness (:perspective account) (if-eq-else CODE_HASH_HI_NEW EMPTY_KECCAK_HI (if-eq-else CODE_HASH_LO_NEW EMPTY_KECCAK_LO (eq! HAS_CODE_NEW 0) (eq! HAS_CODE_NEW 1)) (eq! HAS_CODE_NEW 1))) - + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; -;; 6.3 Account existence ;; +;; 6.3 Account existence ;; ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/hub/constraints/consistencies.lisp b/hub/constraints/consistencies.lisp index 5c52a273..6dca711b 100644 --- a/hub/constraints/consistencies.lisp +++ b/hub/constraints/consistencies.lisp @@ -7,7 +7,7 @@ ;; Stamp Constancies ;; is-stamp-constant should only be applied to stamp columns that grow by 0 or 1 each row. -(defun (is-stamp-constant stamp col) +(defun (is-stamp-constant stamp col) (if-not-zero (did-inc! stamp 1) (remained-constant! col))) diff --git a/hub/constraints/consistency/context/columns.lisp b/hub/constraints/consistency/context/columns.lisp index 63658c63..f2d396b1 100644 --- a/hub/constraints/consistency/context/columns.lisp +++ b/hub/constraints/consistency/context/columns.lisp @@ -1,7 +1,7 @@ (module hub) (defcolumns - ;; context consistency permutation related + ;; context consistency permutation related ( con_FIRST :binary@prove ) ( con_AGAIN :binary@prove ) ) diff --git a/hub/constraints/consistency/context/constraints.lisp b/hub/constraints/consistency/context/constraints.lisp index b0ea86e9..ec4c6d9f 100644 --- a/hub/constraints/consistency/context/constraints.lisp +++ b/hub/constraints/consistency/context/constraints.lisp @@ -9,7 +9,7 @@ (defconstraint context-consistency---perm-cn-first-and-cn-again-constraints () (begin - (eq! (+ con_AGAIN con_FIRST) + (eq! (+ con_AGAIN con_FIRST) ccp_PEEK_AT_CONTEXT) (if-zero (force-bool ccp_PEEK_AT_CONTEXT) (eq! (next con_FIRST) (next ccp_PEEK_AT_CONTEXT))) diff --git a/hub/constraints/consistency/execution_environment/constraints.lisp b/hub/constraints/consistency/execution_environment/constraints.lisp index 507fa2ea..472d2884 100644 --- a/hub/constraints/consistency/execution_environment/constraints.lisp +++ b/hub/constraints/consistency/execution_environment/constraints.lisp @@ -26,7 +26,7 @@ (eq! (next envcp_PC) envcp_PC_NEW) (eq! (next envcp_HEIGHT) envcp_HEIGHT_NEW) (eq! (next envcp_GAS_EXPECTED) envcp_GAS_NEXT)))))) - + (defconstraint execution-environment-consistency---initialization () (if-not-zero (will-remain-constant! envcp_CN) (begin diff --git a/hub/constraints/consistency/storage/columns.lisp b/hub/constraints/consistency/storage/columns.lisp index 75eee3ce..1006128b 100644 --- a/hub/constraints/consistency/storage/columns.lisp +++ b/hub/constraints/consistency/storage/columns.lisp @@ -1,7 +1,7 @@ (module hub) ;; scp_ ⇔ storage consistency permutation -(defpermutation +(defpermutation ;; permuted columns ;; replace scp with storage_consistency_permutation ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/hub/constraints/context-rows/specialized.lisp b/hub/constraints/context-rows/specialized.lisp index 1ecf7070..2fbc4736 100644 --- a/hub/constraints/context-rows/specialized.lisp +++ b/hub/constraints/context-rows/specialized.lisp @@ -10,7 +10,7 @@ (eq! CONTEXT_NUMBER_NEW (+ 1 HUB_STAMP))) -(defun (next-context-is-current) +(defun (next-context-is-current) (eq! CONTEXT_NUMBER_NEW CONTEXT_NUMBER)) @@ -94,7 +94,7 @@ return_data_provider_context ;; provider context return_data_offset ;; rdo return_data_size ;; rds - ) + ) (begin (eq! (shift context/UPDATE relative_row_offset) 1 ) (eq! (shift context/CONTEXT_NUMBER relative_row_offset) return_data_receiver_context ) diff --git a/hub/constraints/heartbeat/constancy_conditions.lisp b/hub/constraints/heartbeat/constancy_conditions.lisp index 119f3e46..46e5e958 100644 --- a/hub/constraints/heartbeat/constancy_conditions.lisp +++ b/hub/constraints/heartbeat/constancy_conditions.lisp @@ -25,7 +25,7 @@ -(defconstraint hub-stamp-constancy-of-TLI-and-NSR () +(defconstraint hub-stamp-constancy-of-TLI-and-NSR () (begin (hub-stamp-constancy TLI) (hub-stamp-constancy NSR))) diff --git a/hub/constraints/instruction-handling/add_bin_ext_mod_mul_shf_wcp.lisp b/hub/constraints/instruction-handling/add_bin_ext_mod_mul_shf_wcp.lisp index 0a64e633..8c6afbd4 100644 --- a/hub/constraints/instruction-handling/add_bin_ext_mod_mul_shf_wcp.lisp +++ b/hub/constraints/instruction-handling/add_bin_ext_mod_mul_shf_wcp.lisp @@ -44,7 +44,7 @@ (* stack/MUL_FLAG [ stack/DEC_FLAG 1 ]))) (defun (stateless-instruction---1-argument-instruction) (* (+ stack/BIN_FLAG stack/WCP_FLAG) [ stack/DEC_FLAG 1 ])) -(defun (stateless-instruction---2-argument-instruction) (+ stack/ADD_FLAG +(defun (stateless-instruction---2-argument-instruction) (+ stack/ADD_FLAG (* stack/BIN_FLAG (- 1 [ stack/DEC_FLAG 1 ])) stack/MOD_FLAG stack/MUL_FLAG @@ -76,8 +76,8 @@ (if-not-zero (stateless-instruction---3-argument-instruction) (stack-pattern-3-1)))) (defconstraint wcp-result-is-binary (:guard (stateless-instruction---precondition)) - (if-not-zero stack/WCP_FLAG - (begin + (if-not-zero stack/WCP_FLAG + (begin (vanishes! [ stack/STACK_ITEM_VALUE_HI 4 ]) (debug (is-binary [ stack/STACK_ITEM_VALUE_LO 4 ]))))) diff --git a/hub/constraints/instruction-handling/btc.lisp b/hub/constraints/instruction-handling/btc.lisp index c1d0728a..a1ef7502 100644 --- a/hub/constraints/instruction-handling/btc.lisp +++ b/hub/constraints/instruction-handling/btc.lisp @@ -42,7 +42,7 @@ ;; ;; should be redundant ;; (defconstraint block-data-instruction-setting-the-peeking-flags (:guard (block-data-standard-hypothesis)) ;; (if-not-zero CMC -;; (eq! (next PEEK_AT_CONTEXT) +;; (eq! (next PEEK_AT_CONTEXT) ;; 1))) (defconstraint block-data-instruction-setting-the-gas-cost (:guard (block-data-standard-hypothesis)) diff --git a/hub/constraints/instruction-handling/call/generalities/1st_set_of_account_rows.lisp b/hub/constraints/instruction-handling/call/generalities/1st_set_of_account_rows.lisp index 6e330ba2..ccdb9a92 100644 --- a/hub/constraints/instruction-handling/call/generalities/1st_set_of_account_rows.lisp +++ b/hub/constraints/instruction-handling/call/generalities/1st_set_of_account_rows.lisp @@ -45,7 +45,7 @@ (account-decrement-balance-by CALL_1st_caller_account_row___row_offset (* (call-instruction---is-CALL) (call-instruction---STACK-value-lo)))))) - + ;; CALLEE account (defconstraint call-instruction---1st-callee-account-operation (:guard (call-instruction---summon-both-account-rows-once-or-more)) (begin diff --git a/hub/constraints/instruction-handling/call/generalities/universal.lisp b/hub/constraints/instruction-handling/call/generalities/universal.lisp index e0d6767b..28cf4a5a 100644 --- a/hub/constraints/instruction-handling/call/generalities/universal.lisp +++ b/hub/constraints/instruction-handling/call/generalities/universal.lisp @@ -137,10 +137,10 @@ (- 1 (call-instruction---callee-has-code)))) (eq! (scenario-shorthand---CALL---smart-contract) (call-instruction---callee-has-code)))) (if-not-zero (+ scenario/CALL_PRC_SUCCESS_CALLER_WILL_REVERT scenario/CALL_PRC_SUCCESS_CALLER_WONT_REVERT) - (begin + (begin (eq! scenario/CALL_PRC_SUCCESS_CALLER_WILL_REVERT (call-instruction---caller-will-revert)) (debug (eq! scenario/CALL_PRC_SUCCESS_CALLER_WONT_REVERT (- 1 (call-instruction---caller-will-revert)))))) - (if-not-zero (scenario-shorthand---CALL---externally-owned-account) + (if-not-zero (scenario-shorthand---CALL---externally-owned-account) (begin (eq! scenario/CALL_EOA_SUCCESS_CALLER_WILL_REVERT (call-instruction---caller-will-revert)) (debug (eq! scenario/CALL_EOA_SUCCESS_CALLER_WONT_REVERT (- 1 (call-instruction---caller-will-revert)))))) diff --git a/hub/constraints/instruction-handling/call/precompiles/blake/success.lisp b/hub/constraints/instruction-handling/call/precompiles/blake/success.lisp index 33ce3261..421663ac 100644 --- a/hub/constraints/instruction-handling/call/precompiles/blake/success.lisp +++ b/hub/constraints/instruction-handling/call/precompiles/blake/success.lisp @@ -49,7 +49,7 @@ EXO_SUM_WEIGHT_BLAKEMODEXP ;; weighted exogenous module flag sum PHASE_BLAKE_RESULT ;; phase )) - + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Miscellaneous-row i + 4 ;; diff --git a/hub/constraints/instruction-handling/call/precompiles/common/constants.lisp b/hub/constraints/instruction-handling/call/precompiles/common/constants.lisp index b835599d..7ae6683a 100644 --- a/hub/constraints/instruction-handling/call/precompiles/common/constants.lisp +++ b/hub/constraints/instruction-handling/call/precompiles/common/constants.lisp @@ -9,7 +9,7 @@ precompile-processing---common---context-row-FKTH---row-offset 2 precompile-processing---common---context-row-success---row-offset 4 - + ;; IDENTITY specific constants precompile-processing---IDENTITY---2nd-misc-row---row-offset 2 diff --git a/hub/constraints/instruction-handling/call/precompiles/flag_sums_and_NSRs.lisp b/hub/constraints/instruction-handling/call/precompiles/flag_sums_and_NSRs.lisp index ca719248..f0654ffd 100644 --- a/hub/constraints/instruction-handling/call/precompiles/flag_sums_and_NSRs.lisp +++ b/hub/constraints/instruction-handling/call/precompiles/flag_sums_and_NSRs.lisp @@ -163,8 +163,8 @@ (defconst precompile-processing---nsr-IDENTITY-FKTH precompile-processing---nsr-standard-failure) (defconst precompile-processing---nsr-IDENTITY-success 4) ;; flag sum shorthands -(defun (precompile-processing---flag-sum-IDENTITY-FKTH) (precompile-processing---flag-sum-standard-failure)) -(defun (precompile-processing---flag-sum-IDENTITY-success) +(defun (precompile-processing---flag-sum-IDENTITY-FKTH) (precompile-processing---flag-sum-standard-failure)) +(defun (precompile-processing---flag-sum-IDENTITY-success) (+ (shift PEEK_AT_SCENARIO 0) (shift PEEK_AT_MISCELLANEOUS 1) (shift PEEK_AT_MISCELLANEOUS 2) @@ -191,7 +191,7 @@ (precompile-processing---nsr-MODEXP-success) (scenario-shorthand---PRC---success) )) ;; MODEXP non stack rows shorthands -(defun (precompile-processing---nsr-MODEXP-FKTR) (+ +(defun (precompile-processing---nsr-MODEXP-FKTR) (+ (shift PEEK_AT_SCENARIO 0 ) (shift PEEK_AT_MISCELLANEOUS precompile-processing---MODEXP-misc-row---cds---row-offset ) (shift PEEK_AT_MISCELLANEOUS precompile-processing---MODEXP-misc-row---extract-bbs---offset ) @@ -202,7 +202,7 @@ (shift PEEK_AT_CONTEXT precompile-processing---MODEXP-context-row---FKTR---row-offset ) ) ) -(defun (precompile-processing---nsr-MODEXP-success) (+ +(defun (precompile-processing---nsr-MODEXP-success) (+ (shift PEEK_AT_SCENARIO 0 ) (shift PEEK_AT_MISCELLANEOUS precompile-processing---MODEXP-misc-row---cds---row-offset ) (shift PEEK_AT_MISCELLANEOUS precompile-processing---MODEXP-misc-row---extract-bbs---offset ) @@ -221,7 +221,7 @@ (defun (precompile-processing---flag-sum-MODEXP-FKTR) (precompile-processing---flag-sum-standard-failure)) (defun (precompile-processing---flag-sum-MODEXP-success) (precompile-processing---flag-sum-standard-success)) ;; NB: the failure scenario FAILURE_KNOWN_TO_HUB is impossible -(defconst +(defconst precompile-processing---MODEXP-misc-row---cds---row-offset 1 precompile-processing---MODEXP-misc-row---extract-bbs---offset 2 precompile-processing---MODEXP-misc-row---extract-ebs---row-offset 3 @@ -236,7 +236,7 @@ precompile-processing---MODEXP-context-row---FKTR---row-offset 7 precompile-processing---MODEXP-context-row---success---row-offset 12 - + precompile-processing---nsr-FKTR 8 precompile-processing---nsr-success 13 ) diff --git a/hub/constraints/instruction-handling/call/precompiles/modexp/common.lisp b/hub/constraints/instruction-handling/call/precompiles/modexp/common.lisp index b8793513..2066b18c 100644 --- a/hub/constraints/instruction-handling/call/precompiles/modexp/common.lisp +++ b/hub/constraints/instruction-handling/call/precompiles/modexp/common.lisp @@ -211,8 +211,8 @@ ;; tgt_id ;; target ID ;; aux_id ;; auxiliary ID ;; src_offset_hi ;; source offset high - (+ (precompile-processing---dup-cdo) - 96 + (+ (precompile-processing---dup-cdo) + 96 (precompile-processing---MODEXP---bbs-lo)) ;; source offset low ;; tgt_offset_lo ;; target offset low ;; size ;; size diff --git a/hub/constraints/instruction-handling/halting/return.lisp b/hub/constraints/instruction-handling/halting/return.lisp index 230e3125..2547a964 100644 --- a/hub/constraints/instruction-handling/halting/return.lisp +++ b/hub/constraints/instruction-handling/halting/return.lisp @@ -240,7 +240,7 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (eq! (shift stack/HASH_INFO_FLAG ROFF_RETURN___STACK_ROW) (return-instruction---trigger_HASHINFO))) - + (defconstraint return-instruction---setting-MXP-data (:guard (return-instruction---standard-scenario-row)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (if-not-zero (shift misc/MXP_FLAG ROFF_RETURN___1ST_MISC_ROW) diff --git a/hub/constraints/instruction-handling/halting/selfdestruct.lisp b/hub/constraints/instruction-handling/halting/selfdestruct.lisp index 0acf07c9..d58ddb49 100644 --- a/hub/constraints/instruction-handling/halting/selfdestruct.lisp +++ b/hub/constraints/instruction-handling/halting/selfdestruct.lisp @@ -198,7 +198,7 @@ (defconstraint selfdestruct-instruction---setting-code-and-deployment-for-the-first-account-row (:guard (selfdestruct-instruction---scenario-precondition)) (if-zero (selfdestruct-instruction---STATICX) - (begin + (begin (if-not-zero XAHOY ;; XAHOY = 1 (begin (account-same-code ROFF_SELFDESTRUCT___ACCOUNT___1ST_DOING_ROW) diff --git a/hub/constraints/instruction-handling/log.lisp b/hub/constraints/instruction-handling/log.lisp index 27886a7e..3a907cae 100644 --- a/hub/constraints/instruction-handling/log.lisp +++ b/hub/constraints/instruction-handling/log.lisp @@ -31,7 +31,7 @@ (- 1 stack/SUX stack/SOX) (- 1 COUNTER_TLI))) -(defconst +(defconst ROFF_LOG___CURRENT_CONTEXT_ROW 2 ROFF_LOG___MISCELLANEOUS_ROW 3 ROFF_LOG___STATICX_XCONTEXT_ROW 3 diff --git a/hub/constraints/instruction-handling/sto.lisp b/hub/constraints/instruction-handling/sto.lisp index 6cb0277a..3918e8a1 100644 --- a/hub/constraints/instruction-handling/sto.lisp +++ b/hub/constraints/instruction-handling/sto.lisp @@ -173,7 +173,7 @@ (eq! GAS_COST (+ GAS_CONST_G_WARM_ACCESS (* (cold-slot) GAS_CONST_G_COLD_SLOAD)))) (if-not-zero (next-not-curr) (if-not-zero (curr-is-orig) - (if-not-zero (orig-is-zero) + (if-not-zero (orig-is-zero) (eq! GAS_COST (+ GAS_CONST_G_SSET (* (cold-slot) GAS_CONST_G_COLD_SLOAD))) (eq! GAS_COST (+ GAS_CONST_G_SRESET (* (cold-slot) GAS_CONST_G_COLD_SLOAD)))))))))) diff --git a/hub/constraints/scenario-rows/shorthands/call.lisp b/hub/constraints/scenario-rows/shorthands/call.lisp index 38241c77..d061edd2 100644 --- a/hub/constraints/scenario-rows/shorthands/call.lisp +++ b/hub/constraints/scenario-rows/shorthands/call.lisp @@ -9,7 +9,7 @@ ;;  CALL/externally_owned_account (defun (scenario-shorthand---CALL---externally-owned-account) - (+ + (+ ;; scenario/CALL_EXCEPTION ;; scenario/CALL_ABORT_WILL_REVERT ;; scenario/CALL_ABORT_WONT_REVERT @@ -26,7 +26,7 @@ ;;  CALL/smart_contract (defun (scenario-shorthand---CALL---smart-contract) - (+ + (+ ;; scenario/CALL_EXCEPTION ;; scenario/CALL_ABORT_WILL_REVERT ;; scenario/CALL_ABORT_WONT_REVERT @@ -43,7 +43,7 @@ ;;  CALL/precompile (defun (scenario-shorthand---CALL---precompile) - (+ + (+ ;; scenario/CALL_EXCEPTION ;; scenario/CALL_ABORT_WILL_REVERT ;; scenario/CALL_ABORT_WONT_REVERT @@ -60,14 +60,14 @@ ;;  CALL/abort (defun (scenario-shorthand---CALL---abort) - (+ + (+ scenario/CALL_ABORT_WILL_REVERT scenario/CALL_ABORT_WONT_REVERT )) ;;  CALL/entry (defun (scenario-shorthand---CALL---entry) - (+ + (+ (scenario-shorthand---CALL---externally-owned-account) (scenario-shorthand---CALL---smart-contract) (scenario-shorthand---CALL---precompile) @@ -75,21 +75,21 @@ ;;  CALL/unexceptional (defun (scenario-shorthand---CALL---unexceptional) - (+ + (+ (scenario-shorthand---CALL---abort) (scenario-shorthand---CALL---entry) )) ;;  CALL/sum (defun (scenario-shorthand---CALL---sum) - (+ + (+ scenario/CALL_EXCEPTION (scenario-shorthand---CALL---unexceptional) )) ;;  CALL/no_precompile (defun (scenario-shorthand---CALL---no-precompile) - (+ + (+ scenario/CALL_EXCEPTION (scenario-shorthand---CALL---abort) (scenario-shorthand---CALL---externally-owned-account) @@ -98,7 +98,7 @@ ;;  CALL/precompile_success (defun (scenario-shorthand---CALL---precompile-success) - (+ + (+ ;; scenario/CALL_EXCEPTION ;; scenario/CALL_ABORT_WILL_REVERT ;; scenario/CALL_ABORT_WONT_REVERT @@ -115,7 +115,7 @@ ;;  CALL/execution_known_to_revert (defun (scenario-shorthand---CALL---execution-known-to-revert) - (+ + (+ ;; scenario/CALL_EXCEPTION ;; scenario/CALL_ABORT_WILL_REVERT ;; scenario/CALL_ABORT_WONT_REVERT @@ -132,7 +132,7 @@ ;;  CALL/execution_known_to_not_revert (defun (scenario-shorthand---CALL---execution-known-to-not-revert) - (+ + (+ ;; scenario/CALL_EXCEPTION ;; scenario/CALL_ABORT_WILL_REVERT ;; scenario/CALL_ABORT_WONT_REVERT @@ -149,7 +149,7 @@ ;;  CALL/success (defun (scenario-shorthand---CALL---success) - (+ + (+ ;; scenario/CALL_EXCEPTION ;; scenario/CALL_ABORT_WILL_REVERT ;; scenario/CALL_ABORT_WONT_REVERT @@ -166,7 +166,7 @@ ;;  CALL/smc_success (defun (scenario-shorthand---CALL---smc-success) - (+ + (+ ;; scenario/CALL_EXCEPTION ;; scenario/CALL_ABORT_WILL_REVERT ;; scenario/CALL_ABORT_WONT_REVERT @@ -183,7 +183,7 @@ ;;  CALL/smc_failure (defun (scenario-shorthand---CALL---smc-failure) - (+ + (+ ;; scenario/CALL_EXCEPTION ;; scenario/CALL_ABORT_WILL_REVERT ;; scenario/CALL_ABORT_WONT_REVERT @@ -200,7 +200,7 @@ ;;  CALL/failure (defun (scenario-shorthand---CALL---failure) - (+ + (+ (scenario-shorthand---CALL---smc-failure) ;; scenario/CALL_EXCEPTION ;; scenario/CALL_ABORT_WILL_REVERT @@ -218,7 +218,7 @@ ;;  CALL/no_context_change (defun (scenario-shorthand---CALL---no-context-change) - (+ + (+ ;; scenario/CALL_EXCEPTION (scenario-shorthand---CALL---abort) ;; scenario/CALL_EOA_SUCCESS_CALLER_WILL_REVERT @@ -245,7 +245,7 @@ ;;  CALL/balance_update_not_required (defun (scenario-shorthand---CALL---balance-update-not-required) - (+ + (+ scenario/CALL_EXCEPTION (scenario-shorthand---CALL---abort) ;; scenario/CALL_EOA_SUCCESS_CALLER_WILL_REVERT @@ -262,7 +262,7 @@ ;;  CALL/balance_update_required (defun (scenario-shorthand---CALL---balance-update-required) - (+ + (+ (scenario-shorthand---CALL---externally-owned-account) (scenario-shorthand---CALL---smart-contract) (scenario-shorthand---CALL---precompile-success) @@ -282,7 +282,7 @@ ;;  CALL/requires_both_accounts_twice (defun (scenario-shorthand---CALL---requires-both-accounts-twice) - (+ + (+ ;; scenario/CALL_EXCEPTION ;; scenario/CALL_ABORT_WILL_REVERT ;; scenario/CALL_ABORT_WONT_REVERT @@ -299,7 +299,7 @@ ;;  CALL/undoes_balance_update_with_failure (defun (scenario-shorthand---CALL---balance-update-undone-with-callee-failure) - (+ + (+ ;; scenario/CALL_EXCEPTION ;; scenario/CALL_ABORT_WILL_REVERT ;; scenario/CALL_ABORT_WONT_REVERT @@ -316,7 +316,7 @@ ;;  CALL/undoes_balance_update_with_revert (defun (scenario-shorthand---CALL---balance-update-undone-with-caller-revert) - (+ + (+ ;; scenario/CALL_EXCEPTION ;; scenario/CALL_ABORT_WILL_REVERT ;; scenario/CALL_ABORT_WONT_REVERT @@ -333,7 +333,7 @@ ;; ;;  CALL/ ;; (defun (scenario-shorthand---CALL---) -;; (+ +;; (+ ;; scenario/CALL_EXCEPTION ;; scenario/CALL_ABORT_WILL_REVERT ;; scenario/CALL_ABORT_WONT_REVERT diff --git a/hub/constraints/scenario-rows/shorthands/precompile.lisp b/hub/constraints/scenario-rows/shorthands/precompile.lisp index e8826279..b7b12fa1 100644 --- a/hub/constraints/scenario-rows/shorthands/precompile.lisp +++ b/hub/constraints/scenario-rows/shorthands/precompile.lisp @@ -8,7 +8,7 @@ ;;  PRC/sum (defun (scenario-shorthand---PRC---common-except-identity-address-bit-sum) - (+ + (+ scenario/PRC_ECRECOVER scenario/PRC_SHA2-256 scenario/PRC_RIPEMD-160 @@ -38,7 +38,7 @@ ;;  PRC/may_only_fail_in_HUB (defun (scenario-shorthand---PRC---may-only-fail-in-the-HUB) - (+ + (+ scenario/PRC_ECRECOVER scenario/PRC_SHA2-256 scenario/PRC_RIPEMD-160 @@ -56,7 +56,7 @@ ;;  PRC/may_only_fail_in_RAM (defun (scenario-shorthand---PRC---may-only-fail-in-the-RAM) - (+ + (+ ;; scenario/PRC_ECRECOVER ;; scenario/PRC_SHA2-256 ;; scenario/PRC_RIPEMD-160 @@ -74,7 +74,7 @@ ;;  PRC/weighted_sum (defun (scenario-shorthand---PRC---weighted-address-bit-sum) - (+ + (+ (* 1 scenario/PRC_ECRECOVER ) (* 2 scenario/PRC_SHA2-256 ) (* 3 scenario/PRC_RIPEMD-160 ) @@ -92,7 +92,7 @@ ;;  PRC/failure (defun (scenario-shorthand---PRC---failure) - (+ + (+ ;; scenario/PRC_ECRECOVER ;; scenario/PRC_SHA2-256 ;; scenario/PRC_RIPEMD-160 @@ -110,7 +110,7 @@ ;;  PRC/success (defun (scenario-shorthand---PRC---success) - (+ + (+ ;; scenario/PRC_ECRECOVER ;; scenario/PRC_SHA2-256 ;; scenario/PRC_RIPEMD-160 @@ -128,14 +128,14 @@ ;;  PRC/scenario_sum (defun (scenario-shorthand---PRC---sum) - (+ + (+ (scenario-shorthand---PRC---failure) (scenario-shorthand---PRC---success) )) ;; ;;  PRC/ ;; (defun (scenario-shorthand---PRC---) -;; (+ +;; (+ ;; scenario/PRC_ECRECOVER ;; scenario/PRC_SHA2-256 ;; scenario/PRC_RIPEMD-160 diff --git a/hub/constraints/scenario-rows/shorthands/return.lisp b/hub/constraints/scenario-rows/shorthands/return.lisp index 85de0cf8..4b5236c9 100644 --- a/hub/constraints/scenario-rows/shorthands/return.lisp +++ b/hub/constraints/scenario-rows/shorthands/return.lisp @@ -57,7 +57,7 @@ )) ;; ;; NOT A CONSTRAINT -;; (defconstraint BULLSHIT-making-sure-everything-compiles-scenario-shorthand-RETURNs () +;; (defconstraint BULLSHIT-making-sure-everything-compiles-scenario-shorthand-RETURNs () ;; (begin (vanishes! (scenario-shorthand---RETURN---message-call) ) ;; (vanishes! (scenario-shorthand---RETURN---empty-deployment) ) ;; (vanishes! (scenario-shorthand---RETURN---nonempty-deployment) ) diff --git a/hub/constraints/storage-rows/specialized.lisp b/hub/constraints/storage-rows/specialized.lisp index 7eae7549..5b600ee8 100644 --- a/hub/constraints/storage-rows/specialized.lisp +++ b/hub/constraints/storage-rows/specialized.lisp @@ -14,7 +14,7 @@ ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defun (storage-reading kappa) +(defun (storage-reading kappa) (begin (eq! (shift storage/VALUE_CURR_HI kappa) (shift storage/VALUE_NEXT_HI kappa)) (eq! (shift storage/VALUE_CURR_LO kappa) (shift storage/VALUE_NEXT_LO kappa)))) diff --git a/hub/constraints/tx_finl/constraints.lisp b/hub/constraints/tx_finl/constraints.lisp index 71e0b141..d78ed25a 100644 --- a/hub/constraints/tx_finl/constraints.lisp +++ b/hub/constraints/tx_finl/constraints.lisp @@ -110,7 +110,7 @@ (defconstraint tx-finalization---success---justifying-txn-data-prediction---leftover-gas (:guard (tx-finalization---success---precondition)) (eq! (shift transaction/GAS_LEFTOVER row-offset---tx-finl---success---transaction-row) (shift GAS_NEXT -1))) - + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; ;; X.3 Transaction FAILURE ;; diff --git a/hub/constraints/tx_skip/constraints.lisp b/hub/constraints/tx_skip/constraints.lisp index 54bafcd7..a66874ae 100644 --- a/hub/constraints/tx_skip/constraints.lisp +++ b/hub/constraints/tx_skip/constraints.lisp @@ -10,7 +10,7 @@ (* TX_SKIP (- HUB_STAMP (prev HUB_STAMP)))) -(defconst +(defconst tx-skip---row-offset---sender-account 0 tx-skip---row-offset---recipient-account 1 tx-skip---row-offset---coinbase-account 2 @@ -126,7 +126,7 @@ tx-skip---row-offset---transaction-row)) (defconstraint tx-skip---setting-coinbase-account-row (:guard (tx-skip---precondition)) - (begin + (begin (eq! (shift account/ADDRESS_HI tx-skip---row-offset---coinbase-account) (shift transaction/COINBASE_ADDRESS_HI tx-skip---row-offset---transaction-row)) (eq! (shift account/ADDRESS_LO tx-skip---row-offset---coinbase-account) diff --git a/hub/lookups/hub_into_add.lisp b/hub/lookups/hub_into_add.lisp index 7b3c0176..2b5c4957 100644 --- a/hub/lookups/hub_into_add.lisp +++ b/hub/lookups/hub_into_add.lisp @@ -1,7 +1,7 @@ (defun (hub-into-add-activation-flag) (and (unexceptional-stack-row) hub.stack/ADD_FLAG)) -(deflookup +(deflookup hub-into-add ;; target columns ( diff --git a/hub/lookups/hub_into_block_hash.lisp b/hub/lookups/hub_into_block_hash.lisp index 3c2a2713..32790f76 100644 --- a/hub/lookups/hub_into_block_hash.lisp +++ b/hub/lookups/hub_into_block_hash.lisp @@ -1,7 +1,7 @@ (defun (hub-into-block-hash-trigger) (* hub.PEEK_AT_STACK (- 1 hub.XAHOY) hub.stack/BTC_FLAG [hub.stack/DEC_FLAG 1])) -(deflookup +(deflookup hub-into-blockhash ;; target columns ( diff --git a/hub/lookups/hub_into_exp.lisp b/hub/lookups/hub_into_exp.lisp index e2e851bc..3e624e33 100644 --- a/hub/lookups/hub_into_exp.lisp +++ b/hub/lookups/hub_into_exp.lisp @@ -1,10 +1,10 @@ -(defun (hub-into-exp-trigger) +(defun (hub-into-exp-trigger) (and hub.PEEK_AT_MISCELLANEOUS hub.misc/EXP_FLAG)) (deflookup hub-into-exp ;; target columns - ( + ( exp.MACRO exp.macro/EXP_INST [exp.macro/DATA 1] diff --git a/hub/lookups/hub_into_instruction_decoder.lisp b/hub/lookups/hub_into_instruction_decoder.lisp index 87eb77e3..b05e6e0c 100644 --- a/hub/lookups/hub_into_instruction_decoder.lisp +++ b/hub/lookups/hub_into_instruction_decoder.lisp @@ -2,7 +2,7 @@ (deflookup hub-into-instdecoder ;; target columns - ( + ( instdecoder.OPCODE instdecoder.STATIC_GAS instdecoder.TWO_LINE_INSTRUCTION diff --git a/hub/lookups/hub_into_log_info.lisp b/hub/lookups/hub_into_log_info.lisp index 0cbdb2da..25fd7e59 100644 --- a/hub/lookups/hub_into_log_info.lisp +++ b/hub/lookups/hub_into_log_info.lisp @@ -1,7 +1,7 @@ (defun (hub-into-log-info-trigger) (* hub.PEEK_AT_STACK hub.stack/LOG_INFO_FLAG (- 1 hub.CT_TLI))) -(deflookup +(deflookup hub-into-loginfo ;; target columns ( diff --git a/hub/lookups/hub_into_mxp.lisp b/hub/lookups/hub_into_mxp.lisp index 0eb77f34..80bd6266 100644 --- a/hub/lookups/hub_into_mxp.lisp +++ b/hub/lookups/hub_into_mxp.lisp @@ -1,7 +1,7 @@ (defun (hub-into-mxp-trigger) (and hub.PEEK_AT_MISCELLANEOUS hub.misc/MXP_FLAG)) -(deflookup +(deflookup hub-into-mxp ;; target columns ( diff --git a/hub/lookups/hub_into_oob.lisp b/hub/lookups/hub_into_oob.lisp index b83e306d..a2e95bce 100644 --- a/hub/lookups/hub_into_oob.lisp +++ b/hub/lookups/hub_into_oob.lisp @@ -4,7 +4,7 @@ (deflookup hub-into-oob ;; target columns - ( + ( oob.OOB_INST [oob.DATA 1] [oob.DATA 2] diff --git a/hub/lookups/hub_into_rlp_addr.lisp b/hub/lookups/hub_into_rlp_addr.lisp index 432e97ef..9e7dc2a1 100644 --- a/hub/lookups/hub_into_rlp_addr.lisp +++ b/hub/lookups/hub_into_rlp_addr.lisp @@ -1,11 +1,11 @@ -(defun (hub-into-rlp-addr-trigger) +(defun (hub-into-rlp-addr-trigger) (and hub.PEEK_AT_ACCOUNT hub.account/RLPADDR_FLAG)) ;; (deflookup hub-into-rlpaddr ;; target columns - ( + ( rlpaddr.RECIPE rlpaddr.ADDR_HI rlpaddr.ADDR_LO diff --git a/hub/lookups/hub_into_rlp_txn.lisp b/hub/lookups/hub_into_rlp_txn.lisp index df92c4a6..d81f4e21 100644 --- a/hub/lookups/hub_into_rlp_txn.lisp +++ b/hub/lookups/hub_into_rlp_txn.lisp @@ -14,7 +14,7 @@ rlptxn.IS_PHASE_ACCESS_LIST (- 1 rlptxn.IS_PREFIX))) -(deflookup +(deflookup hub-into-rlptxn ;; target columns ;; TODO: multiplication by selector likely unnecessary but as we multiply by the same column for the lookup tlptxn into hub ... diff --git a/hub/lookups/hub_into_rom_instruction_fetching.lisp b/hub/lookups/hub_into_rom_instruction_fetching.lisp index 575e7e16..6d0c8d15 100644 --- a/hub/lookups/hub_into_rom_instruction_fetching.lisp +++ b/hub/lookups/hub_into_rom_instruction_fetching.lisp @@ -2,7 +2,7 @@ (deflookup hub-into-rom-instruction-fetching ;; target columns - ( + ( rom.CFI rom.PC rom.OPCODE diff --git a/hub/lookups/hub_into_rom_jump_destination_vetting.lisp b/hub/lookups/hub_into_rom_jump_destination_vetting.lisp index 5f3c9ada..ffed3979 100644 --- a/hub/lookups/hub_into_rom_jump_destination_vetting.lisp +++ b/hub/lookups/hub_into_rom_jump_destination_vetting.lisp @@ -4,7 +4,7 @@ (deflookup hub-into-rom-jump-destination-vetting ;; target columns - ( + ( rom.CFI rom.PC rom.IS_JUMPDEST diff --git a/hub/lookups/hub_into_rom_lex.lisp b/hub/lookups/hub_into_rom_lex.lisp index 7e718f78..4fa79ae7 100644 --- a/hub/lookups/hub_into_rom_lex.lisp +++ b/hub/lookups/hub_into_rom_lex.lisp @@ -5,11 +5,11 @@ (deflookup hub-into-romlex ;; target columns - ( + ( romlex.CODE_FRAGMENT_INDEX romlex.CODE_SIZE romlex.ADDRESS_HI - romlex.ADDRESS_LO + romlex.ADDRESS_LO romlex.DEPLOYMENT_NUMBER romlex.DEPLOYMENT_STATUS romlex.CODE_HASH_HI diff --git a/hub/lookups/hub_into_stp.lisp b/hub/lookups/hub_into_stp.lisp index faf67a0f..36e16fd2 100644 --- a/hub/lookups/hub_into_stp.lisp +++ b/hub/lookups/hub_into_stp.lisp @@ -1,7 +1,7 @@ (defun (hub-into-stp-trigger) (* hub.PEEK_AT_MISCELLANEOUS hub.misc/STP_FLAG)) -(deflookup +(deflookup hub-into-stp ;; target columns ( diff --git a/hub/lookups/hub_into_trm.lisp b/hub/lookups/hub_into_trm.lisp index 5b4057ee..7bad8b86 100644 --- a/hub/lookups/hub_into_trm.lisp +++ b/hub/lookups/hub_into_trm.lisp @@ -4,7 +4,7 @@ (deflookup hub-into-trm ;; target columns - ( + ( trm.TRM_ADDRESS_HI trm.RAW_ADDRESS_HI trm.RAW_ADDRESS_LO diff --git a/hub/lookups/hub_into_wcp.lisp b/hub/lookups/hub_into_wcp.lisp index 46509d1b..9346e96d 100644 --- a/hub/lookups/hub_into_wcp.lisp +++ b/hub/lookups/hub_into_wcp.lisp @@ -1,4 +1,4 @@ -(defun (hub-into-wcp-activation-flag) +(defun (hub-into-wcp-activation-flag) (and (unexceptional-stack-row) hub.stack/WCP_FLAG)) diff --git a/hub/lookups/hub_into_wcp_for_stack_overflow.lisp b/hub/lookups/hub_into_wcp_for_stack_overflow.lisp index e78266f5..1a4b71b4 100644 --- a/hub/lookups/hub_into_wcp_for_stack_overflow.lisp +++ b/hub/lookups/hub_into_wcp_for_stack_overflow.lisp @@ -4,7 +4,7 @@ (defun (projected-height) (- (+ hub.HEIGHT hub.stack/ALPHA) hub.stack/DELTA)) -(deflookup +(deflookup hub-into-wcp-for-sox ;; target columns ( diff --git a/logdata/columns.lisp b/logdata/columns.lisp index 778ad44e..d34da930 100644 --- a/logdata/columns.lisp +++ b/logdata/columns.lisp @@ -1,6 +1,6 @@ (module logdata) -(defcolumns +(defcolumns (ABS_LOG_NUM_MAX :i24) (ABS_LOG_NUM :i24) (LOGS_DATA :binary) diff --git a/logdata/lookups/logdata-to-rlprcpt.lisp b/logdata/lookups/logdata-to-rlprcpt.lisp index 28120bb4..557eaf11 100644 --- a/logdata/lookups/logdata-to-rlprcpt.lisp +++ b/logdata/lookups/logdata-to-rlprcpt.lisp @@ -1,7 +1,7 @@ (defpurefun (sel-logdata-to-rlptxnrcpt) logdata.LOGS_DATA) -(deflookup +(deflookup logdata-into-rlptxnrcpt ;reference columns ( diff --git a/loginfo/columns.lisp b/loginfo/columns.lisp index f2083845..8bb2e09a 100644 --- a/loginfo/columns.lisp +++ b/loginfo/columns.lisp @@ -1,6 +1,6 @@ (module loginfo) -(defcolumns +(defcolumns (ABS_TXN_NUM_MAX :i24) (ABS_TXN_NUM :i24) (TXN_EMITS_LOGS :binary@prove) diff --git a/loginfo/lookups/loginfo-into-logdata.lisp b/loginfo/lookups/loginfo-into-logdata.lisp index 79565fa5..d4fa5654 100644 --- a/loginfo/lookups/loginfo-into-logdata.lisp +++ b/loginfo/lookups/loginfo-into-logdata.lisp @@ -1,7 +1,7 @@ (defpurefun (sel-loginfo-to-logdata) loginfo.TXN_EMITS_LOGS) -(deflookup +(deflookup loginfo-into-logdata ;; target columns ( diff --git a/loginfo/lookups/loginfo-into-rlprcpt.lisp b/loginfo/lookups/loginfo-into-rlprcpt.lisp index 3110e2ab..c9ee8691 100644 --- a/loginfo/lookups/loginfo-into-rlprcpt.lisp +++ b/loginfo/lookups/loginfo-into-rlprcpt.lisp @@ -1,4 +1,4 @@ -(deflookup +(deflookup loginfo-into-rlptxrcpt ;; target columns ( diff --git a/mmio/columns.lisp b/mmio/columns.lisp index 61d21246..98c54ba2 100644 --- a/mmio/columns.lisp +++ b/mmio/columns.lisp @@ -1,6 +1,6 @@ (module mmio) -(defcolumns +(defcolumns (CN_A :i64 :display :dec) (CN_B :i64 :display :dec) (CN_C :i64 :display :dec) @@ -29,7 +29,7 @@ (TARGET_BYTE_OFFSET :i8 :display :dec) (SIZE :i64 :display :dec) (LIMB :i128) - (TOTAL_SIZE :i64 :display :dec) + (TOTAL_SIZE :i64 :display :dec) (EXO_SUM :i32) (EXO_ID :i32) (KEC_ID :i32) @@ -65,7 +65,7 @@ (POW_256 :i128 :array [1:2]) (COUNTER :i8)) -(defalias +(defalias STAMP MMIO_STAMP CT COUNTER CNS CONTEXT_SOURCE diff --git a/mmio/consistency.lisp b/mmio/consistency.lisp index 8da1a52f..8c8b9197 100644 --- a/mmio/consistency.lisp +++ b/mmio/consistency.lisp @@ -1,26 +1,26 @@ (module mmio) -(definterleaved +(definterleaved CN_ABC (CN_A CN_B CN_C)) -(definterleaved +(definterleaved INDEX_ABC (INDEX_A INDEX_B INDEX_C)) -(definterleaved +(definterleaved MMIO_STAMP_3 (MMIO_STAMP MMIO_STAMP MMIO_STAMP)) -(definterleaved +(definterleaved VAL_ABC (VAL_A VAL_B VAL_C)) -(definterleaved +(definterleaved VAL_ABC_NEW (VAL_A_NEW VAL_B_NEW VAL_C_NEW)) -(defpermutation +(defpermutation (CN_ABC_SORTED INDEX_ABC_SORTED MMIO_STAMP_3_SORTED diff --git a/mmio/lookups/mmio_into_blakemodexp.lisp b/mmio/lookups/mmio_into_blakemodexp.lisp index faffd04d..d98d864d 100644 --- a/mmio/lookups/mmio_into_blakemodexp.lisp +++ b/mmio/lookups/mmio_into_blakemodexp.lisp @@ -1,4 +1,4 @@ -(deflookup +(deflookup mmio-into-blake2fmodexpdata ;reference columns ( diff --git a/mmio/lookups/mmio_into_ecdata.lisp b/mmio/lookups/mmio_into_ecdata.lisp index 5d12da8d..689256e0 100644 --- a/mmio/lookups/mmio_into_ecdata.lisp +++ b/mmio/lookups/mmio_into_ecdata.lisp @@ -1,4 +1,4 @@ -(deflookup +(deflookup mmio-into-ecdata ;reference columns ( diff --git a/mmio/lookups/mmio_into_kec.lisp b/mmio/lookups/mmio_into_kec.lisp index deed1f2a..4a27582f 100644 --- a/mmio/lookups/mmio_into_kec.lisp +++ b/mmio/lookups/mmio_into_kec.lisp @@ -1,4 +1,4 @@ -(deflookup +(deflookup mmio-into-kec ;reference columns ( diff --git a/mmio/lookups/mmio_into_logdata.lisp b/mmio/lookups/mmio_into_logdata.lisp index d6cb18cc..5abd4dfa 100644 --- a/mmio/lookups/mmio_into_logdata.lisp +++ b/mmio/lookups/mmio_into_logdata.lisp @@ -1,4 +1,4 @@ -(deflookup +(deflookup mmio-into-logdata ;reference columns ( diff --git a/mmio/lookups/mmio_into_mmu.lisp b/mmio/lookups/mmio_into_mmu.lisp index 6a076fca..19bf0ee1 100644 --- a/mmio/lookups/mmio_into_mmu.lisp +++ b/mmio/lookups/mmio_into_mmu.lisp @@ -13,7 +13,7 @@ mmio.IS_RAM_EXCISION mmio.IS_RAM_VANISHES)) -(deflookup +(deflookup mmio-into-mmu ;reference columns ( diff --git a/mmio/lookups/mmio_into_ripsha.lisp b/mmio/lookups/mmio_into_ripsha.lisp index 26c81b8a..8787a8cc 100644 --- a/mmio/lookups/mmio_into_ripsha.lisp +++ b/mmio/lookups/mmio_into_ripsha.lisp @@ -1,4 +1,4 @@ -(deflookup +(deflookup mmio-into-ripsha ;reference columns ( @@ -17,4 +17,4 @@ (* mmio.EXO_IS_RIPSHA mmio.LIMB) (* mmio.EXO_IS_RIPSHA mmio.SIZE) (* mmio.EXO_IS_RIPSHA mmio.TOTAL_SIZE) - )) \ No newline at end of file + )) diff --git a/mmio/lookups/mmio_into_rlptxn.lisp b/mmio/lookups/mmio_into_rlptxn.lisp index f5ddb8df..175688f0 100644 --- a/mmio/lookups/mmio_into_rlptxn.lisp +++ b/mmio/lookups/mmio_into_rlptxn.lisp @@ -1,4 +1,4 @@ -(deflookup +(deflookup mmio-into-rlptxn ;reference columns ( diff --git a/mmio/lookups/mmio_into_rom.lisp b/mmio/lookups/mmio_into_rom.lisp index 064a1386..864c1f13 100644 --- a/mmio/lookups/mmio_into_rom.lisp +++ b/mmio/lookups/mmio_into_rom.lisp @@ -1,4 +1,4 @@ -(deflookup +(deflookup mmio-into-rom ;reference columns ( diff --git a/mmu/columns.lisp b/mmu/columns.lisp index ff40271a..70c5efc0 100644 --- a/mmu/columns.lisp +++ b/mmu/columns.lisp @@ -1,6 +1,6 @@ (module mmu) -(defcolumns +(defcolumns ;; shared columns (STAMP :i32 :display :dec) (MMIO_STAMP :i32 :display :dec) @@ -29,7 +29,7 @@ (IS_MODEXP_ZERO :binary@prove) (IS_MODEXP_DATA :binary@prove) (IS_BLAKE :binary@prove) - ;; USED ONLY IN MICRO ROW BUT ARE SHARED + ;; USED ONLY IN MICRO ROW BUT ARE SHARED (LZRO :binary@prove) (NT_ONLY :binary@prove) (NT_FIRST :binary@prove) diff --git a/mmu/constants.lisp b/mmu/constants.lisp index 182a2d33..e4886e2e 100644 --- a/mmu/constants.lisp +++ b/mmu/constants.lisp @@ -1,6 +1,6 @@ (module mmu) -(defconst +(defconst ;; ;; MMU NB OF PP ROWS ;; diff --git a/mmu/instructions/any_to_ram_with_padding/common.lisp b/mmu/instructions/any_to_ram_with_padding/common.lisp index 219d5721..b1028144 100644 --- a/mmu/instructions/any_to_ram_with_padding/common.lisp +++ b/mmu/instructions/any_to_ram_with_padding/common.lisp @@ -30,7 +30,7 @@ (defun (any-to-ram-with-padding---trsf-size) (+ (* (any-to-ram-with-padding---mixed) (- macro/REF_SIZE macro/SRC_OFFSET_LO)) (* (any-to-ram-with-padding---pure-data) macro/SIZE))) (defun (any-to-ram-with-padding---padd-size) (+ (* (any-to-ram-with-padding---pure-padd) macro/SIZE) - (* (any-to-ram-with-padding---mixed) + (* (any-to-ram-with-padding---mixed) (- macro/SIZE (- macro/REF_SIZE macro/SRC_OFFSET_LO))))) ;; "" (defconstraint any-to-ram-with-padding---common---1st-preprocessing-row (:guard (* MACRO (is-any-to-ram-with-padding))) diff --git a/mmu/instructions/exo_to_ram_transplant.lisp b/mmu/instructions/exo_to_ram_transplant.lisp index cec6c228..c4c67076 100644 --- a/mmu/instructions/exo_to_ram_transplant.lisp +++ b/mmu/instructions/exo_to_ram_transplant.lisp @@ -20,14 +20,14 @@ LLARGE)) (defconstraint exo-to-ram-transplant---setting-the-TOTs (:guard (* IS_EXO_TO_RAM_TRANSPLANTS MACRO)) - (begin + (begin ;; setting nb of rows (vanishes! TOTLZ) (eq! TOTNT (next prprc/EUC_CEIL)) (vanishes! TOTRZ))) (defconstraint exo-to-ram-transplant---setting-micro-instruction-constant-values (:guard (* IS_EXO_TO_RAM_TRANSPLANTS MACRO)) - (begin + (begin ;; setting mmio constant values (eq! (shift micro/CN_T NB_PP_ROWS_EXO_TO_RAM_TRANSPLANTS_PO) macro/TGT_ID) (eq! (shift micro/EXO_SUM NB_PP_ROWS_EXO_TO_RAM_TRANSPLANTS_PO) macro/EXO_SUM) diff --git a/mmu/instructions/modexp_zero.lisp b/mmu/instructions/modexp_zero.lisp index 7241984d..dec3c0c9 100644 --- a/mmu/instructions/modexp_zero.lisp +++ b/mmu/instructions/modexp_zero.lisp @@ -14,13 +14,13 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (defconstraint modexp-zero---setting-the-TOTs (:guard (* MACRO IS_MODEXP_ZERO)) - (begin + (begin (vanishes! TOTLZ) (eq! TOTNT NB_MICRO_ROWS_TOT_MODEXP_ZERO) (vanishes! TOTRZ))) (defconstraint modexp-zero---setting-micro-instruction-constant-values (:guard (* MACRO IS_MODEXP_ZERO)) - (begin + (begin (eq! (shift micro/EXO_SUM NB_PP_ROWS_MODEXP_ZERO_PO) EXO_SUM_WEIGHT_BLAKEMODEXP) (eq! (shift micro/PHASE NB_PP_ROWS_MODEXP_ZERO_PO) macro/PHASE) (eq! (shift micro/EXO_ID NB_PP_ROWS_MODEXP_ZERO_PO) macro/TGT_ID))) diff --git a/mmu/lookups/mmu_into_euc.lisp b/mmu/lookups/mmu_into_euc.lisp index 0260df2b..564587a9 100644 --- a/mmu/lookups/mmu_into_euc.lisp +++ b/mmu/lookups/mmu_into_euc.lisp @@ -1,7 +1,7 @@ (defun (mmu-to-euc-selector) (* mmu.PRPRC mmu.prprc/EUC_FLAG)) -(deflookup +(deflookup mmu-into-euc ;reference columns ( diff --git a/mmu/lookups/mmu_into_mmio.lisp b/mmu/lookups/mmu_into_mmio.lisp index e8fb8ff0..d45ea794 100644 --- a/mmu/lookups/mmu_into_mmio.lisp +++ b/mmu/lookups/mmu_into_mmio.lisp @@ -1,4 +1,4 @@ -(deflookup +(deflookup mmu-into-mmio ;reference columns ( diff --git a/mmu/lookups/mmu_into_wcp.lisp b/mmu/lookups/mmu_into_wcp.lisp index 2d1c873e..60181462 100644 --- a/mmu/lookups/mmu_into_wcp.lisp +++ b/mmu/lookups/mmu_into_wcp.lisp @@ -1,7 +1,7 @@ (defun (mmu-to-wcp-selector) (* mmu.PRPRC mmu.prprc/WCP_FLAG)) -(deflookup +(deflookup mmu-into-wcp ;reference columns ( diff --git a/mxp/columns.lisp b/mxp/columns.lisp index b2d1d474..68307634 100644 --- a/mxp/columns.lisp +++ b/mxp/columns.lisp @@ -1,6 +1,6 @@ (module mxp) -(defcolumns +(defcolumns (STAMP :i32) (CN :i64) (CT :i5) @@ -46,7 +46,7 @@ (SIZE_1_NONZERO_NO_MXPX :binary) (SIZE_2_NONZERO_NO_MXPX :binary)) - (defalias + (defalias S1NZNOMXPX SIZE_1_NONZERO_NO_MXPX S2NZNOMXPX SIZE_2_NONZERO_NO_MXPX) diff --git a/mxp/constants.lisp b/mxp/constants.lisp index fa1e7cd5..c0fde302 100644 --- a/mxp/constants.lisp +++ b/mxp/constants.lisp @@ -1,6 +1,6 @@ (module mxp) -(defconst +(defconst CT_MAX_TRIVIAL 0 CT_MAX_NON_TRIVIAL 3 CT_MAX_NON_TRIVIAL_BUT_MXPX 16 diff --git a/mxp/constraints.lisp b/mxp/constraints.lisp index 3e15952f..e5a97f2e 100644 --- a/mxp/constraints.lisp +++ b/mxp/constraints.lisp @@ -108,7 +108,7 @@ ;;;;;;;;;;;;;;;;;;;; (defconstraint setting-mtntop () - (begin + (begin (debug (is-binary MTNTOP)) (debug (if-zero [MXP_TYPE 4] (vanishes! MTNTOP))) @@ -129,27 +129,27 @@ (defconstraint setting-s1nznomp-s2nznomp () (begin (debug (is-binary S1NZNOMXPX)) - (debug (is-binary S2NZNOMXPX)) + (debug (is-binary S2NZNOMXPX)) (debug (counter-constancy CT S1NZNOMXPX)) (debug (counter-constancy CT S2NZNOMXPX)) (if-not-zero MXPX (begin (vanishes! S1NZNOMXPX) (vanishes! S2NZNOMXPX)) - (begin (if-not-zero SIZE_1_LO + (begin (if-not-zero SIZE_1_LO (eq! S1NZNOMXPX 1)) - (if-not-zero SIZE_1_HI + (if-not-zero SIZE_1_HI (eq! S1NZNOMXPX 1)) - (if-zero SIZE_1_LO - (if-zero SIZE_1_HI + (if-zero SIZE_1_LO + (if-zero SIZE_1_HI (vanishes! S1NZNOMXPX))) - (if-not-zero SIZE_2_LO + (if-not-zero SIZE_2_LO (eq! S2NZNOMXPX 1)) - (if-not-zero SIZE_2_HI + (if-not-zero SIZE_2_HI (eq! S2NZNOMXPX 1)) - (if-zero SIZE_2_LO - (if-zero SIZE_2_HI + (if-zero SIZE_2_LO + (if-zero SIZE_2_HI (vanishes! S2NZNOMXPX))))))) - + ;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; ;; 2.7 heartbeat ;; @@ -371,7 +371,7 @@ ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defpermutation +(defpermutation (CN_perm STAMP_perm C_MEM_perm diff --git a/mxp/lookups/mxp_into_instdecoder.lisp b/mxp/lookups/mxp_into_instdecoder.lisp index 7999d3a9..03bba01c 100644 --- a/mxp/lookups/mxp_into_instdecoder.lisp +++ b/mxp/lookups/mxp_into_instdecoder.lisp @@ -1,7 +1,7 @@ (deflookup mxp-into-instdecoder ;; source columns ( - instdecoder.OPCODE ;; INST in the specs + instdecoder.OPCODE ;; INST in the specs instdecoder.BILLING_PER_WORD ;; ♢GWORD in the specs instdecoder.BILLING_PER_BYTE ;; ♢GBYTE in the specs instdecoder.MXP_TYPE_1 ;; ♢TYPE_1 in the specs @@ -11,14 +11,14 @@ instdecoder.MXP_TYPE_5 ;; ♢TYPE_5 in the specs ) ;target columns - ( - mxp.INST - mxp.GWORD - mxp.GBYTE + ( + mxp.INST + mxp.GWORD + mxp.GBYTE [mxp.MXP_TYPE 1] ;; TYPE_1 in the specs [mxp.MXP_TYPE 2] ;; TYPE_2 in the specs [mxp.MXP_TYPE 3] ;; TYPE_3 in the specs [mxp.MXP_TYPE 4] ;; TYPE_4 in the specs - [mxp.MXP_TYPE 5] ;; TYPE_5 in the specs + [mxp.MXP_TYPE 5] ;; TYPE_5 in the specs ) ) diff --git a/oob/columns.lisp b/oob/columns.lisp index 9a975135..497414dc 100644 --- a/oob/columns.lisp +++ b/oob/columns.lisp @@ -1,6 +1,6 @@ (module oob) -(defcolumns +(defcolumns (STAMP :i32) (CT :i3) (CT_MAX :i3) diff --git a/oob/constants.lisp b/oob/constants.lisp index 1e19e16c..06e82624 100644 --- a/oob/constants.lisp +++ b/oob/constants.lisp @@ -1,6 +1,6 @@ (module oob) -(defconst +(defconst CT_MAX_JUMP 0 CT_MAX_JUMPI 1 CT_MAX_RDC 2 diff --git a/oob/constraints.lisp b/oob/constraints.lisp index 8e55433c..284f1ace 100644 --- a/oob/constraints.lisp +++ b/oob/constraints.lisp @@ -521,7 +521,7 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; ;; 5.1 Common ;; -;; constraints for ;; +;; constraints for ;; ;; precompiles ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/oob/lookups/oob-into-add.lisp b/oob/lookups/oob-into-add.lisp index d3b4ae94..c92e100e 100644 --- a/oob/lookups/oob-into-add.lisp +++ b/oob/lookups/oob-into-add.lisp @@ -1,7 +1,7 @@ (defun (oob-into-add-activation-flag) oob.ADD_FLAG) -(deflookup +(deflookup oob-into-add ;source columns ( diff --git a/oob/lookups/oob-into-mod.lisp b/oob/lookups/oob-into-mod.lisp index 9a53e70c..647dafe5 100644 --- a/oob/lookups/oob-into-mod.lisp +++ b/oob/lookups/oob-into-mod.lisp @@ -1,7 +1,7 @@ (defun (oob-into-mod-activation-flag) oob.MOD_FLAG) -(deflookup +(deflookup oob-into-mod ;source columns ( diff --git a/oob/lookups/oob-into-wcp.lisp b/oob/lookups/oob-into-wcp.lisp index 2d931cd7..4c6be68e 100644 --- a/oob/lookups/oob-into-wcp.lisp +++ b/oob/lookups/oob-into-wcp.lisp @@ -1,7 +1,7 @@ (defun (oob-into-wcp-activation-flag) oob.WCP_FLAG) -(deflookup +(deflookup oob-into-wcp ( wcp.ARGUMENT_1_HI diff --git a/reftables/bin_reftable.lisp b/reftables/bin_reftable.lisp index 2da0f831..b573f92a 100644 --- a/reftables/bin_reftable.lisp +++ b/reftables/bin_reftable.lisp @@ -1,6 +1,6 @@ (module binreftable) -(defcolumns +(defcolumns (INST :byte :display :opcode) (RESULT_BYTE :byte) (INPUT_BYTE_1 :byte) diff --git a/reftables/shf_reftable.lisp b/reftables/shf_reftable.lisp index d5868b29..4109f5d1 100644 --- a/reftables/shf_reftable.lisp +++ b/reftables/shf_reftable.lisp @@ -1,6 +1,6 @@ (module shfreftable) -(defcolumns +(defcolumns (IOMF :binary) (BYTE1 :byte) (MSHP :byte) diff --git a/rlpaddr/columns.lisp b/rlpaddr/columns.lisp index e24079ef..4182548b 100644 --- a/rlpaddr/columns.lisp +++ b/rlpaddr/columns.lisp @@ -1,6 +1,6 @@ (module rlpaddr) -(defcolumns +(defcolumns ;; INPUTS (RECIPE :byte) (RECIPE_1 :binary@prove) @@ -33,7 +33,7 @@ (SELECTOR_KECCAK_RES :binary)) ;; aliases -(defalias +(defalias ct COUNTER) diff --git a/rlpaddr/constants.lisp b/rlpaddr/constants.lisp index 3cd2a95f..8746807a 100644 --- a/rlpaddr/constants.lisp +++ b/rlpaddr/constants.lisp @@ -1,6 +1,6 @@ (module rlpaddr) -(defconst +(defconst MAX_CT_CREATE 7 MAX_CT_CREATE2 5) diff --git a/rlpaddr/lookups/rlpaddr_into_trm.lisp b/rlpaddr/lookups/rlpaddr_into_trm.lisp index 2e41b123..a8ef71c5 100644 --- a/rlpaddr/lookups/rlpaddr_into_trm.lisp +++ b/rlpaddr/lookups/rlpaddr_into_trm.lisp @@ -1,4 +1,4 @@ -(deflookup +(deflookup rlpaddr-into-trm ;reference columns ( diff --git a/rlptxn/columns.lisp b/rlptxn/columns.lisp index e5e77381..8d6377d4 100644 --- a/rlptxn/columns.lisp +++ b/rlptxn/columns.lisp @@ -1,6 +1,6 @@ (module rlptxn) -(defcolumns +(defcolumns (ABS_TX_NUM :i16) (LIMB :i128) (nBYTES :i5) @@ -59,7 +59,7 @@ (PHASE :i5)) ;; aliases -(defalias +(defalias CT COUNTER LC LIMB_CONSTRUCTED P POWER diff --git a/rlptxn/constants.lisp b/rlptxn/constants.lisp index 5e39c1ec..7788e2dc 100644 --- a/rlptxn/constants.lisp +++ b/rlptxn/constants.lisp @@ -1,6 +1,6 @@ (module rlptxn) -(defconst +(defconst UNPROTECTED_V 27 UNPROTECTED_V_PO (+ UNPROTECTED_V 1) PROTECTED_BASE_V 35 diff --git a/rlptxn/lookups/rlptxn_into_rom.lisp b/rlptxn/lookups/rlptxn_into_rom.lisp index e961f516..bdd3d293 100644 --- a/rlptxn/lookups/rlptxn_into_rom.lisp +++ b/rlptxn/lookups/rlptxn_into_rom.lisp @@ -2,7 +2,7 @@ (defun (sel-rlptxn-to-rom) (* (~ rlptxn.CODE_FRAGMENT_INDEX) rlptxn.IS_PHASE_DATA (- 1 rlptxn.IS_PREFIX) rlptxn.LC)) -(deflookup +(deflookup rlptxn-into-rom ;; target columns ( diff --git a/rlptxrcpt/columns.lisp b/rlptxrcpt/columns.lisp index a5b2dd1d..a61887f4 100644 --- a/rlptxrcpt/columns.lisp +++ b/rlptxrcpt/columns.lisp @@ -1,6 +1,6 @@ (module rlptxrcpt) -(defcolumns +(defcolumns (ABS_TX_NUM :i32) (ABS_TX_NUM_MAX :i32) (ABS_LOG_NUM :i32) @@ -34,7 +34,7 @@ (PHASE_ID :i16)) ;; aliases -(defalias +(defalias CT COUNTER LC LIMB_CONSTRUCTED P POWER) diff --git a/rlptxrcpt/constants.lisp b/rlptxrcpt/constants.lisp index 6053b034..3ee05f44 100644 --- a/rlptxrcpt/constants.lisp +++ b/rlptxrcpt/constants.lisp @@ -1,6 +1,6 @@ (module rlptxrcpt) -(defconst +(defconst SUBPHASE_ID_WEIGHT_IS_PREFIX 6 SUBPHASE_ID_WEIGHT_IS_OT 12 SUBPHASE_ID_WEIGHT_IS_OD 24 diff --git a/rlptxrcpt/constraints.lisp b/rlptxrcpt/constraints.lisp index e413b33d..3308fe77 100644 --- a/rlptxrcpt/constraints.lisp +++ b/rlptxrcpt/constraints.lisp @@ -40,7 +40,7 @@ (if-eq (* PHASE (prev PHASE)) 1 (or! (remained-constant! C) (did-dec! C 1)))) -;; Constancies +;; Constancies (defconstraint block-constancies () (begin (block-constant ABS_TX_NUM_MAX) (block-constant ABS_LOG_NUM_MAX))) diff --git a/rom/columns.lisp b/rom/columns.lisp index 71034cee..c7e51876 100644 --- a/rom/columns.lisp +++ b/rom/columns.lisp @@ -1,6 +1,6 @@ (module rom) -(defcolumns +(defcolumns (CODE_FRAGMENT_INDEX :i32) (CODE_FRAGMENT_INDEX_INFTY :i32) (CODE_SIZE :i32 :display :dec) @@ -25,7 +25,7 @@ (OPCODE :byte :display :opcode) (IS_JUMPDEST :binary)) -(defalias +(defalias PC PROGRAM_COUNTER CFI CODE_FRAGMENT_INDEX CT COUNTER diff --git a/rom/lookups/rom_into_instdecoder.lisp b/rom/lookups/rom_into_instdecoder.lisp index 7d686795..556f812f 100644 --- a/rom/lookups/rom_into_instdecoder.lisp +++ b/rom/lookups/rom_into_instdecoder.lisp @@ -1,4 +1,4 @@ -(deflookup +(deflookup rom-into-instdecoder ;; target columns ( diff --git a/romlex/columns.lisp b/romlex/columns.lisp index 7926ffba..0a9d73ec 100644 --- a/romlex/columns.lisp +++ b/romlex/columns.lisp @@ -1,6 +1,6 @@ (module romlex) -(defcolumns +(defcolumns (CODE_FRAGMENT_INDEX :i32) (CODE_FRAGMENT_INDEX_INFTY :i32) (CODE_SIZE :i32) @@ -13,7 +13,7 @@ (COMMIT_TO_STATE :binary@prove) (READ_FROM_STATE :binary@prove)) -(defalias +(defalias CFI CODE_FRAGMENT_INDEX) diff --git a/romlex/lookups/romLex_into_rom.lisp b/romlex/lookups/romLex_into_rom.lisp index 84bcade4..74a3a13d 100644 --- a/romlex/lookups/romLex_into_rom.lisp +++ b/romlex/lookups/romLex_into_rom.lisp @@ -1,4 +1,4 @@ -(deflookup +(deflookup romlex-into-rom ;; target columns ( diff --git a/shakiradata/columns.lisp b/shakiradata/columns.lisp index 62f676e5..ab2df1f4 100644 --- a/shakiradata/columns.lisp +++ b/shakiradata/columns.lisp @@ -1,6 +1,6 @@ (module shakiradata) -(defcolumns +(defcolumns (SHAKIRA_STAMP :i32) (ID :i32) (PHASE :byte) diff --git a/shakiradata/constants.lisp b/shakiradata/constants.lisp index 66d5355b..21bdde7a 100644 --- a/shakiradata/constants.lisp +++ b/shakiradata/constants.lisp @@ -1,6 +1,6 @@ (module shakiradata) -(defconst +(defconst INDEX_MAX_RESULT 1) diff --git a/shakiradata/lookups/shakira_into_wcp_increasing_id.lisp b/shakiradata/lookups/shakira_into_wcp_increasing_id.lisp index fe3c72bb..f4ce56d0 100644 --- a/shakiradata/lookups/shakira_into_wcp_increasing_id.lisp +++ b/shakiradata/lookups/shakira_into_wcp_increasing_id.lisp @@ -1,17 +1,17 @@ (defun (is-data) (force-bool (+ shakiradata.IS_KECCAK_DATA - ;; IS_KECCAK_RESULT + ;; IS_KECCAK_RESULT shakiradata.IS_SHA2_DATA - ;; IS_SHA2_RESULT + ;; IS_SHA2_RESULT shakiradata.IS_RIPEMD_DATA - ;; IS_RIPEMD_RESULT + ;; IS_RIPEMD_RESULT ))) (defun (is-first-data-row) (force-bool (* (is-data) (- 1 (prev (is-data)))))) -(deflookup +(deflookup shakiradata-into-wcp-increasing-id ; target colums (in WCP) ( diff --git a/shakiradata/lookups/shakira_into_wcp_nonzero_last_nbytes.lisp b/shakiradata/lookups/shakira_into_wcp_nonzero_last_nbytes.lisp index f2f279d7..9525de9a 100644 --- a/shakiradata/lookups/shakira_into_wcp_nonzero_last_nbytes.lisp +++ b/shakiradata/lookups/shakira_into_wcp_nonzero_last_nbytes.lisp @@ -9,7 +9,7 @@ (defun (is-final-data-row) (force-bool (* (is-data) (next (is-result))))) -(deflookup +(deflookup shakiradata-into-wcp-nonzero-last-nbytes ; target colums (in WCP) ( diff --git a/shakiradata/lookups/shakira_into_wcp_small_last_nbytes.lisp b/shakiradata/lookups/shakira_into_wcp_small_last_nbytes.lisp index 00f3386d..5785c711 100644 --- a/shakiradata/lookups/shakira_into_wcp_small_last_nbytes.lisp +++ b/shakiradata/lookups/shakira_into_wcp_small_last_nbytes.lisp @@ -1,4 +1,4 @@ -(deflookup +(deflookup shakiradata-into-wcp-small-last-nbytes ; target colums (in WCP) ( diff --git a/shf/columns.lisp b/shf/columns.lisp index c0f61a3e..7c604413 100644 --- a/shf/columns.lisp +++ b/shf/columns.lisp @@ -1,6 +1,6 @@ (module shf) -(defcolumns +(defcolumns (SHIFT_STAMP :i32) (IOMF :binary) (COUNTER :i8) @@ -54,7 +54,7 @@ (SHB_7_LO :byte)) ;; aliases -(defalias +(defalias STAMP SHIFT_STAMP SHD SHIFT_DIRECTION OLI ONE_LINE_INSTRUCTION diff --git a/shf/lookups/shf_into_shfRT.lisp b/shf/lookups/shf_into_shfRT.lisp index b123c369..e9d3e014 100644 --- a/shf/lookups/shf_into_shfRT.lisp +++ b/shf/lookups/shf_into_shfRT.lisp @@ -1,4 +1,4 @@ -(deflookup +(deflookup shf-into-shfreftable-hi ;reference columns ( @@ -9,7 +9,7 @@ shfreftable.RAP shfreftable.ONES ) - ;source columns + ;source columns ( shf.IOMF shf.BYTE_2 @@ -19,7 +19,7 @@ shf.ONES )) -(deflookup +(deflookup shf-into-shfreftable-lo ;reference columns ( @@ -29,7 +29,7 @@ shfreftable.LAS shfreftable.RAP ) - ;source columns + ;source columns ( shf.IOMF shf.BYTE_3 diff --git a/stp/columns.lisp b/stp/columns.lisp index 6687d9a4..e2b07ac5 100644 --- a/stp/columns.lisp +++ b/stp/columns.lisp @@ -1,6 +1,6 @@ (module stp) -(defcolumns +(defcolumns (STAMP :i24) (CT :byte) (CT_MAX :byte) @@ -35,7 +35,7 @@ (ARG_2_LO :i128) (RES_LO :i128)) -(defalias +(defalias OOGX OUT_OF_GAS_EXCEPTION EXO_INST EXOGENOUS_MODULE_INSTRUCTION) diff --git a/stp/constraints.lisp b/stp/constraints.lisp index d64bf944..1297b083 100644 --- a/stp/constraints.lisp +++ b/stp/constraints.lisp @@ -1,6 +1,6 @@ (module stp) -(defconst +(defconst STP_CT_MAX_CALL 4 STP_CT_MAX_CALL_OOGX 2 STP_CT_MAX_CREATE 2 @@ -165,7 +165,7 @@ ;; rows of CREATE instructions that don't produce an OOGX (defconstraint CREATE-type---unexceptional---row-i-plus-2 (:guard (first-row-of-unexceptional-CREATE)) - (begin + (begin ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; -------------> row i + 2 ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/stp/lookups/stp_into_mod.lisp b/stp/lookups/stp_into_mod.lisp index bb905f79..89d15d7d 100644 --- a/stp/lookups/stp_into_mod.lisp +++ b/stp/lookups/stp_into_mod.lisp @@ -1,4 +1,4 @@ -(deflookup +(deflookup stp-into-mod ; target columns (in MOD) ( diff --git a/stp/lookups/stp_into_wcp.lisp b/stp/lookups/stp_into_wcp.lisp index 7d66e002..a8157185 100644 --- a/stp/lookups/stp_into_wcp.lisp +++ b/stp/lookups/stp_into_wcp.lisp @@ -1,4 +1,4 @@ -(deflookup +(deflookup stp-into-wcp ; target colums (in WCP) ( diff --git a/trm/columns.lisp b/trm/columns.lisp index 60d3ffa3..6e8f94d0 100644 --- a/trm/columns.lisp +++ b/trm/columns.lisp @@ -1,6 +1,6 @@ (module trm) -(defcolumns +(defcolumns (STAMP :i24) (RAW_ADDRESS_HI :i128) (RAW_ADDRESS_LO :i128) diff --git a/txndata/columns.lisp b/txndata/columns.lisp index fde99312..b56b204e 100644 --- a/txndata/columns.lisp +++ b/txndata/columns.lisp @@ -1,6 +1,6 @@ (module txndata) -(defcolumns +(defcolumns (ABS_TX_NUM_MAX :i16) (ABS_TX_NUM :i16) (REL_BLOCK :i16) @@ -49,7 +49,7 @@ (INST :byte :display :opcode) (IS_LAST_TX_OF_BLOCK :binary)) -(defalias +(defalias ABS_MAX ABS_TX_NUM_MAX ABS ABS_TX_NUM BLK REL_BLOCK diff --git a/txndata/constants.lisp b/txndata/constants.lisp index 351522e9..cd696f03 100644 --- a/txndata/constants.lisp +++ b/txndata/constants.lisp @@ -1,6 +1,6 @@ (module txndata) -(defconst +(defconst CT_MAX_TYPE_0 7 CT_MAX_TYPE_1 8 CT_MAX_TYPE_2 8 diff --git a/txndata/lookups/txndata_into_blockdata.lisp b/txndata/lookups/txndata_into_blockdata.lisp index 32d639dd..3a6cec0b 100644 --- a/txndata/lookups/txndata_into_blockdata.lisp +++ b/txndata/lookups/txndata_into_blockdata.lisp @@ -1,4 +1,4 @@ -(deflookup +(deflookup txndata-into-blockdata ; target columns ( diff --git a/txndata/lookups/txndata_into_euc.lisp b/txndata/lookups/txndata_into_euc.lisp index 92e40c09..1f81ed11 100644 --- a/txndata/lookups/txndata_into_euc.lisp +++ b/txndata/lookups/txndata_into_euc.lisp @@ -1,4 +1,4 @@ -(deflookup +(deflookup txndata-into-euc ; target columns ( diff --git a/txndata/lookups/txndata_into_rlpaddr.lisp b/txndata/lookups/txndata_into_rlpaddr.lisp index b2e12f27..556f50e4 100644 --- a/txndata/lookups/txndata_into_rlpaddr.lisp +++ b/txndata/lookups/txndata_into_rlpaddr.lisp @@ -1,7 +1,7 @@ (defun (sel-txndata-to-rlpaddr) txndata.IS_DEP) -(deflookup +(deflookup txndata-into-rlpaddr ;; target columns ( diff --git a/txndata/lookups/txndata_into_rlptxn.lisp b/txndata/lookups/txndata_into_rlptxn.lisp index 6fddba8e..f84678c7 100644 --- a/txndata/lookups/txndata_into_rlptxn.lisp +++ b/txndata/lookups/txndata_into_rlptxn.lisp @@ -1,4 +1,4 @@ -(deflookup +(deflookup txndata-into-rlptxn ;; target columns ( diff --git a/txndata/lookups/txndata_into_rlptxrcpt.lisp b/txndata/lookups/txndata_into_rlptxrcpt.lisp index a42605d9..7c478b5d 100644 --- a/txndata/lookups/txndata_into_rlptxrcpt.lisp +++ b/txndata/lookups/txndata_into_rlptxrcpt.lisp @@ -1,4 +1,4 @@ -(deflookup +(deflookup txndata-into-rlptxrcpt ;; target columns ( diff --git a/txndata/lookups/txndata_into_romlex.lisp b/txndata/lookups/txndata_into_romlex.lisp index 7cf23b04..fffa0cd5 100644 --- a/txndata/lookups/txndata_into_romlex.lisp +++ b/txndata/lookups/txndata_into_romlex.lisp @@ -1,7 +1,7 @@ (defun (sel-txn-data-to-rom-lex) (* txndata.IS_DEP (~ txndata.INIT_CODE_SIZE))) -(deflookup +(deflookup txndata-into-romlex ;; target columns ( diff --git a/txndata/lookups/txndata_into_wcp.lisp b/txndata/lookups/txndata_into_wcp.lisp index 015766cc..069cae30 100644 --- a/txndata/lookups/txndata_into_wcp.lisp +++ b/txndata/lookups/txndata_into_wcp.lisp @@ -1,4 +1,4 @@ -(deflookup +(deflookup txndata-into-wcp ; target columns ( diff --git a/wcp/columns.lisp b/wcp/columns.lisp index 9fdb9152..220723be 100644 --- a/wcp/columns.lisp +++ b/wcp/columns.lisp @@ -1,6 +1,6 @@ (module wcp) -(defcolumns +(defcolumns (WORD_COMPARISON_STAMP :i32) (COUNTER :byte) (CT_MAX :byte) @@ -41,7 +41,7 @@ (BIT_4 :binary@prove)) ;; aliases -(defalias +(defalias STAMP WORD_COMPARISON_STAMP OLI ONE_LINE_INSTRUCTION VLI VARIABLE_LENGTH_INSTRUCTION diff --git a/wcp/constraints.lisp b/wcp/constraints.lisp index e926d4fe..4ac6b273 100644 --- a/wcp/constraints.lisp +++ b/wcp/constraints.lisp @@ -4,7 +4,7 @@ (+ (one-line-inst) (variable-length-inst))) (defun (weight-sum) - (+ + (+ (* EVM_INST_LT IS_LT) (* EVM_INST_GT IS_GT) (* EVM_INST_SLT IS_SLT)