Skip to content

Commit

Permalink
Update Slow Tests
Browse files Browse the repository at this point in the history 
This updates the slow test to be almost exactly as they were original
defined (i.e. using the full corset syntax).  At this stage, there are
a number of outstanding issues which remain, and some of the tests have
parts commented out.
  • Loading branch information
@DavePearce
DavePearce committed Dec 13, 2024
1 parent f737b77 commit 404a7eb
Show file tree
Hide file tree
Showing 5 changed files with 1,087 additions and 195 deletions.
4 changes: 2 additions & 2 deletions pkg/test/valid_corset_test.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -664,10 +664,10 @@ func TestSlow_Wcp(t *testing.T) {
Check(t, true, "wcp")
}

func TestSlow_Mxp(t *testing.T) {
/* func TestSlow_Mxp(t *testing.T) {
Check(t, true, "mxp")
}

*/
// ===================================================================
// Test Helpers
// ===================================================================
Expand Down
230 changes: 209 additions & 21 deletions testdata/bin-dynamic.lisp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(STAMP :i32)
(CT_MAX :byte)
(COUNTER :byte)
(INST :byte)
(INST :byte :display :opcode)
(ARGUMENT_1_HI :i128)
(ARGUMENT_1_LO :i128)
(ARGUMENT_2_HI :i128)
Expand Down Expand Up @@ -40,42 +40,230 @@
(XXX_BYTE_HI :byte)
(XXX_BYTE_LO :byte))

(defconstraint byte_decompositions () (begin (if COUNTER (- ACC_1 BYTE_1) (- ACC_1 (+ (* 256 (shift ACC_1 -1)) BYTE_1))) (if COUNTER (- ACC_2 BYTE_2) (- ACC_2 (+ (* 256 (shift ACC_2 -1)) BYTE_2))) (if COUNTER (- ACC_3 BYTE_3) (- ACC_3 (+ (* 256 (shift ACC_3 -1)) BYTE_3))) (if COUNTER (- ACC_4 BYTE_4) (- ACC_4 (+ (* 256 (shift ACC_4 -1)) BYTE_4))) (if COUNTER (- ACC_5 BYTE_5) (- ACC_5 (+ (* 256 (shift ACC_5 -1)) BYTE_5))) (if COUNTER (- ACC_6 BYTE_6) (- ACC_6 (+ (* 256 (shift ACC_6 -1)) BYTE_6)))))
;; aliases
(defalias
CT COUNTER
ARG_1_HI ARGUMENT_1_HI
ARG_1_LO ARGUMENT_1_LO
ARG_2_HI ARGUMENT_2_HI
ARG_2_LO ARGUMENT_2_LO
RES_HI RESULT_HI
RES_LO RESULT_LO)

(defconstraint bits-and-related () (if (+ IS_BYTE IS_SIGNEXTEND) 0 (if (- COUNTER 15) (begin (- PIVOT (+ (* 128 (shift BITS -15)) (* 64 (shift BITS -14)) (* 32 (shift BITS -13)) (* 16 (shift BITS -12)) (* 8 (shift BITS -11)) (* 4 (shift BITS -10)) (* 2 (shift BITS -9)) (shift BITS -8))) (- BYTE_2 (+ (* 128 (shift BITS -7)) (* 64 (shift BITS -6)) (* 32 (shift BITS -5)) (* 16 (shift BITS -4)) (* 8 (shift BITS -3)) (* 4 (shift BITS -2)) (* 2 (shift BITS -1)) BITS)) (- LOW_4 (+ (* 8 (shift BITS -3)) (* 4 (shift BITS -2)) (* 2 (shift BITS -1)) BITS)) (- BIT_B_4 (shift BITS -4)) (- NEG (shift BITS -15))))))
(defconst
;; opcode values
SIGNEXTEND 11
AND 22
OR 23
XOR 24
NOT 25
BYTE 26
;; constant values
LLARGE 16
LLARGEMO 15)

