Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
27 changes: 27 additions & 0 deletions test/Transforms/PCLLowering/pcl_bool_downstream_use.llzk
Original file line number Diff line number Diff line change
@@ -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]]
34 changes: 34 additions & 0 deletions test/Transforms/R1CSLowering/r1cs_table_offset_preservation.llzk
Original file line number Diff line number Diff line change
@@ -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
51 changes: 51 additions & 0 deletions test/Transforms/RedundantOperation/stateful_ops_preservation.llzk
Original file line number Diff line number Diff line change
@@ -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]]
24 changes: 24 additions & 0 deletions test/Transforms/RedundantReadWrite/offset_read_preservation.llzk
Original file line number Diff line number Diff line change
@@ -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
Loading