Skip to content

Commit

Permalink
perf: bin adaptative line (#66)
Browse files Browse the repository at this point in the history
  • Loading branch information
@letypequividelespoubelles @OlivierBBB
letypequividelespoubelles authored and OlivierBBB committed Feb 21, 2024
1 parent 9c8e6b7 commit bee0faf
Show file tree
Hide file tree
Showing 2 changed files with 105 additions and 120 deletions.
66 changes: 32 additions & 34 deletions bin/columns.lisp
View file
Original file line number Diff line number Diff line change
@@ -1,49 +1,47 @@
(module bin)

(defcolumns
STAMP
(ONE_LINE_INSTRUCTION :binary)
(MLI :binary)
(STAMP :i32)
(CT_MAX :byte)
(COUNTER :byte)
(INST :byte :display :opcode)
ARGUMENT_1_HI
ARGUMENT_1_LO
ARGUMENT_2_HI
ARGUMENT_2_LO
RESULT_HI
RESULT_LO
(IS_AND :binary)
(IS_OR :binary)
(IS_XOR :binary)
(IS_NOT :binary)
(IS_BYTE :binary)
(IS_SIGNEXTEND :binary)
(SMALL :binary)
(BITS :binary)
(BIT_B_4 :binary)
(LOW_4 :byte)
(NEG :binary)
(BIT_1 :binary)
(ARGUMENT_1_HI :i128)
(ARGUMENT_1_LO :i128)
(ARGUMENT_2_HI :i128)
(ARGUMENT_2_LO :i128)
(RESULT_HI :i128)
(RESULT_LO :i128)
(IS_AND :binary@prove)
(IS_OR :binary@prove)
(IS_XOR :binary@prove)
(IS_NOT :binary@prove)
(IS_BYTE :binary@prove)
(IS_SIGNEXTEND :binary@prove)
(SMALL :binary@prove)
(BITS :binary@prove)
(BIT_B_4 :binary@prove)
(LOW_4 :byte@prove)
(NEG :binary@prove)
(BIT_1 :binary@prove)
(PIVOT :byte)
(BYTE_1 :byte)
(BYTE_2 :byte)
(BYTE_3 :byte)
(BYTE_4 :byte)
(BYTE_5 :byte)
(BYTE_6 :byte)
ACC_1
ACC_2
ACC_3
ACC_4
ACC_5
ACC_6
(BYTE_1 :byte@prove)
(BYTE_2 :byte@prove)
(BYTE_3 :byte@prove)
(BYTE_4 :byte@prove)
(BYTE_5 :byte@prove)
(BYTE_6 :byte@prove)
(ACC_1 :i128)
(ACC_2 :i128)
(ACC_3 :i128)
(ACC_4 :i128)
(ACC_5 :i128)
(ACC_6 :i128)
;; decoded bytes:
(XXX_BYTE_HI :byte)
(XXX_BYTE_LO :byte))

;; aliases
(defalias
OLI ONE_LINE_INSTRUCTION
CT COUNTER
ARG_1_HI ARGUMENT_1_HI
ARG_1_LO ARGUMENT_1_LO
Expand Down
159 changes: 73 additions & 86 deletions bin/constraints.lisp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,21 +17,6 @@
THEN
ELSE))

;; 2.1 binary constraints
;; binary constraints
(defconstraint binary_constraints ()
(begin (is-binary IS_AND)
(is-binary IS_OR)
(is-binary IS_XOR)
(is-binary IS_NOT)
(is-binary IS_BYTE)
(is-binary IS_SIGNEXTEND)
(is-binary SMALL)
(is-binary BITS)
(is-binary NEG)
(is-binary BIT_B_4)
(is-binary BIT_1)))

;; 2.2 Shorthands
(defun (flag-sum)
(+ IS_AND IS_OR IS_XOR IS_NOT IS_BYTE IS_SIGNEXTEND))
Expand Down Expand Up @@ -60,18 +45,28 @@
(defconstraint stamp-increments ()
(vanishes! (* (will-inc! STAMP 0) (will-inc! STAMP 1))))

