Skip to content

Commit d855c03

Browse files
letypequividelespoubellesletypequividelespoubelles
authored
Revert "feat: TRM reimplem" (#623)
1 parent ab7d065 commit d855c03

File tree

5 files changed

+72
-124
lines changed

5 files changed

+72
-124
lines changed

‎constants/constants.lisp

Lines changed: 0 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -252,23 +252,11 @@
252252
LLARGEPO (+ LLARGE 1)
253253
WORD_SIZE 32
254254
WORD_SIZE_MO (- WORD_SIZE 1)
255-
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
256-
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;
257-
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; SHIFT ;;
258-
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;
259-
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
260-
TWOFIFTYSIX_TO_THE_FOUR (^ 256 4)
261-
TWOFIFTYSIX_TO_THE_FOUR_MO (- TWOFIFTYSIX_TO_THE_FOUR 1)
262-
TWOFIFTYSIX_TO_THE_TWELVE (^ 256 12)
263-
TWOFIFTYSIX_TO_THE_TWELVE_MO (- TWOFIFTYSIX_TO_THE_TWELVE 1)
264-
TWOFIFTYSIX_TO_THE_TWENTY (^ 256 20)
265-
TWOFIFTYSIX_TO_THE_TWENTY_MO (- TWOFIFTYSIX_TO_THE_TWENTY 1)
266255
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
267256
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;
268257
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; PRECOMPILES ;;
269258
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;
270259
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
271-
NUMBER_OF_PRECOMPILES 9 ;;London value
272260
PRC_ECPAIRING_SIZE (* 6 WORD_SIZE)
273261
PRC_BLAKE2F_SIZE 213
274262
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

‎trm/columns.lisp

Lines changed: 12 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,17 +1,19 @@
11
(module trm)
22

33
(defcolumns
4-
(STAMP :i40)
5-
(FIRST :binary)
4+
(STAMP :i24)
65
(RAW_ADDRESS_HI :i128)
76
(RAW_ADDRESS_LO :i128)
87
(TRM_ADDRESS_HI :i32)
9-
(IS_PRECOMPILE :binary)
8+
(IS_PRECOMPILE :binary@prove)
109
(CT :i4)
11-
(ARG_1_HI :i128)
12-
(ARG_1_LO :i128)
13-
(ARG_2_HI :i128)
14-
(ARG_2_LO :i128)
15-
(RES :binary)
16-
(INST :byte :display :opcode)
17-
)
10+
(ACC_HI :i128)
11+
(ACC_LO :i128)
12+
(ACC_T :i32)
13+
(PLATEAU_BIT :binary@prove)
14+
(ONE :binary@prove)
15+
(BYTE_HI :byte@prove)
16+
(BYTE_LO :byte@prove))
17+
18+
(defalias
19+
PBIT PLATEAU_BIT)

‎trm/constants.lisp

Lines changed: 0 additions & 10 deletions
This file was deleted.

‎trm/constraints.lisp

Lines changed: 60 additions & 72 deletions
Original file line numberDiff line numberDiff line change
@@ -9,39 +9,31 @@
99
(defconstraint first-row (:domain {0})
1010
(vanishes! STAMP))
1111

12-
(defconstraint stamp-increment ()
13-
(or! (will-remain-constant! STAMP) (will-inc! STAMP 1)))
14-
1512
;; 3
1613
(defconstraint null-stamp-null-columns ()
1714
(if-zero STAMP
1815
(begin (vanishes! RAW_ADDRESS_HI)
1916
(vanishes! RAW_ADDRESS_LO)
2017
(vanishes! TRM_ADDRESS_HI)
2118
(vanishes! IS_PRECOMPILE)
22-
(vanishes! (next CT))
2319
(debug (vanishes! CT))
2420
(debug (vanishes! BYTE_HI))
2521
(debug (vanishes! BYTE_LO)))))
2622

27-
(defconstraint setting-first ()
28-
(eq! FIRST
29-
(- STAMP (prev STAMP))))
30-
31-
(defconstraint heartbeat (:guard STAMP)
32-
(begin
33-
(if-not-zero (- TRM_CT_MAX CT)
34-
(begin
35-
(will-remain-constant! STAMP)
36-
(will-inc! CT 1)))
37-
(if-zero (- TRM_CT_MAX CT)
38-
(begin
39-
(will-inc! STAMP 1)
40-
(vanishes! (next CT))))))
41-
23+
(defconstraint heartbeat ()
24+
(begin ;; 2
25+
(or! (will-remain-constant! STAMP) (will-inc! STAMP 1))
26+
;; 4
27+
(if-not-zero (- (next STAMP) STAMP)
28+
(vanishes! (next CT)))
29+
;; 5
30+
(if-not-zero STAMP
31+
(if-eq-else CT LLARGEMO (will-inc! STAMP 1) (will-inc! CT 1)))))
32+
33+
;; 6
4234
(defconstraint last-row (:domain {-1})
4335
(if-not-zero STAMP
44-
(eq! CT TRM_CT_MAX)))
36+
(eq! CT LLARGEMO)))
4537

4638
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
4739
;; ;;
@@ -54,62 +46,58 @@
5446
(stamp-constancy STAMP IS_PRECOMPILE)
5547
(stamp-constancy STAMP TRM_ADDRESS_HI)))
5648