(defconstraint pivot () (if CT_MAX 0 (begin (if (- IS_BYTE 1) (if LOW_4 (if COUNTER (if BIT_B_4 (- PIVOT BYTE_3) (- PIVOT BYTE_4))) (if (+ (shift BIT_1 -1) (- 1 BIT_1)) (if BIT_B_4 (- PIVOT BYTE_3) (- PIVOT BYTE_4))))) (if (- IS_SIGNEXTEND 1) (if (- LOW_4 15) (if COUNTER (if BIT_B_4 (- PIVOT BYTE_4) (- PIVOT BYTE_3))) (if (+ (shift BIT_1 -1) (- 1 BIT_1)) (if BIT_B_4 (- PIVOT BYTE_4) (- PIVOT BYTE_3))))))))
(defpurefun (if-eq-else A B THEN ELSE)
(if-zero-else (- A B)
THEN
ELSE))

(defconstraint counter-constancies () (begin (if COUNTER 0 (- ARGUMENT_1_HI (shift ARGUMENT_1_HI -1))) (if COUNTER 0 (- ARGUMENT_1_LO (shift ARGUMENT_1_LO -1))) (if COUNTER 0 (- ARGUMENT_2_HI (shift ARGUMENT_2_HI -1))) (if COUNTER 0 (- ARGUMENT_2_LO (shift ARGUMENT_2_LO -1))) (if COUNTER 0 (- RESULT_HI (shift RESULT_HI -1))) (if COUNTER 0 (- RESULT_LO (shift RESULT_LO -1))) (if COUNTER 0 (- INST (shift INST -1))) (if COUNTER 0 (- CT_MAX (shift CT_MAX -1))) (if COUNTER 0 (- PIVOT (shift PIVOT -1))) (if COUNTER 0 (- BIT_B_4 (shift BIT_B_4 -1))) (if COUNTER 0 (- LOW_4 (shift LOW_4 -1))) (if COUNTER 0 (- NEG (shift NEG -1))) (if COUNTER 0 (- SMALL (shift SMALL -1)))))
;; 2.2 Shorthands
(defun (flag-sum)
(+ IS_AND IS_OR IS_XOR IS_NOT IS_BYTE IS_SIGNEXTEND))

(defconstraint bit_1 () (if CT_MAX 0 (begin (if (- IS_BYTE 1) (begin (if LOW_4 (- BIT_1 1) (if (- COUNTER 0) BIT_1 (if (- COUNTER LOW_4) (- BIT_1 (+ (shift BIT_1 -1) 1)) (- BIT_1 (shift BIT_1 -1))))))) (if (- IS_SIGNEXTEND 1) (begin (if (- 15 LOW_4) (- BIT_1 1) (if (- COUNTER 0) BIT_1 (if (- COUNTER (- 15 LOW_4)) (- BIT_1 (+ (shift BIT_1 -1) 1)) (- BIT_1 (shift BIT_1 -1))))))))))
(defun (weight-sum)
(+ (* IS_AND AND)
(* IS_OR OR)
(* IS_XOR XOR)
(* IS_NOT NOT)
(* IS_BYTE BYTE)
(* IS_SIGNEXTEND SIGNEXTEND)))

(defconstraint is-signextend-result () (if IS_SIGNEXTEND 0 (if CT_MAX (begin (- RESULT_HI ARGUMENT_2_HI) (- RESULT_LO ARGUMENT_2_LO)) (if SMALL (begin (- RESULT_HI ARGUMENT_2_HI) (- RESULT_LO ARGUMENT_2_LO)) (begin (if BIT_B_4 (begin (- BYTE_5 (* NEG 255)) (if BIT_1 (- BYTE_6 (* NEG 255)) (- BYTE_6 BYTE_4))) (begin (if BIT_1 (- BYTE_5 (* NEG 255)) (- BYTE_5 BYTE_3)) (- RESULT_LO ARGUMENT_2_LO))))))))
;; 2.3 Instruction decoding
(defconstraint no-bin-no-flag ()
(if-zero-else STAMP
(vanishes! (flag-sum))
(eq! (flag-sum) 1)))

