Skip to content

Commit 5fc5f6f

Browse files
letypequividelespoubellesletypequividelespoubelles
committed
ras
Signed-off-by: F Bojarski <[email protected]>
1 parent 661a290 commit 5fc5f6f

File tree

2 files changed

+48
-51
lines changed

2 files changed

+48
-51
lines changed

‎rlptxrcpt/osaka/columns.lisp‎

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -10,10 +10,7 @@
1010
(LIMB_CONSTRUCTED :binary@prove)
1111
(INDEX :i24)
1212
(INDEX_LOCAL :i24)
13-
(PHASE_1 :binary@prove )
14-
(PHASE_2 :binary@prove )
15-
(PHASE_3 :binary@prove )
16-
(PHASE_5 :binary@prove )
13+
(PHASE :binary@prove :array [5])
1714
(PHASE_END :binary@prove)
1815
(COUNTER :i32)
1916
(nSTEP :i32)

‎rlptxrcpt/osaka/constraints.lisp‎

Lines changed: 47 additions & 47 deletions
Original file line numberDiff line numberDiff line change
@@ -50,7 +50,7 @@
5050
(counter-constant IS_DATA)))
5151

5252
(defconstraint special-ct-constancy ()
53-
(if-not-zero (+ (- 1 PHASE_5) (- 1 DEPTH_1) IS_PREFIX (- 1 IS_DATA))
53+
(if-not-zero (+ (- 1 [PHASE 5]) (- 1 DEPTH_1) IS_PREFIX (- 1 IS_DATA))
5454
(counter-constant [INPUT 1])))
5555

5656
(defconstraint ct-incrementing ()
@@ -59,21 +59,21 @@
5959
(counter-incrementing LC_CORRECTION)))
6060

6161
(defconstraint phase5-incrementing ()
62-
(phase-incrementing PHASE_5 DEPTH_1))
62+
(phase-incrementing [PHASE 5] DEPTH_1))
6363

6464
(defconstraint is-topic-incrementing ()
6565
(phase-incrementing IS_TOPIC INDEX_LOCAL))
6666

6767
(defconstraint phase1-constant ()
68-
(phase-constancy PHASE_1 TXRCPT_SIZE))
68+
(phase-constancy [PHASE 1] TXRCPT_SIZE))
6969

