From 65a1a9a1795fcb9ce31cbbeea9e4079dd9e67b83 Mon Sep 17 00:00:00 2001 From: DavePearce Date: Fri, 13 Dec 2024 13:27:27 +1300 Subject: [PATCH] Fixes for Quick Tests This puts through various minor fixes for the quick tests. What remains now is to update the larger tests. At this stage, performance may be starting to become an issue. --- pkg/corset/stdlib.lisp | 19 +++++++++++++++---- pkg/test/valid_corset_test.go | 20 ++++++++++---------- testdata/bit_decomposition.lisp | 2 +- testdata/byte_decomposition.lisp | 4 ++-- testdata/byte_sorting.lisp | 2 +- testdata/counter.lisp | 15 +-------------- testdata/type_invalid_05.lisp | 2 +- testdata/word_sorting.lisp | 4 ++-- 8 files changed, 33 insertions(+), 35 deletions(-) diff --git a/pkg/corset/stdlib.lisp b/pkg/corset/stdlib.lisp index 1d26ec07..d9966e69 100644 --- a/pkg/corset/stdlib.lisp +++ b/pkg/corset/stdlib.lisp @@ -1,12 +1,14 @@ (defpurefun ((vanishes! :@loob) x) x) +;; ============================================================================= +;; Logical +;; ============================================================================= (defpurefun ((or! :@loob) x y) (* x y)) (defpurefun ((eq! :@loob) x y) (- x y)) -(defpurefun (prev x) (shift x -1)) -(defpurefun (next x) (shift x 1)) - -;; +;; ============================================================================= +;; Control Flow +;; ============================================================================= (defpurefun (if-not-eq lhs rhs then) (if (eq! lhs rhs) @@ -28,3 +30,12 @@ then ;; False branch else)) + +;; ============================================================================= +;; Temporal +;; ============================================================================= +(defpurefun (prev x) (shift x -1)) +(defpurefun (next x) (shift x 1)) +(defpurefun (will-eq! e0 e1) (eq! (next e0) e1)) +(defpurefun (will-inc! e0 offset) (will-eq! e0 (+ e0 offset))) +(defpurefun (will-remain-constant! e0) (will-eq! e0 e0)) diff --git a/pkg/test/valid_corset_test.go b/pkg/test/valid_corset_test.go index efdfb446..c284acd5 100644 --- a/pkg/test/valid_corset_test.go +++ b/pkg/test/valid_corset_test.go @@ -625,23 +625,23 @@ func Test_PureFun_04(t *testing.T) { // =================================================================== func Test_Counter(t *testing.T) { - Check(t, false, "counter") + Check(t, true, "counter") } func Test_ByteDecomp(t *testing.T) { - Check(t, false, "byte_decomposition") + Check(t, true, "byte_decomposition") } func Test_BitDecomp(t *testing.T) { - Check(t, false, "bit_decomposition") + Check(t, true, "bit_decomposition") } func Test_ByteSorting(t *testing.T) { - Check(t, false, "byte_sorting") + Check(t, true, "byte_sorting") } func Test_WordSorting(t *testing.T) { - Check(t, false, "word_sorting") + Check(t, true, "word_sorting") } func Test_Memory(t *testing.T) { @@ -649,23 +649,23 @@ func Test_Memory(t *testing.T) { } func TestSlow_Add(t *testing.T) { - Check(t, false, "add") + Check(t, true, "add") } func TestSlow_BinStatic(t *testing.T) { - Check(t, false, "bin-static") + Check(t, true, "bin-static") } func TestSlow_BinDynamic(t *testing.T) { - Check(t, false, "bin-dynamic") + Check(t, true, "bin-dynamic") } func TestSlow_Wcp(t *testing.T) { - Check(t, false, "wcp") + Check(t, true, "wcp") } func TestSlow_Mxp(t *testing.T) { - Check(t, false, "mxp") + Check(t, true, "mxp") } // =================================================================== diff --git a/testdata/bit_decomposition.lisp b/testdata/bit_decomposition.lisp index f5a33ce5..4cfdb8bd 100644 --- a/testdata/bit_decomposition.lisp +++ b/testdata/bit_decomposition.lisp @@ -6,4 +6,4 @@ (BIT_3 :i1@prove)) ;; NIBBLE = 8*BIT_3 + 4*BIT_2 + 2*BIT_1 + BIT_0 -(defconstraint decomp () (- NIBBLE (+ BIT_0 (* 2 BIT_1) (* 4 BIT_2) (* 8 BIT_3)))) +(defconstraint decomp () (eq! NIBBLE (+ BIT_0 (* 2 BIT_1) (* 4 BIT_2) (* 8 BIT_3)))) diff --git a/testdata/byte_decomposition.lisp b/testdata/byte_decomposition.lisp index 12bc1785..84042838 100644 --- a/testdata/byte_decomposition.lisp +++ b/testdata/byte_decomposition.lisp @@ -35,9 +35,9 @@ ;; If CT[k] == 3 (if-eq-else CT 3 ;; Then, CT[k+1] == 0 - (shift CT 1) + (eq! (next CT) 0) ;; Else, CT[k]+1 == CT[k+1] - (- (+ 1 CT) (next CT)))) + (eq! (+ 1 CT) (next CT)))) ;; Argument accumulates byte values. (defconstraint accumulator (:guard ST) diff --git a/testdata/byte_sorting.lisp b/testdata/byte_sorting.lisp index 2e0624ea..1a114f20 100644 --- a/testdata/byte_sorting.lisp +++ b/testdata/byte_sorting.lisp @@ -8,4 +8,4 @@ (defcolumns (Delta :i8@prove)) ;; Delta == X - X[i-1] -(defconstraint sort () (- Delta (- X (shift X -1)))) +(defconstraint sort () (eq! Delta (- X (shift X -1)))) diff --git a/testdata/counter.lisp b/testdata/counter.lisp index 44c364f7..b52b0e07 100644 --- a/testdata/counter.lisp +++ b/testdata/counter.lisp @@ -1,16 +1,3 @@ -(defpurefun (vanishes! e0) e0) -;; -(defpurefun (next X) (shift X 1)) -(defpurefun (prev X) (shift X -1)) -;; -(defpurefun (eq! x y) (- x y)) -;; -(defpurefun (will-eq! e0 e1) (eq! (next e0) e1)) -(defpurefun (will-inc! e0 offset) (will-eq! e0 (+ e0 offset))) -(defpurefun (will-remain-constant! e0) (will-eq! e0 e0)) -;; -(defpurefun (if-eq-else x val then else) (if (eq! x val) then else)) - ;; =================================================== ;; Constraints ;; =================================================== @@ -18,7 +5,7 @@ ;; In the first row, STAMP is always zero. This allows for an ;; arbitrary amount of padding at the beginning which has no function. -(defconstraint first (:domain {0}) STAMP) +(defconstraint first (:domain {0}) (eq! STAMP 0)) ;; In the last row of a valid frame, the counter must have its max ;; value. This ensures that all non-padding frames are complete. diff --git a/testdata/type_invalid_05.lisp b/testdata/type_invalid_05.lisp index 4ee1f8d8..6b8e0f38 100644 --- a/testdata/type_invalid_05.lisp +++ b/testdata/type_invalid_05.lisp @@ -1,5 +1,5 @@ (defcolumns - (BIT :binary@loob) + (BIT :binary) (X :binary@loob)) (defconstraint c1 () (if (+ 2 BIT) X)) diff --git a/testdata/word_sorting.lisp b/testdata/word_sorting.lisp index 81ec278c..920f138f 100644 --- a/testdata/word_sorting.lisp +++ b/testdata/word_sorting.lisp @@ -9,7 +9,7 @@ (defcolumns (Byte_0 :i8@prove) (Byte_1 :i8@prove)) ;; Ensure Delta is a u16 -(defconstraint delta_type () (- Delta (+ (* 256 Byte_1) Byte_0))) +(defconstraint delta_type () (eq! Delta (+ (* 256 Byte_1) Byte_0))) ;; Delta == X - X[i-1] -(defconstraint sort () (- Delta (- X (shift X -1)))) +(defconstraint sort () (eq! Delta (- X (shift X -1))))