(defconstraint countereset ()
(if-not-zero (will-remain-constant! STAMP)
(defconstraint new-stamp-reset-ct ()
(if-not-zero (- (next STAMP) STAMP)
(vanishes! (next CT))))

(defconstraint oli-incrementation (:guard OLI)
(will-inc! STAMP 1))
(defconstraint isnot-ctmax ()
(if-eq IS_NOT 1 (eq! CT_MAX LLARGEMO)))

(defconstraint isbyte-ctmax ()
(if-eq (+ IS_BYTE IS_SIGNEXTEND) 1
(if-zero ARG_1_HI
(eq! CT_MAX LLARGEMO)
(vanishes! CT_MAX))))

(defconstraint ct-small ()
(eq! 1
(~ (- CT LLARGE))))

(defconstraint mli-incrementation (:guard MLI)
(if-eq-else CT LLARGEMO (will-inc! STAMP 1) (will-inc! CT 1)))
(defconstraint countereset (:guard STAMP)
(if-eq-else CT CT_MAX (will-inc! STAMP 1) (will-inc! CT 1)))

(defconstraint last-row (:domain {-1})
(if-eq MLI 1 (eq! CT LLARGEMO)))
(eq! CT CT_MAX))

(defconstraint counter-constancies ()
(begin (counter-constancy CT ARG_1_HI)
Expand All @@ -81,10 +76,12 @@
(counter-constancy CT RES_HI)
(counter-constancy CT RES_LO)
(counter-constancy CT INST)
(counter-constancy CT CT_MAX)
(counter-constancy CT PIVOT)
(counter-constancy CT BIT_B_4)
(counter-constancy CT LOW_4)
(counter-constancy CT NEG)))
(counter-constancy CT NEG)
(counter-constancy CT SMALL)))