7070
;; 4.1.2 Global Phase Constraints ;;
7171
(defconstraint impose-phase-id ()
7272
(eq! PHASE_ID
73-
(+ (* 1 PHASE_1)
74-
(* 2 PHASE_2)
75-
(* 3 PHASE_3)
76-
(* 5 PHASE_5)
73+
(+ (* 1 [PHASE 1])
74+
(* 2 [PHASE 2])
75+
(* 3 [PHASE 3])
76+
(* 5 [PHASE 5])
7777
(* SUBPHASE_ID_WEIGHT_IS_PREFIX IS_PREFIX)
7878
(* SUBPHASE_ID_WEIGHT_IS_OT IS_TOPIC)
7979
(* SUBPHASE_ID_WEIGHT_IS_OD IS_DATA)
@@ -84,22 +84,22 @@
8484
(begin (vanishes! ABS_TX_NUM)
8585
(vanishes! ABS_LOG_NUM)))
8686

87-
(defun (phase-sum) (+ PHASE_1 PHASE_2 PHASE_3 PHASE_5))
87+
(defun (phase-sum) (+ [PHASE 1] [PHASE 2] [PHASE 3] [PHASE 5]))
8888

8989
(defconstraint phase-exclusion ()
9090
(if-zero ABS_TX_NUM
9191
(vanishes! (phase-sum))
9292
(eq! 1 (phase-sum))))
9393

9494
(defconstraint ABS_TX_NUM-evolution ()
95-
(if (or! (eq! PHASE_1 0) (remained-constant! PHASE_1))
95+
(if (or! (eq! [PHASE 1] 0) (remained-constant! [PHASE 1]))
9696
;; no change
9797
(remained-constant! ABS_TX_NUM)
9898
;; increment
9999
(did-inc! ABS_TX_NUM 1)))
100100

101101
(defconstraint ABS_LOG_NUM-evolution ()
102-
(if-zero (+ (- 1 PHASE_5) (- 1 DEPTH_1) (- 1 IS_PREFIX) IS_TOPIC IS_DATA CT)
102+
(if-zero (+ (- 1 [PHASE 5]) (- 1 DEPTH_1) (- 1 IS_PREFIX) IS_TOPIC IS_DATA CT)
103103
(did-inc! ABS_LOG_NUM 1)
104104
(remained-constant! ABS_LOG_NUM)))
105105

@@ -111,27 +111,27 @@
111111
(if-not-zero PHASE_SIZE
112112
(vanishes! PHASE_END)))
113113

114-
(defun (phase-wght-sum) (+ PHASE_1
115-
(* 2 PHASE_2)
116-
(* 3 PHASE_3)
117-
(* 5 PHASE_5)))
114+
(defun (phase-wght-sum) (+ [PHASE 1]
115+
(* 2 [PHASE 2])
116+
(* 3 [PHASE 3])
117+
(* 5 [PHASE 5])))
118118

119119
(defconstraint no-end-no-change-phase (:guard ABS_TX_NUM)
120120
(if-zero PHASE_END
121121
(eq! (phase-wght-sum)
122-
(+ (next PHASE_1)
123-
(* 2 (next PHASE_2))
124-
(* 3 (next PHASE_3))
125-
(* 5 (next PHASE_5))))))
122+
(+ (next [PHASE 1])
123+
(* 2 (next [PHASE 2]))
124+
(* 3 (next [PHASE 3]))
125+
(* 5 (next [PHASE 5]))))))
126126

127127
(defconstraint phase-transition ()
128128
(if-eq PHASE_END 1
129129
(begin (eq! 1
130-
(+ (* PHASE_1 (next PHASE_2))
131-
(* PHASE_2 (next PHASE_3))
132-
(* PHASE_3 (next PHASE_5))
133-
(* PHASE_5 (next PHASE_1))))
134-
(if-eq PHASE_5 1 (vanishes! TXRCPT_SIZE)))))
130+
(+ (* [PHASE 1] (next [PHASE 2]))
131+
(* [PHASE 2] (next [PHASE 3]))
132+
(* [PHASE 3] (next [PHASE 5]))
133+
(* [PHASE 5] (next [PHASE 1]))))
134+
(if-eq [PHASE 5] 1 (vanishes! TXRCPT_SIZE)))))
135135