(defconstraint small () (if (+ IS_BYTE IS_SIGNEXTEND) 0 (if (- COUNTER 15) (if ARGUMENT_1_HI (if (- ARGUMENT_1_LO (+ (* 16 (shift BITS -4)) (* 8 (shift BITS -3)) (* 4 (shift BITS -2)) (* 2 (shift BITS -1)) BITS)) (- SMALL 1) SMALL)))))
(defconstraint inst-to-flag ()
(eq! INST (weight-sum)))

(defconstraint inst-to-flag () (- INST (+ (* IS_AND 22) (* IS_OR 23) (* IS_XOR 24) (* IS_NOT 25) (* IS_BYTE 26) (* IS_SIGNEXTEND 11))))
;; 2.4 Heartbeat
(defconstraint first-row (:domain {0})
(vanishes! STAMP))

(defconstraint target-constraints () (if (- COUNTER CT_MAX) (begin (- ACC_1 ARGUMENT_1_HI) (- ACC_2 ARGUMENT_1_LO) (- ACC_3 ARGUMENT_2_HI) (- ACC_4 ARGUMENT_2_LO) (- ACC_5 RESULT_HI) (- ACC_6 RESULT_LO))))
(defconstraint stamp-increments ()
(vanishes! (* (will-inc! STAMP 0) (will-inc! STAMP 1))))

(defconstraint countereset () (if STAMP 0 (if (- COUNTER CT_MAX) (- (shift STAMP 1) (+ STAMP 1)) (- (shift COUNTER 1) (+ COUNTER 1)))))
(defconstraint new-stamp-reset-ct ()
(if-not-zero (- (next STAMP) STAMP)
(vanishes! (next CT))))

(defconstraint stamp-increments () (* (- (shift STAMP 1) (+ STAMP 0)) (- (shift STAMP 1) (+ STAMP 1))))
(defconstraint isnot-ctmax ()
(if-eq IS_NOT 1 (eq! CT_MAX LLARGEMO)))

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

(defconstraint no-bin-no-flag () (if STAMP (+ IS_AND IS_OR IS_XOR IS_NOT IS_BYTE IS_SIGNEXTEND) (- (+ IS_AND IS_OR IS_XOR IS_NOT IS_BYTE IS_SIGNEXTEND) 1)))
(defconstraint ct-small ()
(eq! 1
(~ (- CT LLARGE))))

(defconstraint is-byte-result () (if IS_BYTE 0 (if CT_MAX (begin RESULT_HI RESULT_LO) (begin RESULT_HI (- RESULT_LO (* SMALL PIVOT))))))
(defconstraint countereset (:guard STAMP)
(if-eq-else CT CT_MAX (will-inc! STAMP 1) (will-inc! CT 1)))

(defconstraint result-via-deflookup () (if (+ IS_AND IS_OR IS_XOR IS_NOT) 0 (begin (- BYTE_5 XXX_BYTE_HI) (- BYTE_6 XXX_BYTE_LO))))
(defconstraint last-row (:domain {-1})
(eq! CT CT_MAX))

(defconstraint isnot-ctmax () (if (- IS_NOT 1) (- CT_MAX 15)))
(defconstraint counter-constancies ()
(begin (counter-constancy CT ARG_1_HI)
(counter-constancy CT ARG_1_LO)
(counter-constancy CT ARG_2_HI)
(counter-constancy CT ARG_2_LO)
(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 SMALL)))

(defconstraint ct-small () (- 1 (~ (- COUNTER 16))))
;; 2.6 byte decompositions
(defconstraint byte_decompositions ()
(begin (byte-decomposition CT ACC_1 BYTE_1)
(byte-decomposition CT ACC_2 BYTE_2)
(byte-decomposition CT ACC_3 BYTE_3)
(byte-decomposition CT ACC_4 BYTE_4)
(byte-decomposition CT ACC_5 BYTE_5)
(byte-decomposition CT ACC_6 BYTE_6)))