49+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
50+
;; ;;
51+
;; 2.3 PBIT constraints ;;
52+
;; ;;
53+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
54+
(defconstraint pbit-constraint ()
55+
(begin (if-not-zero CT
56+
(or! (remained-constant! PBIT) (did-inc! PBIT 1)))
57+
(if-eq CT LLARGEMO
58+
(eq! 1
59+
(+ (shift PBIT (- 0 4))
60+
(shift PBIT (- 0 3)))))))
61+
62+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
63+
;; ;;
64+
;; 2.4 Byte Decomposition ;;
65+
;; ;;
66+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
67+
(defconstraint byte-decompositions ()
68+
(begin (byte-decomposition CT ACC_HI BYTE_HI)
69+
(byte-decomposition CT ACC_LO BYTE_LO)
70+
(byte-decomposition CT ACC_T (* BYTE_HI PBIT))))
5771

5872
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
5973
;; ;;
60-
;; 2.4 setting WCP calls ;;
61-
;; ;;
62-
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
63-
(defun (wcpcall-leq offset arg1hi arg1lo arg2hi arg2lo)
64-
(begin (eq! (shift INST offset) WCP_INST_LEQ)
65-
(eq! (shift ARG_1_HI offset) arg1hi)
66-
(eq! (shift ARG_1_LO offset) arg1lo)
67-
(eq! (shift ARG_2_HI offset) arg2hi)
68-
(eq! (shift ARG_2_LO offset) arg2lo)))
69-
70-
(defun (result-is-true offset)
71-
(eq! (shift RES offset) 1))
72-
73-
(defconstraint address-is-twenty-bytes (:guard FIRST)
74-
(begin
75-
(wcpcall-leq ROW_OFFSET_ADDRESS 0 TRM_ADDRESS_HI RAW_ADDRESS_LO TWOFIFTYSIX_TO_THE_FOUR 0)
76-
(result-is-true ROW_OFFSET_ADDRESS)))
77-
78-
(defconstraint leading-bytes-is-twelve-bytes (:guard FIRST)
79-
(begin
80-
(eq! (shift INST ROW_OFFSET_ADDRESS_TRM) WCP_INST_LEQ)
81-
(vanishes! (shift ARG_1_HI ROW_OFFSET_ADDRESS_TRM))
82-
(vanishes! (shift ARG_2_HI ROW_OFFSET_ADDRESS_TRM))
83-
(eq! (shift ARG_2_LO ROW_OFFSET_ADDRESS_TRM) TWOFIFTYSIX_TO_THE_TWELVE_MO)
84-
(result-is-true ROW_OFFSET_ADDRESS_TRM)))
85-
86-
(defconstraint address-is-not-zero (:guard FIRST)
87-
(begin
88-
(eq! (shift INST ROW_OFFSET_NON_ZERO_ADDR) EVM_INST_ISZERO)
89-
(eq! (shift ARG_1_HI ROW_OFFSET_NON_ZERO_ADDR) TRM_ADDRESS_HI)
90-
(eq! (shift ARG_2_HI ROW_OFFSET_NON_ZERO_ADDR) RAW_ADDRESS_LO)
91-
))
92-
93-
(defconstraint address-is-prc-range (:guard FIRST)
94-
(wcpcall-leq ROW_OFFSET_PRC_ADDR TRM_ADDRESS_HI RAW_ADDRESS_LO 0 NUMBER_OF_PRECOMPILES))
95-
96-
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
97-
;; ;;
98-
;; 2.5 target constraints ;;
74+
;; 1.5 target constraints ;;
9975
;; ;;
10076
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
101-
(defconstraint setting-precompile (:guard FIRST)
102-
(eq! IS_PRECOMPILE
103-
(* (shift RES ROW_OFFSET_PRC_ADDR)
104-
(- 1 (shift RES ROW_OFFSET_NON_ZERA_ADDR)))))
105-
106-
(defun (leading-byte)
107-
(shift ARG_1_LO ROW_OFFSET_ADDRESS_TRM))
108-
109-
(defconstraint proving-trm (:guard FIRST)
110-
(eq! RAW_ADDRESS_HI
111-
(+ (* TWOFIFTYSIX_TO_THE_FOUR (leading-byte))
112-
TRM_ADDRESS_HI)))
113-
77+
(defconstraint target-constraint ()
78+
(if-eq CT LLARGEMO
79+
(begin (eq! RAW_ADDRESS_HI ACC_HI)
80+
(eq! RAW_ADDRESS_LO ACC_LO)
81+
(eq! TRM_ADDRESS_HI ACC_T))))
82+
83+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
84+
;; ;;
85+
;; 2.4 Identifying precompiles ;;
86+
;; ;;
87+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
88+
(defconstraint is-prec-constraint ()
89+
(if-eq CT LLARGEMO
90+
(if-zero (+ TRM_ADDRESS_HI (- RAW_ADDRESS_LO BYTE_LO))
91+
(if-zero BYTE_LO
92+
(vanishes! IS_PRECOMPILE)
93+
(eq! (+ (* (- 9 BYTE_LO)
94+
(- (* 2 IS_PRECOMPILE) 1))
95+
(- IS_PRECOMPILE 1))
96+
(reduce +
97+
(for k
98+
[0 : 7]
99+
(* (^ 2 k)
100+
(shift ONE (- 0 k)))))))
101+
(vanishes! IS_PRECOMPILE))))
114102

115103

‎trm/lookups/trm_into_wvp.lisp

Lines changed: 0 additions & 20 deletions
This file was deleted.

0 commit comments

Comments
 (0)