136136
;; 4.1.3 Byte decomposition's loop heartbeat ;;
137137
(defconstraint ct-imply-done (:guard ABS_TX_NUM)
@@ -166,25 +166,25 @@
166166

167167
;; 4.1.6 Byte size updates ;;
168168
(defconstraint globalsize-update ()
169-
(if-zero PHASE_1
169+
(if-zero [PHASE 1]
170170
(eq! TXRCPT_SIZE
171171
(- (prev TXRCPT_SIZE) (* LC nBYTES)))))
172172

173173
(defconstraint phase-size-update ()
174-
(if-eq 1 (* PHASE_5 DEPTH_1)
174+
(if-eq 1 (* [PHASE 5] DEPTH_1)
175175
(eq! PHASE_SIZE
176176
(- (prev PHASE_SIZE) (* LC nBYTES)))))
177177

178178
;; LC correction nullity ;;
179179
(defconstraint lc-correction-nullity ()
180-
(if-zero (+ PHASE_1 (* PHASE_5 IS_DATA))
180+
(if-zero (+ [PHASE 1] (* [PHASE 5] IS_DATA))
181181
(vanishes! LC_CORRECTION)))
182182

183183
;; 4.1.8 Finalization Constraints ;;
184184
(defconstraint finalization (:domain {-1})
185185
(if-not-zero ABS_TX_NUM
186186
(begin (eq! PHASE_END 1)
187-
(eq! PHASE_5 1)
187+
(eq! [PHASE 5] 1)
188188
(eq! ABS_TX_NUM ABS_TX_NUM_MAX)
189189
(eq! ABS_LOG_NUM ABS_LOG_NUM_MAX))))
190190

@@ -194,8 +194,8 @@
194194
;; ;;
195195
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
196196
;; 4.2.1 Phase 1 : RLP prefix ;;
197-
(defconstraint phase1-init (:guard PHASE_1);; 4.1.1
198-
(if-zero (prev PHASE_1)
197+
(defconstraint phase1-init (:guard [PHASE 1]);; 4.1.1
198+
(if-zero (prev [PHASE 1])
199199
(begin (vanishes! (+ (- 1 IS_PREFIX) PHASE_END (next IS_PREFIX)))
200200
(eq! nSTEP 1)
201201
(if-zero [INPUT 1]
@@ -205,17 +205,17 @@
205205
(* [INPUT 1] (^ 256 LLARGEMO)))
206206
(eq! nBYTES 1))))))
207207

208-
(defconstraint phase1-rlprefix (:guard PHASE_1)
208+
(defconstraint phase1-rlprefix (:guard [PHASE 1])
209209
(if-zero IS_PREFIX
210210
(begin (eq! nSTEP 8)
211211
(vanishes! LC_CORRECTION)
212212
(eq! [INPUT 1] TXRCPT_SIZE)
213-
(rlpPrefixOfByteString [INPUT 1] CT nSTEP DONE PHASE_1 ACC_SIZE POWER BIT [ACC 1] [ACC 2] LC LIMB nBYTES)
213+
(rlpPrefixOfByteString [INPUT 1] CT nSTEP DONE [PHASE 1] ACC_SIZE POWER BIT [ACC 1] [ACC 2] LC LIMB nBYTES)
214214
(if-eq DONE 1 (eq! PHASE_END 1)))))
215215

216216
;; 4.2.2 Phase 2 : status code Rz ;;
217217
(defconstraint phase2 ()
218-
(if-eq PHASE_2 1
218+
(if-eq [PHASE 2] 1
219219
(begin (eq! nSTEP 1)
220220
(if-zero [INPUT 1]
221221
(eq! LIMB
@@ -227,19 +227,19 @@
227227

228228
;; 4.2.3 Phase 3 : cumulative gas Ru ;;
229229
(defconstraint phase3 ()
230-
(if-eq PHASE_3 1
230+
(if-eq [PHASE 3] 1
231231
(begin (eq! nSTEP 8)
232232
(rlpPrefixInt [INPUT 1] CT nSTEP DONE [BYTE 1] [ACC 1] ACC_SIZE POWER BIT BIT_ACC LIMB LC nBYTES)
233233
(if-eq DONE 1
234234
(begin (limbShifting [INPUT 1] POWER ACC_SIZE LIMB nBYTES)
235235
(eq! PHASE_END 1))))))
236236

237237
;; Phase 5: log series Rl ;;
238-
(defconstraint phase5-init (:guard PHASE_5)
239-
(if-zero (prev PHASE_5)
238+
(defconstraint phase5-init (:guard [PHASE 5])
239+
(if-zero (prev [PHASE 5])
240240
(vanishes! (+ DEPTH_1 (- 1 IS_PREFIX) IS_TOPIC IS_DATA))))
241241

242-
(defconstraint phase5-phaseRlpPrefix (:guard PHASE_5)
242+
(defconstraint phase5-phaseRlpPrefix (:guard [PHASE 5])
243243
(if-zero DEPTH_1
244244
(begin (eq! [INPUT 1] PHASE_SIZE)
245245
(if-zero [INPUT 1]
@@ -249,22 +249,22 @@
249249
(eq! nBYTES 1)
250250
(eq! PHASE_END 1))
251251
(begin (eq! nSTEP 8)
252-
(rlpPrefixOfByteString [INPUT 1] CT nSTEP DONE PHASE_5 ACC_SIZE POWER BIT [ACC 1] [ACC 2] LC LIMB nBYTES)
252+
(rlpPrefixOfByteString [INPUT 1] CT nSTEP DONE [PHASE 5] ACC_SIZE POWER BIT [ACC 1] [ACC 2] LC LIMB nBYTES)
253253
(if-eq DONE 1
254254
(vanishes! (+ (- 1 (next DEPTH_1))
255255
(- 1 (next IS_PREFIX))
256256
(next IS_TOPIC)
257257
(next IS_DATA)))))))))
258258

259-
(defconstraint phase5-logentryRlpPrefix (:guard PHASE_5)
259+
(defconstraint phase5-logentryRlpPrefix (:guard [PHASE 5])
260260
(if-eq 1 (* DEPTH_1 IS_PREFIX (- 1 IS_TOPIC) (- 1 IS_DATA))
261261
(begin (eq! [INPUT 1] LOG_ENTRY_SIZE)
262262
(eq! nSTEP 8)
263-
(rlpPrefixOfByteString [INPUT 1] CT nSTEP DONE PHASE_5 ACC_SIZE POWER BIT [ACC 1] [ACC 2] LC LIMB nBYTES)
263+
(rlpPrefixOfByteString [INPUT 1] CT nSTEP DONE [PHASE 5] ACC_SIZE POWER BIT [ACC 1] [ACC 2] LC LIMB nBYTES)
264264
(if-eq DONE 1
265265
(vanishes! (+ (next IS_PREFIX) (next IS_TOPIC) (next IS_DATA)))))))
266266

267-
(defconstraint phase5-rlpAddress (:guard PHASE_5)
267+
(defconstraint phase5-rlpAddress (:guard [PHASE 5])
268268
(if-zero (+ IS_PREFIX IS_TOPIC IS_DATA)
269269
(begin (eq! nSTEP 3)
270270
(eq! LC 1)
@@ -281,7 +281,7 @@
281281
(- 1 (next IS_TOPIC))
282282
(next IS_DATA))))))))
283283

284-
(defconstraint phase5-topic-prefix (:guard PHASE_5)
284+
(defconstraint phase5-topic-prefix (:guard [PHASE 5])
285285
(if-eq (* IS_PREFIX IS_TOPIC) 1
286286
(begin (vanishes! INDEX_LOCAL)
287287
(eq! nSTEP 1)
@@ -306,7 +306,7 @@
306306
(- 1 (next IS_TOPIC))
307307
(next IS_DATA))))))))
308308

309-
(defconstraint phase5-topic (:guard PHASE_5)
309+
(defconstraint phase5-topic (:guard [PHASE 5])
310310
(if-zero (+ IS_PREFIX (- 1 IS_TOPIC))
311311
(begin (eq! nSTEP 3)
312312
(eq! LC 1)
@@ -330,7 +330,7 @@
330330
(- 1 (next IS_TOPIC))
331331
(next IS_DATA)))))))))
332332

333-
(defconstraint phase5-dataprefix (:guard PHASE_5)
333+
(defconstraint phase5-dataprefix (:guard [PHASE 5])
334334
(if-eq (* IS_PREFIX IS_DATA) 1
335335
(begin (eq! [INPUT 1] LOCAL_SIZE)
336336
(if-zero LOCAL_SIZE
@@ -372,7 +372,7 @@
372372
CT
373373
nSTEP
374374
DONE
375-
PHASE_1
375+
[PHASE 1]
376376
ACC_SIZE
377377
POWER
378378
BIT
@@ -386,7 +386,7 @@
386386
(next IS_TOPIC)
387387
(- 1 (next IS_DATA))))))))))
388388

389-
(defconstraint phase5-data (:guard PHASE_5)
389+
(defconstraint phase5-data (:guard [PHASE 5])
390390
(if-zero (+ IS_PREFIX (- 1 IS_DATA))
391391
(begin (eq! INDEX_LOCAL CT)
392392
(eq! LC 1)
@@ -401,13 +401,13 @@
401401
(next IS_TOPIC)
402402
(next IS_DATA)))))))))
403403

404-
(defconstraint phase5-logEntrySize-update (:guard PHASE_5)
404+
(defconstraint phase5-logEntrySize-update (:guard [PHASE 5])
405405
(if-zero (+ (- 1 DEPTH_1)
406406
(* IS_PREFIX (- 1 IS_TOPIC) (- 1 IS_DATA)))
407407
(eq! LOG_ENTRY_SIZE
408408
(- (prev LOG_ENTRY_SIZE) (* LC nBYTES)))))
409409

410-
(defconstraint phase5-localsize-update (:guard PHASE_5)
410+
(defconstraint phase5-localsize-update (:guard [PHASE 5])
411411
(if-zero (+ IS_PREFIX
412412
(- 1 (+ IS_TOPIC IS_DATA)))
413413
(eq! LOCAL_SIZE

0 commit comments

Comments
 (0)