Skip to content

Commit ab7d065

Browse files
letypequividelespoubellesletypequividelespoubelles
committed
feat: TRM reimplem
Signed-off-by: F Bojarski <[email protected]>
1 parent 3b387d6 commit ab7d065

File tree

5 files changed

+124
-72
lines changed

5 files changed

+124
-72
lines changed

‎constants/constants.lisp‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -252,11 +252,23 @@
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)
255266
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
256267
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;
257268
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; PRECOMPILES ;;
258269
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;
259270
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
271+
NUMBER_OF_PRECOMPILES 9 ;;London value
260272
PRC_ECPAIRING_SIZE (* 6 WORD_SIZE)
261273
PRC_BLAKE2F_SIZE 213
262274
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

‎trm/columns.lisp‎

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

33
(defcolumns
4-
(STAMP :i24)
4+
(STAMP :i40)
5+
(FIRST :binary)
56
(RAW_ADDRESS_HI :i128)
67
(RAW_ADDRESS_LO :i128)
78
(TRM_ADDRESS_HI :i32)
8-
(IS_PRECOMPILE :binary@prove)
9+
(IS_PRECOMPILE :binary)
910
(CT :i4)
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)
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+
)

‎trm/constants.lisp‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
(module trm)
2+
3+
(defconst
4+
TRM_CT_MAX 3
5+
TRM_NB_ROWS (+ TRM_CT_MAX 1)
6+
ROW_OFFSET_ADDRESS 0
7+
ROW_OFFSET_ADDRESS_TRM 1
8+
ROW_OFFSET_NON_ZERA_ADDR 2
9+
ROW_OFFSET_PRC_ADDR 3
10+
)

‎trm/constraints.lisp‎

Lines changed: 72 additions & 60 deletions
Original file line numberDiff line numberDiff line change
@@ -9,31 +9,39 @@
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+
1215
;; 3
1316
(defconstraint null-stamp-null-columns ()
1417
(if-zero STAMP
1518
(begin (vanishes! RAW_ADDRESS_HI)
1619
(vanishes! RAW_ADDRESS_LO)
1720
(vanishes! TRM_ADDRESS_HI)
1821
(vanishes! IS_PRECOMPILE)
22+
(vanishes! (next CT))
1923
(debug (vanishes! CT))
2024
(debug (vanishes! BYTE_HI))
2125
(debug (vanishes! BYTE_LO)))))
2226

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
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+
3442
(defconstraint last-row (:domain {-1})
3543
(if-not-zero STAMP
36-
(eq! CT LLARGEMO)))
44+
(eq! CT TRM_CT_MAX)))
3745

3846
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
3947
;; ;;
@@ -46,58 +54,62 @@
4654
(stamp-constancy STAMP IS_PRECOMPILE)
4755
(stamp-constancy STAMP TRM_ADDRESS_HI)))
4856

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))))
7157

7258
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
7359
;; ;;
74-
;; 1.5 target constraints ;;
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 ;;
7599
;; ;;
76100
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
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))))
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+
102114

103115

‎trm/lookups/trm_into_wvp.lisp‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
(deflookup
2+
trm-into-wcp
3+
; target columns
4+
(
5+
wcp.ARGUMENT_1_HI
6+
wcp.ARGUMENT_1_LO
7+
wcp.ARGUMENT_2_HI
8+
wcp.ARGUMENT_2_LO
9+
wcp.RESULT
10+
wcp.INST
11+
)
12+
; source columns
13+
(
14+
trm.ARGUMENT_1_HI
15+
trm.ARGUMENT_1_LO
16+
trm.ARGUMENT_2_HI
17+
trm.ARGUMENT_2_LO
18+
trm.RESULT
19+
trm.INST
20+
))

0 commit comments

Comments
 (0)