|
61 | 61 | ;; 2.2 Constancies ;; |
62 | 62 | ;; ;; |
63 | 63 | ;;;;;;;;;;;;;;;;;;;;;;;;;;; |
64 | | - |
65 | 64 | (defun (transaction-constant X) |
66 | 65 | (if-not-zero CT |
67 | 66 | (eq! X (prev X)))) |
|
155 | 154 | (defun (optional_to_addr_hi) (shift OUTGOING_HI 1)) |
156 | 155 | (defun (optional_to_addr_lo) (shift OUTGOING_LO 1)) |
157 | 156 | (defun (nonce) (shift OUTGOING_LO 2)) |
158 | | -(defun (is_dep) (force-bin (shift OUTGOING_HI 3))) |
| 157 | +(defun (is_dep) (shift OUTGOING_HI 3)) |
159 | 158 | (defun (value) (shift OUTGOING_LO 3)) |
160 | 159 | (defun (data_cost) (shift OUTGOING_HI 4)) |
161 | 160 | (defun (data_size) (shift OUTGOING_LO 4)) |
|
250 | 249 |
|
251 | 250 | (defun (result-must-be-false row-offset) (vanishes! (shift RES row-offset))) |
252 | 251 | (defun (result-must-be-true row-offset) (eq! (shift RES row-offset) 1)) |
253 | | - |
254 | | - |
255 | 252 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
256 | 253 | ;; ;; |
257 | 254 | ;; 2.9 Shared computations ;; |
258 | 255 | ;; ;; |
259 | 256 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
260 | 257 |
|
261 | | -(defconstraint comparison---nonce-must-not-exceed-EIP-2681-max-nonce |
262 | | - (:guard (first-row-of-new-transaction)) |
| 258 | +(defconstraint comparison---nonce-must-not-exceed-EIP-2681-max-nonce (:guard (first-row-of-new-transaction)) |
263 | 259 | (begin |
264 | 260 | (small-call-to-LT row-offset---nonce-comparison NONCE EIP2681_MAX_NONCE) |
265 | 261 | (result-must-be-true row-offset---nonce-comparison))) |
266 | 262 |
|
267 | | -(defconstraint comparison---initial-balance-must-cover-value-plus-maximal-gas-cost |
268 | | - (:guard (first-row-of-new-transaction)) |
| 263 | +(defconstraint comparison---initial-balance-must-cover-value-plus-maximal-gas-cost (:guard (first-row-of-new-transaction)) |
269 | 264 | (begin |
270 | 265 | (small-call-to-LEQ row-offset---initial-balance-comparison (+ (value) (* (max_fee) (gas_limit))) INITIAL_BALANCE) |
271 | 266 | (result-must-be-true row-offset---initial-balance-comparison))) |
272 | 267 |
|
273 | | -(defconstraint comparaison---code-size-limit-check |
274 | | - (:guard (first-row-of-new-transaction)) |
275 | | - (if-not-zero (is_dep) |
276 | | - (begin |
277 | | - (small-call-to-LEQ row-offset---init-code-size-limit |
278 | | - (data_size) |
279 | | - MAX_INIT_CODE_SIZE) |
280 | | - (result-must-be-true row-offset---init-code-size-limit)))) |
281 | | - |
282 | | -(defconstraint euc-call---computing-number-of-words-in-init-code |
283 | | - (:guard (first-row-of-new-transaction)) |
284 | | - (if-not-zero (is_dep) |
285 | | - (begin |
286 | | - (call-to-EUC row-offset---init-code-pricing |
287 | | - (+ (data_size) WORD_SIZE_MO) |
288 | | - WORD_SIZE)))) |
289 | | - |
290 | | -(defun (number_of_words_in_init_code) (shift RES row-offset---init-code-pricing)) |
291 | | - |
292 | | -(defun (init_code_cost) |
293 | | - (* GAS_CONST_INIT_CODE_WORD |
294 | | - (number_of_words_in_init_code) |
295 | | - )) |
296 | | - |
297 | | -(defun (upfront_gas_cost) |
298 | | - (+ (* TYPE0 (legacy_upfront_gas_cost)) |
299 | | - (* TYPE1 (access_upfront_gas_cost)) |
300 | | - (* TYPE2 (access_upfront_gas_cost)))) |
301 | | - |
302 | | -(defun (legacy_upfront_gas_cost) |
303 | | - (+ (data_cost) |
304 | | - (* (is_dep) GAS_CONST_G_TX_CREATE) |
305 | | - (* (is_dep) (init_code_cost)) |
306 | | - GAS_CONST_G_TRANSACTION |
307 | | - )) |
308 | | - |
309 | | -(defun (access_upfront_gas_cost) |
310 | | - (+ (data_cost) |
311 | | - (* (is_dep) GAS_CONST_G_TX_CREATE) |
312 | | - (* (is_dep) (init_code_cost)) |
313 | | - GAS_CONST_G_TRANSACTION |
314 | | - (* (num_addr) GAS_CONST_G_ACCESS_LIST_ADRESS) |
315 | | - (* (num_keys) GAS_CONST_G_ACCESS_LIST_STORAGE))) |
| 268 | +(defun (upfront_gas_cost) |
| 269 | + (+ (* TYPE0 (legacy_upfront_gas_cost)) |
| 270 | + (* TYPE1 (access_upfront_gas_cost)) |
| 271 | + (* TYPE2 (access_upfront_gas_cost)))) |
| 272 | +(defun (legacy_upfront_gas_cost) |
| 273 | + (+ (data_cost) |
| 274 | + GAS_CONST_G_TRANSACTION |
| 275 | + (* (is_dep) GAS_CONST_G_TX_CREATE))) |
| 276 | +(defun (access_upfront_gas_cost) |
| 277 | + (+ (data_cost) |
| 278 | + GAS_CONST_G_TRANSACTION |
| 279 | + (* (is_dep) GAS_CONST_G_TX_CREATE) |
| 280 | + (* (num_addr) GAS_CONST_G_ACCESS_LIST_ADRESS) |
| 281 | + (* (num_keys) GAS_CONST_G_ACCESS_LIST_STORAGE))) |
316 | 282 |
|
317 | 283 | (defconstraint comparison---gas-limit-must-cover-upfront-gas-cost (:guard (first-row-of-new-transaction)) |
318 | 284 | (begin |
|
0 commit comments