|
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