(defconstraint new-stamp-reset-ct () (if (- (shift STAMP 1) STAMP) 0 (shift COUNTER 1)))
;; 2.7 target constraints
(defconstraint target-constraints ()
(if-eq CT CT_MAX
(begin (eq! ACC_1 ARG_1_HI)
(eq! ACC_2 ARG_1_LO)
(eq! ACC_3 ARG_2_HI)
(eq! ACC_4 ARG_2_LO)
(eq! ACC_5 RES_HI)
(eq! ACC_6 RES_LO))))

(defconstraint last-row (:domain {-1}) (- COUNTER CT_MAX))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; 2.8 binary column constraints ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; 2.8.2 BITS and related columns
(defconstraint bits-and-related (:guard (+ IS_BYTE IS_SIGNEXTEND))
(if-eq CT LLARGEMO
(begin (eq! PIVOT
(+ (* 128 (shift BITS -15))
(* 64 (shift BITS -14))
(* 32 (shift BITS -13))
(* 16 (shift BITS -12))
(* 8 (shift BITS -11))
(* 4 (shift BITS -10))
(* 2 (shift BITS -9))
(shift BITS -8)))
(eq! BYTE_2
(+ (* 128 (shift BITS -7))
(* 64 (shift BITS -6))
(* 32 (shift BITS -5))
(* 16 (shift BITS -4))
(* 8 (shift BITS -3))
(* 4 (shift BITS -2))
(* 2 (shift BITS -1))
BITS))
(eq! LOW_4
(+ (* 8 (shift BITS -3))
(* 4 (shift BITS -2))
(* 2 (shift BITS -1))
BITS))
(eq! BIT_B_4 (shift BITS -4))
(eq! NEG (shift BITS -15)))))

(defconstraint first-row (:domain {0}) STAMP)
;; 2.8.3 [[1]] constraints
;; (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 (:guard (+ IS_BYTE IS_SIGNEXTEND))
(if-eq CT LLARGEMO
(if-zero ARG_1_HI
(if-eq-else ARG_1_LO (+ (* 16 (shift BITS -4))
(* 8 (shift BITS -3))
(* 4 (shift BITS -2))
(* 2 (shift BITS -1))
BITS)
(eq! SMALL 1)
(vanishes! SMALL)))))

;; 2.9 pivot constraints
(defconstraint pivot (:guard CT_MAX)
(begin (if-eq IS_BYTE 1
(if-zero-else LOW_4
(if-zero CT
(if-zero-else BIT_B_4
(eq! PIVOT BYTE_3)
(eq! PIVOT BYTE_4)))
(if-zero (+ (prev BIT_1) (- 1 BIT_1))
(if-zero-else 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-else BIT_B_4
(eq! PIVOT BYTE_4)
(eq! PIVOT BYTE_3)))
(if-zero (+ (prev BIT_1) (- 1 BIT_1))
(if-zero-else BIT_B_4
(eq! PIVOT BYTE_4)
(eq! PIVOT BYTE_3)))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; 2.10 result constraints ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defconstraint is-byte-result (:guard IS_BYTE)
(if-zero-else 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-zero-else CT_MAX
(begin (eq! RES_HI ARG_2_HI)
(eq! RES_LO ARG_2_LO))
(if-zero-else SMALL
;; SMALL == 0
(begin (eq! RES_HI ARG_2_HI)
(eq! RES_LO ARG_2_LO))
;; SMALL == 1
(begin (if-zero-else BIT_B_4
;; b4 == 0
(begin (eq! BYTE_5 (* NEG 255))
(if-zero-else BIT_1
;; [[1]] == 0
(eq! BYTE_6 (* NEG 255))
;; [[1]] == 1
(eq! BYTE_6 BYTE_4)))
;; b4 == 1
(begin (if-zero-else 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)
(eq! BYTE_6 XXX_BYTE_LO)))
Loading

0 comments on commit 404a7eb

Please sign in to comment.