Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Trm constraints #34

Merged
merged 7 commits into from
Nov 3, 2023
Merged

Trm constraints #34

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
284cbc6
add trm constraints
letypequividelespoubelles Jun 23, 2023
621c20b
delete .bin
letypequividelespoubelles Jun 23, 2023
c697a98
Formatting
delehef Jun 23, 2023
8683451
style: style
letypequividelespoubelles Oct 27, 2023
e79e00e
fix(trm): fix rebase
letypequividelespoubelles Oct 27, 2023
af02777
refactor: ras
letypequividelespoubelles Oct 30, 2023
1ea2155
refactor: delete old trm constraints
letypequividelespoubelles Nov 2, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -70,6 +70,8 @@ RLP_TXRCPT := rlp_txrcpt/columns.lisp rlp_txrcpt/constraints.lisp

LIBRARY := library/constant.lisp library/rlp_constraints_pattern.lisp

TRM := trm/columns.lisp trm/constraints.lisp

ZKEVM_MODULES := ${LIBRARY} \
${ALU} \
${BIN} \
Expand All @@ -87,6 +89,7 @@ ZKEVM_MODULES := ${LIBRARY} \
${TABLES} \
${TXN_DATA} \
${WCP} \
${TRM}

define.go: ${ZKEVM_MODULES}
${CORSET} wizard-iop -vv -P define -o $@ ${ZKEVM_MODULES}
Expand Down
6 changes: 3 additions & 3 deletions rlp_txrcpt/constraints.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,16 +75,16 @@
(counter-incrementing LC))
(counter-incrementing LC_CORRECTION)))

(defconstraint phase3-decrementing ()
(defconstraint phase4-decrementing ()
(phase-decrementing [PHASE 4] IS_PREFIX))

(defconstraint phase4-incrementing ()
(defconstraint phase5-incrementing ()
(phase-incrementing [PHASE 5] DEPTH_1))

(defconstraint istopic-incrementing ()
(phase-incrementing IS_TOPIC INDEX_LOCAL))

(defconstraint phase0-constant ()
(defconstraint phase1-constant ()
(phase-constancy [PHASE 1] TXRCPT_SIZE))

;; 4.1.2 Global Phase Constraints ;;
Expand Down
34 changes: 17 additions & 17 deletions trm/columns.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,19 +1,19 @@
(module trm)

(defcolumns
STAMP
ADDR_HI
ADDR_LO
TRM_ADDR_HI
(IS_PREC :binary)
;;
CT
(BYTE_HI :byte)
(BYTE_LO :byte)
ACC_HI
ACC_LO
ACC_T
;;
(PBIT :binary)
(ONES :binary)
)
(defcolumns
STAMP
ADDR_HI
ADDR_LO
TRM_ADDR_HI
(IS_PREC :binary)
;;
CT
ACC_HI
ACC_LO
ACC_T
(PBIT :binary)
(ONE :binary)
(BYTE_HI :byte)
(BYTE_LO :byte))


181 changes: 81 additions & 100 deletions trm/constraints.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,125 +1,106 @@
(module trm)

(defconst
MAX_PREC_ADDR 9
LLARGEMO 15)

(defconst
LLARGEMO 15)

;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; 2.1 heartbeat ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;

;; 1
(defconstraint first-row (:domain {0})
(vanishes! STAMP))
(vanishes! STAMP))

;; 3
(defconstraint null-stamp-null-columns ()
(if-zero STAMP
(begin (vanishes! ADDR_HI)
(vanishes! ADDR_LO)
(vanishes! TRM_ADDR_HI)
(vanishes! IS_PREC)
(vanishes! CT)
(vanishes! BYTE_HI)
(vanishes! BYTE_LO))))

(defconstraint heartbeat ()
(begin
(* (will-remain-constant! STAMP) (will-inc! STAMP 1))
(if-not-zero (will-remain-constant! STAMP) (vanishes! (next CT)))
(if-zero STAMP
(begin
(vanishes! ADDR_HI)
(vanishes! ADDR_LO)
(vanishes! TRM_ADDR_HI)
(vanishes! IS_PREC)
(vanishes! CT)
(vanishes! BYTE_HI)
(vanishes! BYTE_LO)))
(if-not-zero STAMP
(if-eq-else CT LLARGEMO
(will-inc! STAMP 1)
(will-inc! CT 1)))))

(begin ;; 2
(or! (will-remain-constant! STAMP) (will-inc! STAMP 1))
;; 4
(if-not-zero (- (next STAMP) STAMP)
(vanishes! (next CT)))
;; 5
(if-not-zero STAMP
(if-eq-else CT LLARGEMO (will-inc! STAMP 1) (will-inc! CT 1)))))

;; 6
(defconstraint last-row (:domain {-1})
(if-not-zero STAMP (= CT LLARGEMO)))
(if-not-zero STAMP
(eq! CT LLARGEMO)))

