From 81d59f252a121ac8d4b6df265d0398c7849771a4 Mon Sep 17 00:00:00 2001 From: "Cyne Jarvis J. Zarceno" Date: Thu, 25 Jun 2026 21:53:16 +0800 Subject: [PATCH 1/6] test semantic preservation regressions --- .../PCLLowering/pcl_bool_downstream_use.llzk | 28 ++++++++++ .../stateful_ops_preservation.llzk | 51 +++++++++++++++++++ .../offset_read_preservation.llzk | 24 +++++++++ 3 files changed, 103 insertions(+) create mode 100644 test/Transforms/PCLLowering/pcl_bool_downstream_use.llzk create mode 100644 test/Transforms/RedundantOperation/stateful_ops_preservation.llzk create mode 100644 test/Transforms/RedundantReadWrite/offset_read_preservation.llzk 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..fbf5cfc484 --- /dev/null +++ b/test/Transforms/PCLLowering/pcl_bool_downstream_use.llzk @@ -0,0 +1,28 @@ +// 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 + constrain.eq %xor, %eq1 : i1, i1 + 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: %[[ASSERT_EQ:[0-9a-zA-Z_\.]+]] = pcl.eq %[[XOR]], %[[EQ1]] +// CHECK: pcl.assert %[[ASSERT_EQ]] 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 From e38bd9bd9db1ce76595603ca40eb28e029c89f24 Mon Sep 17 00:00:00 2001 From: "Cyne Jarvis J. Zarceno" Date: Thu, 25 Jun 2026 22:06:42 +0800 Subject: [PATCH 2/6] adjust pcl downstream proof --- test/Transforms/PCLLowering/pcl_bool_downstream_use.llzk | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/test/Transforms/PCLLowering/pcl_bool_downstream_use.llzk b/test/Transforms/PCLLowering/pcl_bool_downstream_use.llzk index fbf5cfc484..3985f7c9e6 100644 --- a/test/Transforms/PCLLowering/pcl_bool_downstream_use.llzk +++ b/test/Transforms/PCLLowering/pcl_bool_downstream_use.llzk @@ -13,7 +13,7 @@ module attributes {llzk.lang} { %eq1 = bool.cmp eq(%a, %b) : !F, !F %eq2 = bool.cmp eq(%b, %c) : !F, !F %xor = bool.xor %eq1, %eq2 - constrain.eq %xor, %eq1 : i1, i1 + %use = bool.and %xor, %eq1 function.return } } @@ -24,5 +24,4 @@ module attributes {llzk.lang} { // 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: %[[ASSERT_EQ:[0-9a-zA-Z_\.]+]] = pcl.eq %[[XOR]], %[[EQ1]] -// CHECK: pcl.assert %[[ASSERT_EQ]] +// CHECK: %[[USE:[0-9a-zA-Z_\.]+]] = pcl.and %[[XOR]], %[[EQ1]] From 00b073c7782c0a542e498c73e8d87cde4f089ec9 Mon Sep 17 00:00:00 2001 From: "Cyne Jarvis J. Zarceno" Date: Thu, 25 Jun 2026 22:31:36 +0800 Subject: [PATCH 3/6] test r1cs table offset preservation --- .../r1cs_table_offset_preservation.llzk | 26 +++++++++++++++++++ 1 file changed, 26 insertions(+) create mode 100644 test/Transforms/R1CSLowering/r1cs_table_offset_preservation.llzk 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..cf3bf53988 --- /dev/null +++ b/test/Transforms/R1CSLowering/r1cs_table_offset_preservation.llzk @@ -0,0 +1,26 @@ +// 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 @cell : !felt.type<"babybear"> {column, llzk.pub} + + 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<"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: %[[PREV:[0-9a-zA-Z_\.]+]] = r1cs.def 0 : !r1cs.signal {pub = #r1cs.pub} +// CHECK: %[[CURR:[0-9a-zA-Z_\.]+]] = r1cs.def 1 : !r1cs.signal {pub = #r1cs.pub} +// 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 From e19548912fc2f52d0f3e24b42d990ad10c0daf8e Mon Sep 17 00:00:00 2001 From: "Cyne Jarvis J. Zarceno" Date: Thu, 25 Jun 2026 22:31:36 +0800 Subject: [PATCH 4/6] test r1cs table offset preservation --- .../r1cs_table_offset_preservation.llzk | 28 +++++++++++++++++++ 1 file changed, 28 insertions(+) create mode 100644 test/Transforms/R1CSLowering/r1cs_table_offset_preservation.llzk 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..dd10e20693 --- /dev/null +++ b/test/Transforms/R1CSLowering/r1cs_table_offset_preservation.llzk @@ -0,0 +1,28 @@ +// 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() -> !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<"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: %[[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 From 4030199080496bc95d4c0b20234957e2be783d05 Mon Sep 17 00:00:00 2001 From: "Cyne Jarvis J. Zarceno" Date: Thu, 25 Jun 2026 22:56:30 +0800 Subject: [PATCH 5/6] test r1cs offset proof public output --- .../R1CSLowering/r1cs_table_offset_preservation.llzk | 3 +++ 1 file changed, 3 insertions(+) diff --git a/test/Transforms/R1CSLowering/r1cs_table_offset_preservation.llzk b/test/Transforms/R1CSLowering/r1cs_table_offset_preservation.llzk index dd10e20693..b2c9aebb3b 100644 --- a/test/Transforms/R1CSLowering/r1cs_table_offset_preservation.llzk +++ b/test/Transforms/R1CSLowering/r1cs_table_offset_preservation.llzk @@ -11,6 +11,9 @@ module attributes {llzk.lang, llzk.main = !struct.type<@Rows>} { } function.def @constrain(%self: !struct.type<@Rows>) { + %out = struct.readm %self[@out] : !struct.type<@Rows>, !felt.type<"babybear"> + %zero = felt.const 0 <"babybear"> + constrain.eq %out, %zero : !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"> From 8baa711c648219b0a540864e1774482ebd6a84b6 Mon Sep 17 00:00:00 2001 From: "Cyne Jarvis J. Zarceno" Date: Thu, 25 Jun 2026 23:11:17 +0800 Subject: [PATCH 6/6] test r1cs offset proof input --- .../r1cs_table_offset_preservation.llzk | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/test/Transforms/R1CSLowering/r1cs_table_offset_preservation.llzk b/test/Transforms/R1CSLowering/r1cs_table_offset_preservation.llzk index b2c9aebb3b..39ec6243e1 100644 --- a/test/Transforms/R1CSLowering/r1cs_table_offset_preservation.llzk +++ b/test/Transforms/R1CSLowering/r1cs_table_offset_preservation.llzk @@ -5,15 +5,17 @@ module attributes {llzk.lang, llzk.main = !struct.type<@Rows>} { struct.member @out : !felt.type<"babybear"> {llzk.pub} struct.member @cell : !felt.type<"babybear"> {column} - function.def @compute() -> !struct.type<@Rows> { + 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>) { + function.def @constrain( + %self: !struct.type<@Rows>, + %a: !felt.type<"babybear"> {llzk.pub} + ) { %out = struct.readm %self[@out] : !struct.type<@Rows>, !felt.type<"babybear"> - %zero = felt.const 0 <"babybear"> - constrain.eq %out, %zero : !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"> @@ -22,7 +24,8 @@ module attributes {llzk.lang, llzk.main = !struct.type<@Rows>} { } } -// CHECK-LABEL: r1cs.circuit @Rows inputs () { +// 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