diff --git a/test/Transforms/PCLLowering/pcl_bool_downstream_use.llzk b/test/Transforms/PCLLowering/pcl_bool_downstream_use.llzk new file mode 100644 index 0000000000..3985f7c9e6 --- /dev/null +++ b/test/Transforms/PCLLowering/pcl_bool_downstream_use.llzk @@ -0,0 +1,27 @@ +// REQUIRES: with-pcl +// RUN: llzk-opt -llzk-to-pcl -verify-diagnostics %s | FileCheck --enable-var-scope %s + +!F = !felt.type<"goldilocks"> +module attributes {llzk.lang} { + struct.def @A { + function.def @compute(%a: !F, %b: !F, %c: !F) -> !struct.type<@A> attributes {function.allow_witness} { + %self = struct.new : <@A> + function.return %self : !struct.type<@A> + } + + function.def @constrain(%self: !struct.type<@A>, %a: !F, %b: !F, %c: !F) attributes {function.allow_constraint, function.allow_non_native_field_ops} { + %eq1 = bool.cmp eq(%a, %b) : !F, !F + %eq2 = bool.cmp eq(%b, %c) : !F, !F + %xor = bool.xor %eq1, %eq2 + %use = bool.and %xor, %eq1 + function.return + } + } +} + +// CHECK-LABEL: func.func @A( +// CHECK: %[[EQ1:[0-9a-zA-Z_\.]+]] = pcl.eq %arg0, %arg1 +// CHECK: %[[EQ2:[0-9a-zA-Z_\.]+]] = pcl.eq %arg1, %arg2 +// CHECK: %[[IFF:[0-9a-zA-Z_\.]+]] = pcl.iff %[[EQ1]], %[[EQ2]] +// CHECK: %[[XOR:[0-9a-zA-Z_\.]+]] = pcl.not %[[IFF]] +// CHECK: %[[USE:[0-9a-zA-Z_\.]+]] = pcl.and %[[XOR]], %[[EQ1]] diff --git a/test/Transforms/R1CSLowering/r1cs_table_offset_preservation.llzk b/test/Transforms/R1CSLowering/r1cs_table_offset_preservation.llzk new file mode 100644 index 0000000000..39ec6243e1 --- /dev/null +++ b/test/Transforms/R1CSLowering/r1cs_table_offset_preservation.llzk @@ -0,0 +1,34 @@ +// RUN: llzk-opt -llzk-full-r1cs-lowering -verify-diagnostics %s | r1cs-opt --verify-diagnostics - | FileCheck --enable-var-scope %s + +module attributes {llzk.lang, llzk.main = !struct.type<@Rows>} { + struct.def @Rows { + struct.member @out : !felt.type<"babybear"> {llzk.pub} + struct.member @cell : !felt.type<"babybear"> {column} + + function.def @compute(%a: !felt.type<"babybear">) -> !struct.type<@Rows> { + %self = struct.new : !struct.type<@Rows> + function.return %self : !struct.type<@Rows> + } + + function.def @constrain( + %self: !struct.type<@Rows>, + %a: !felt.type<"babybear"> {llzk.pub} + ) { + %out = struct.readm %self[@out] : !struct.type<@Rows>, !felt.type<"babybear"> + constrain.eq %out, %a : !felt.type<"babybear"> + %prev = struct.readm %self[@cell] : !struct.type<@Rows>, !felt.type<"babybear"> {tableOffset = -1 : index} + %curr = struct.readm %self[@cell] : !struct.type<@Rows>, !felt.type<"babybear"> {tableOffset = 0 : index} + constrain.eq %prev, %curr : !felt.type<"babybear"> + function.return + } + } +} + +// CHECK-LABEL: r1cs.circuit @Rows inputs ( +// CHECK-SAME: %[[A:[0-9a-zA-Z_\.]+]]: !r1cs.signal {#r1cs.pub} +// CHECK: %[[OUT:[0-9a-zA-Z_\.]+]] = r1cs.def 0 : !r1cs.signal {pub = #r1cs.pub} +// CHECK: %[[PREV:[0-9a-zA-Z_\.]+]] = r1cs.def 1 : !r1cs.signal +// CHECK: %[[CURR:[0-9a-zA-Z_\.]+]] = r1cs.def 2 : !r1cs.signal +// CHECK: %[[PREV_LIN:[0-9a-zA-Z_\.]+]] = r1cs.to_linear %[[PREV]] : !r1cs.signal to !r1cs.linear +// CHECK: %[[CURR_LIN:[0-9a-zA-Z_\.]+]] = r1cs.to_linear %[[CURR]] : !r1cs.signal to !r1cs.linear +// CHECK: r1cs.constrain diff --git a/test/Transforms/RedundantOperation/stateful_ops_preservation.llzk b/test/Transforms/RedundantOperation/stateful_ops_preservation.llzk new file mode 100644 index 0000000000..1d024e4213 --- /dev/null +++ b/test/Transforms/RedundantOperation/stateful_ops_preservation.llzk @@ -0,0 +1,51 @@ +// RUN: llzk-opt -split-input-file --llzk-duplicate-op-elim %s | FileCheck --enable-var-scope %s + +module attributes {llzk.lang} { + global.def @g : !felt.type = 1 + + struct.def @GlobalState { + struct.member @out : !felt.type {llzk.pub} + + function.def @compute() -> !struct.type<@GlobalState> { + %self = struct.new : !struct.type<@GlobalState> + %two = felt.const 2 + %before = global.read @g : !felt.type + global.write @g = %two : !felt.type + %after = global.read @g : !felt.type + struct.writem %self[@out] = %after : !struct.type<@GlobalState>, !felt.type + function.return %self : !struct.type<@GlobalState> + } + + function.def @constrain(%self: !struct.type<@GlobalState>) { + function.return + } + } +} + +// CHECK-LABEL: function.def @compute() +// CHECK: %[[BEFORE:[0-9a-zA-Z_\.]+]] = global.read @g : !felt.type +// CHECK: global.write @g +// CHECK: %[[AFTER:[0-9a-zA-Z_\.]+]] = global.read @g : !felt.type +// CHECK: struct.writem {{.*}}\[@out\] = %[[AFTER]] + +// ----- + +module attributes {llzk.lang} { + function.def @ram_state() -> !felt.type attributes {function.allow_witness} { + %addr = arith.constant 0 : index + %one = felt.const 1 + %two = felt.const 2 + ram.store %addr, %one : !felt.type + %before = ram.load %addr : !felt.type + ram.store %addr, %two : !felt.type + %after = ram.load %addr : !felt.type + function.return %after : !felt.type + } +} + +// CHECK-LABEL: function.def @ram_state() +// CHECK: ram.store +// CHECK: %[[BEFORE:[0-9a-zA-Z_\.]+]] = ram.load +// CHECK: ram.store +// CHECK: %[[AFTER:[0-9a-zA-Z_\.]+]] = ram.load +// CHECK: function.return %[[AFTER]] diff --git a/test/Transforms/RedundantReadWrite/offset_read_preservation.llzk b/test/Transforms/RedundantReadWrite/offset_read_preservation.llzk new file mode 100644 index 0000000000..e9b88e00a8 --- /dev/null +++ b/test/Transforms/RedundantReadWrite/offset_read_preservation.llzk @@ -0,0 +1,24 @@ +// RUN: llzk-opt --llzk-duplicate-read-write-elim %s | FileCheck --enable-var-scope %s + +module attributes {llzk.lang} { + struct.def @Rows { + struct.member @cell : !felt.type {column} + + function.def @compute() -> !struct.type<@Rows> { + %self = struct.new : !struct.type<@Rows> + function.return %self : !struct.type<@Rows> + } + + function.def @constrain(%self: !struct.type<@Rows>) { + %prev = struct.readm %self[@cell] : !struct.type<@Rows>, !felt.type {tableOffset = -1 : index} + %curr = struct.readm %self[@cell] : !struct.type<@Rows>, !felt.type {tableOffset = 0 : index} + constrain.eq %prev, %curr : !felt.type, !felt.type + function.return + } + } +} + +// CHECK-LABEL: function.def @constrain( +// CHECK: %[[PREV:[0-9a-zA-Z_\.]+]] = struct.readm {{.*}}\[@cell\] : {{.*}} {tableOffset = -1 : index} +// CHECK: %[[CURR:[0-9a-zA-Z_\.]+]] = struct.readm {{.*}}\[@cell\] : {{.*}} {tableOffset = 0 : index} +// CHECK: constrain.eq %[[PREV]], %[[CURR]] : !felt.type, !felt.type