;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; 2.2 stamp constancy ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;
(defconstraint stamp-constancies ()
(begin (stamp-constancy STAMP ADDR_HI)
(stamp-constancy STAMP ADDR_LO)
(stamp-constancy STAMP IS_PREC)
(stamp-constancy STAMP TRM_ADDR_HI)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; 2.2 stamp constancy ;;
;; 2.3 PBIT constraints ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defconstraint stamp-constancies ()
(begin
(stamp-constancy STAMP ADDR_HI)
(stamp-constancy STAMP ADDR_LO)
(stamp-constancy STAMP TRM_ADDR_HI)
(stamp-constancy STAMP IS_PREC)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; 2.3 Pivot bit constraints ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defconstraint pivot-bit ()
(begin
(is-binary PBIT)
(if-zero CT
(vanishes! PBIT))
(if-not-zero CT
(vanishes! (* (remained-constant! PBIT) (did-inc! PBIT 1))))
(if-eq CT 12
(= 1 (+ PBIT (prev PBIT))))))
(defconstraint pbit-constraint ()
(begin (if-zero CT
(vanishes! PBIT)
(or! (remained-constant! PBIT) (did-inc! PBIT 1)))
(if-eq CT 12
(begin (vanishes! (prev PBIT))
(eq! PBIT 1)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; 2.4 binary, bytehood and byte decompositions ;;
;; 2.4 Byte Decomposition ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defconstraint byte-decompositions ()
(begin (byte-decomposition CT ACC_HI BYTE_HI)
(byte-decomposition CT ACC_LO BYTE_LO)
(byte-decomposition CT ACC_T (* BYTE_HI PBIT))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; 1.5 target constraints ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;)
(defconstraint target-constraint ()
(if-eq CT 15
(begin (eq! ADDR_HI ACC_HI)
(eq! ADDR_LO ACC_LO)
(eq! TRM_ADDR_HI ACC_T))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; 2.4 Identifying precompiles ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defconstraint is-prec-constraint ()
(if-eq CT 15
(if-zero (+ TRM_ADDR_HI (- ADDR_LO BYTE_LO))
(if-zero BYTE_LO
(vanishes! IS_PREC)
(eq! (+ (* (- 9 BYTE_LO)
(- (* 2 IS_PREC) 1))
(- IS_PREC 1))
(reduce +
(for k
[0 : 7]
(* (^ 2 k)
(shift ONE (- 0 k)))))))
(vanishes! IS_PREC))))

(defconstraint binary-and-byte-decompositions ()
(begin
(byte-decomposition CT ACC_HI BYTE_HI)
(byte-decomposition CT ACC_LO BYTE_LO)
(byte-decomposition CT ACC_T (* PBIT BYTE_HI))))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; 2.5 Target constraints ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(defconstraint target-constraints ()
(if-eq CT LLARGEMO
(begin
(= ADDR_HI ACC_HI)
(= ADDR_LO ACC_LO)
(= TRM_ADDR_HI ACC_T))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; 2.6 Identifying precompiles ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defun (bit-decomposition-associated-with-ONES) (+ ONES
(* (shift ONES -1) 2)
(* (shift ONES -2) 4)
(* (shift ONES -3) 8)
(* (shift ONES -4) 16)
(* (shift ONES -5) 32)
(* (shift ONES -6) 64)
(* (shift ONES -7) 128)))

(defconstraint binaryness ()
(begin
(is-binary IS_PREC)
(is-binary ONES)))

(defconstraint identifying-precompiles ()
(if-eq CT LLARGEMO
(begin
(if-not-zero (+ TRM_ADDR_HI (- ADDR_LO BYTE_LO))
(= IS_PREC 0))
(if-zero (+ TRM_ADDR_HI (- ADDR_LO BYTE_LO))
(if-zero BYTE_LO
(= IS_PREC 0)
(=
(+ (* (- MAX_PREC_ADDR BYTE_LO) (- (* 2 IS_PREC) 1) (- IS_PREC 1)))
(bit-decomposition-associated-with-ONES)))))))
19 changes: 0 additions & 19 deletions trm_sally/columns.lisp
View file
Open in desktop

This file was deleted.

Loading