;; 2.6 byte decompositions
(defconstraint byte_decompositions ()
Expand All @@ -97,7 +94,7 @@

;; 2.7 target constraints
(defconstraint target-constraints ()
(if-eq CT LLARGEMO
(if-eq CT CT_MAX
(begin (eq! ACC_1 ARG_1_HI)
(eq! ACC_2 ARG_1_LO)
(eq! ACC_3 ARG_2_HI)
Expand All @@ -110,18 +107,8 @@
;; 2.8 binary column constraints ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defconstraint set-oli-mli ()
(if-zero (+ IS_BYTE IS_SIGNEXTEND)
(vanishes! OLI)
(if-zero ARG_1_HI
(vanishes! OLI)
(eq! OLI 1))))

(defconstraint oli-mli-exclusivity ()
(eq! (+ OLI MLI) (flag-sum)))

;; 2.8.2 BITS and related columns
(defconstraint bits-and-related ()
(defconstraint bits-and-related (:guard (+ IS_BYTE IS_SIGNEXTEND))
(if-eq CT LLARGEMO
(begin (eq! PIVOT
(+ (* 128 (shift BITS -15))
Expand Down Expand Up @@ -150,13 +137,13 @@
(eq! NEG (shift BITS -15)))))

;; 2.8.3 [[1]] constraints
(defconstraint bit_1 ()
(defconstraint bit_1 (:guard CT_MAX)
(begin (if-eq IS_BYTE 1 (plateau-constraint CT BIT_1 LOW_4))
(if-eq IS_SIGNEXTEND 1
(plateau-constraint CT BIT_1 (- LLARGEMO LOW_4)))))

;; 2.8.4 SMALL constraints
(defconstraint small ()
(defconstraint small (:guard (+ IS_BYTE IS_SIGNEXTEND))
(if-eq CT LLARGEMO
(if-zero ARG_1_HI
(if-eq-else ARG_1_LO (+ (* 16 (shift BITS -4))
Expand All @@ -168,64 +155,64 @@
(vanishes! SMALL)))))

;; 2.9 pivot constraints
(defconstraint pivot (:guard MLI)
(begin (if-not-zero IS_BYTE
(if-zero LOW_4
(if-zero CT
(if-zero BIT_B_4
(eq! PIVOT BYTE_3)
(eq! PIVOT BYTE_4)))
(if-zero (+ (prev BIT_1) (- 1 BIT_1))
(if-zero BIT_B_4
(eq! PIVOT BYTE_3)
(eq! PIVOT BYTE_4)))))
(if-not-zero IS_SIGNEXTEND
(if-eq-else LOW_4 LLARGEMO
(if-zero CT
(if-zero BIT_B_4
(eq! PIVOT BYTE_4)
(eq! PIVOT BYTE_3)))
(if-zero (+ (prev BIT_1) (- 1 BIT_1))
(if-zero BIT_B_4
(eq! PIVOT BYTE_4)
(eq! PIVOT BYTE_3)))))))
(defconstraint pivot (:guard CT_MAX)
(begin (if-eq IS_BYTE 1
(if-zero LOW_4
(if-zero CT
(if-zero BIT_B_4
(eq! PIVOT BYTE_3)
(eq! PIVOT BYTE_4)))
(if-zero (+ (prev BIT_1) (- 1 BIT_1))
(if-zero BIT_B_4
(eq! PIVOT BYTE_3)
(eq! PIVOT BYTE_4)))))
(if-eq IS_SIGNEXTEND 1
(if-eq-else LOW_4 LLARGEMO
(if-zero CT
(if-zero BIT_B_4
(eq! PIVOT BYTE_4)
(eq! PIVOT BYTE_3)))
(if-zero (+ (prev BIT_1) (- 1 BIT_1))
(if-zero BIT_B_4
(eq! PIVOT BYTE_4)
(eq! PIVOT BYTE_3)))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; 2.10 result constraints ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defconstraint is-byte-result (:guard IS_BYTE)
(if-eq-else OLI 1
(begin (vanishes! RES_HI)
(vanishes! RES_LO))
(begin (vanishes! RES_HI)
(eq! RES_LO (* SMALL PIVOT)))))
(if-zero CT_MAX
(begin (vanishes! RES_HI)
(vanishes! RES_LO))
(begin (vanishes! RES_HI)
(eq! RES_LO (* SMALL PIVOT)))))

(defconstraint is-signextend-result (:guard IS_SIGNEXTEND)
(if-eq-else OLI 1
(begin (eq! RES_HI ARG_2_HI)
(eq! RES_LO ARG_2_LO))
(if-zero SMALL
;; SMALL == 0
(begin (eq! RES_HI ARG_2_HI)
(eq! RES_LO ARG_2_LO))
;; SMALL == 1
(begin (if-zero BIT_B_4
;; b4 == 0
(begin (eq! BYTE_5 (* NEG 255))
(if-zero BIT_1
;; [[1]] == 0
(eq! BYTE_6 (* NEG 255))
;; [[1]] == 1
(eq! BYTE_6 BYTE_4)))
;; b4 == 1
(begin (if-zero BIT_1
;; [[1]] == 0
(eq! BYTE_5 (* NEG 255))
;; [[1]] == 1
(eq! BYTE_5 BYTE_3))
(eq! RES_LO ARG_2_LO)))))))
(if-zero CT_MAX
(begin (eq! RES_HI ARG_2_HI)
(eq! RES_LO ARG_2_LO))
(if-zero SMALL
;; SMALL == 0
(begin (eq! RES_HI ARG_2_HI)
(eq! RES_LO ARG_2_LO))
;; SMALL == 1
(begin (if-zero BIT_B_4
;; b4 == 0
(begin (eq! BYTE_5 (* NEG 255))
(if-zero BIT_1
;; [[1]] == 0
(eq! BYTE_6 (* NEG 255))
;; [[1]] == 1
(eq! BYTE_6 BYTE_4)))
;; b4 == 1
(begin (if-zero BIT_1
;; [[1]] == 0
(eq! BYTE_5 (* NEG 255))
;; [[1]] == 1
(eq! BYTE_5 BYTE_3))
(eq! RES_LO ARG_2_LO)))))))

(defconstraint result-via-lookup (:guard (+ IS_AND IS_OR IS_XOR IS_NOT))
(begin (eq! BYTE_5 XXX_BYTE_HI)
Expand Down

0 comments on commit bee0faf

Please sign in to comment.