Skip to content

Loop invariants #43

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
raghav198 merged 13 commits into from
Jun 24, 2026
Merged

Loop invariants #43

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
3734a72
Single loop invariant inference done
Jun 20, 2026
f55a423
Loop invariants now mostly strengthening to prove postcondition, thin…
Jun 23, 2026
470c9cc
Added circom examples
Jun 23, 2026
e0afe3e
New verification results with proper alignment
Jun 23, 2026
d4e76b5
Proper while->for conversion
Jun 23, 2026
b47393b
Fixing some errors as they come up
Jun 23, 2026
f883675
Latest results
Jun 23, 2026
b7eeeef
Added demo script
Jun 23, 2026
a3e1680
Latest results
Jun 23, 2026
138e6eb
Nested loop support and symbolic store added to WP
Jun 24, 2026
3eb895a
Added back missing slice invariant strengthening
Jun 24, 2026
889cafd
New results, added {signal} attribute to mux_ep
Jun 24, 2026
5321cb7
Removed unused StrongestPostcondition
Jun 24, 2026
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
711 changes: 711 additions & 0 deletions examples/circom-demo/AveragePooling2D_stride_test.llzk
View file
Open in desktop

Large diffs are not rendered by default.

711 changes: 711 additions & 0 deletions examples/circom-demo/AveragePooling2D_test.llzk
View file
Open in desktop

Large diffs are not rendered by default.

125 changes: 125 additions & 0 deletions examples/circom-demo/BatchNormalization_test.llzk
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,125 @@
module attributes {llzk.lang, llzk.main = !struct.type<@BatchNormalization2D_0::@BatchNormalization2D_0<[]>>} {
poly.template @BatchNormalization2D_0 {
struct.def @BatchNormalization2D_0 {
struct.member @out : !array.type<5,5,3 x !felt.type<"babybear">> {llzk.pub}
function.def @product(%arg0: !array.type<5,5,3 x !felt.type<"babybear">>, %arg1: !array.type<3 x !felt.type<"babybear">>, %arg2: !array.type<3 x !felt.type<"babybear">>) -> !struct.type<@BatchNormalization2D_0::@BatchNormalization2D_0<[]>> attributes {function.allow_constraint, function.allow_non_native_field_ops, function.allow_witness, llzk.derived} {
%c3 = arith.constant 3 : index
%c1 = arith.constant 1 : index
%c5 = arith.constant 5 : index
%c0 = arith.constant 0 : index
%self = struct.new : <@BatchNormalization2D_0::@BatchNormalization2D_0<[]>> {product_source = "compute"}
%nondet = llzk.nondet : !array.type<5,5,3 x !felt.type<"babybear">> {product_source = "compute"}
%0 = struct.readm %self[@out] : <@BatchNormalization2D_0::@BatchNormalization2D_0<[]>>, !array.type<5,5,3 x !felt.type<"babybear">> {product_source = "constrain"}
scf.for %arg3 = %c0 to %c5 step %c1 {
%1 = cast.tofelt %arg3 : index, !felt.type<"babybear"> {product_source = "compute"}
%2 = cast.tofelt %arg3 : index, !felt.type<"babybear"> {product_source = "constrain"}
scf.for %arg4 = %c0 to %c5 step %c1 {
%3 = cast.tofelt %arg4 : index, !felt.type<"babybear"> {product_source = "compute"}
%4 = cast.tofelt %arg4 : index, !felt.type<"babybear"> {product_source = "constrain"}
scf.for %arg5 = %c0 to %c3 step %c1 {
%5 = cast.tofelt %arg5 : index, !felt.type<"babybear"> {product_source = "compute"}
%6 = cast.toindex %5 : !felt.type<"babybear"> {product_source = "compute"}
%7 = array.read %arg1[%6] : <3 x !felt.type<"babybear">>, !felt.type<"babybear"> {product_source = "compute"}
%8 = cast.toindex %1 : !felt.type<"babybear"> {product_source = "compute"}
%9 = cast.toindex %3 : !felt.type<"babybear"> {product_source = "compute"}
%10 = cast.toindex %5 : !felt.type<"babybear"> {product_source = "compute"}
%11 = array.read %arg0[%8, %9, %10] : <5,5,3 x !felt.type<"babybear">>, !felt.type<"babybear"> {product_source = "compute"}
%12 = felt.mul %7, %11 : !felt.type<"babybear">, !felt.type<"babybear"> {product_source = "compute"}
%13 = cast.toindex %5 : !felt.type<"babybear"> {product_source = "compute"}
%14 = array.read %arg2[%13] : <3 x !felt.type<"babybear">>, !felt.type<"babybear"> {product_source = "compute"}
%15 = felt.add %12, %14 : !felt.type<"babybear">, !felt.type<"babybear"> {product_source = "compute"}
%16 = cast.toindex %1 : !felt.type<"babybear"> {product_source = "compute"}
%17 = cast.toindex %3 : !felt.type<"babybear"> {product_source = "compute"}
%18 = cast.toindex %5 : !felt.type<"babybear"> {product_source = "compute"}
array.write %nondet[%16, %17, %18] = %15 : <5,5,3 x !felt.type<"babybear">>, !felt.type<"babybear"> {product_source = "compute"}
%19 = cast.tofelt %arg5 : index, !felt.type<"babybear"> {product_source = "constrain"}
%20 = cast.toindex %19 : !felt.type<"babybear"> {product_source = "constrain"}
%21 = array.read %arg1[%20] : <3 x !felt.type<"babybear">>, !felt.type<"babybear"> {product_source = "constrain"}
%22 = cast.toindex %2 : !felt.type<"babybear"> {product_source = "constrain"}
%23 = cast.toindex %4 : !felt.type<"babybear"> {product_source = "constrain"}
%24 = cast.toindex %19 : !felt.type<"babybear"> {product_source = "constrain"}
%25 = array.read %arg0[%22, %23, %24] : <5,5,3 x !felt.type<"babybear">>, !felt.type<"babybear"> {product_source = "constrain"}
%26 = felt.mul %21, %25 : !felt.type<"babybear">, !felt.type<"babybear"> {product_source = "constrain"}
%27 = cast.toindex %19 : !felt.type<"babybear"> {product_source = "constrain"}
%28 = array.read %arg2[%27] : <3 x !felt.type<"babybear">>, !felt.type<"babybear"> {product_source = "constrain"}
%29 = felt.add %26, %28 : !felt.type<"babybear">, !felt.type<"babybear"> {product_source = "constrain"}
%30 = cast.toindex %2 : !felt.type<"babybear"> {product_source = "constrain"}
%31 = cast.toindex %4 : !felt.type<"babybear"> {product_source = "constrain"}
%32 = cast.toindex %19 : !felt.type<"babybear"> {product_source = "constrain"}
%33 = array.read %0[%30, %31, %32] : <5,5,3 x !felt.type<"babybear">>, !felt.type<"babybear"> {product_source = "constrain"}
constrain.eq %33, %29 : !felt.type<"babybear">, !felt.type<"babybear"> {product_source = "constrain"}
} {product_source = "fused"}
} {product_source = "fused"}
} {product_source = "fused"}
struct.writem %self[@out] = %nondet : <@BatchNormalization2D_0::@BatchNormalization2D_0<[]>>, !array.type<5,5,3 x !felt.type<"babybear">> {product_source = "compute"}
function.return %self : !struct.type<@BatchNormalization2D_0::@BatchNormalization2D_0<[]>>
}
function.def @compute(%arg0: !array.type<5,5,3 x !felt.type<"babybear">>, %arg1: !array.type<3 x !felt.type<"babybear">>, %arg2: !array.type<3 x !felt.type<"babybear">>) -> !struct.type<@BatchNormalization2D_0::@BatchNormalization2D_0<[]>> attributes {function.allow_non_native_field_ops, function.allow_witness, product_source = "compute"} {
%c3 = arith.constant 3 : index
%c1 = arith.constant 1 : index
%c5 = arith.constant 5 : index
%c0 = arith.constant 0 : index
%self = struct.new : <@BatchNormalization2D_0::@BatchNormalization2D_0<[]>> {product_source = "compute"}
%nondet = llzk.nondet : !array.type<5,5,3 x !felt.type<"babybear">> {product_source = "compute"}
scf.for %arg3 = %c0 to %c5 step %c1 {
%0 = cast.tofelt %arg3 : index, !felt.type<"babybear"> {product_source = "compute"}
scf.for %arg4 = %c0 to %c5 step %c1 {
%1 = cast.tofelt %arg4 : index, !felt.type<"babybear"> {product_source = "compute"}
scf.for %arg5 = %c0 to %c3 step %c1 {
%2 = cast.tofelt %arg5 : index, !felt.type<"babybear"> {product_source = "compute"}
%3 = cast.toindex %2 : !felt.type<"babybear"> {product_source = "compute"}
%4 = array.read %arg1[%3] : <3 x !felt.type<"babybear">>, !felt.type<"babybear"> {product_source = "compute"}
%5 = cast.toindex %0 : !felt.type<"babybear"> {product_source = "compute"}
%6 = cast.toindex %1 : !felt.type<"babybear"> {product_source = "compute"}
%7 = cast.toindex %2 : !felt.type<"babybear"> {product_source = "compute"}
%8 = array.read %arg0[%5, %6, %7] : <5,5,3 x !felt.type<"babybear">>, !felt.type<"babybear"> {product_source = "compute"}
%9 = felt.mul %4, %8 : !felt.type<"babybear">, !felt.type<"babybear"> {product_source = "compute"}
%10 = cast.toindex %2 : !felt.type<"babybear"> {product_source = "compute"}
%11 = array.read %arg2[%10] : <3 x !felt.type<"babybear">>, !felt.type<"babybear"> {product_source = "compute"}
%12 = felt.add %9, %11 : !felt.type<"babybear">, !felt.type<"babybear"> {product_source = "compute"}
%13 = cast.toindex %0 : !felt.type<"babybear"> {product_source = "compute"}
%14 = cast.toindex %1 : !felt.type<"babybear"> {product_source = "compute"}
%15 = cast.toindex %2 : !felt.type<"babybear"> {product_source = "compute"}
array.write %nondet[%13, %14, %15] = %12 : <5,5,3 x !felt.type<"babybear">>, !felt.type<"babybear"> {product_source = "compute"}
} {product_source = "compute"}
} {product_source = "compute"}
} {product_source = "compute"}
struct.writem %self[@out] = %nondet : <@BatchNormalization2D_0::@BatchNormalization2D_0<[]>>, !array.type<5,5,3 x !felt.type<"babybear">> {product_source = "compute"}
function.return {product_source = "compute"} %self : !struct.type<@BatchNormalization2D_0::@BatchNormalization2D_0<[]>>
}
function.def @constrain(%arg0: !struct.type<@BatchNormalization2D_0::@BatchNormalization2D_0<[]>>, %arg1: !array.type<5,5,3 x !felt.type<"babybear">>, %arg2: !array.type<3 x !felt.type<"babybear">>, %arg3: !array.type<3 x !felt.type<"babybear">>) attributes {function.allow_constraint, function.allow_non_native_field_ops, product_source = "constrain"} {
%c3 = arith.constant 3 : index
%c1 = arith.constant 1 : index
%c5 = arith.constant 5 : index
%c0 = arith.constant 0 : index
%0 = struct.readm %arg0[@out] : <@BatchNormalization2D_0::@BatchNormalization2D_0<[]>>, !array.type<5,5,3 x !felt.type<"babybear">> {product_source = "constrain"}
scf.for %arg4 = %c0 to %c5 step %c1 {
%1 = cast.tofelt %arg4 : index, !felt.type<"babybear"> {product_source = "constrain"}
scf.for %arg5 = %c0 to %c5 step %c1 {
%2 = cast.tofelt %arg5 : index, !felt.type<"babybear"> {product_source = "constrain"}
scf.for %arg6 = %c0 to %c3 step %c1 {
%3 = cast.tofelt %arg6 : index, !felt.type<"babybear"> {product_source = "constrain"}
%4 = cast.toindex %3 : !felt.type<"babybear"> {product_source = "constrain"}
%5 = array.read %arg2[%4] : <3 x !felt.type<"babybear">>, !felt.type<"babybear"> {product_source = "constrain"}
%6 = cast.toindex %1 : !felt.type<"babybear"> {product_source = "constrain"}
%7 = cast.toindex %2 : !felt.type<"babybear"> {product_source = "constrain"}
%8 = cast.toindex %3 : !felt.type<"babybear"> {product_source = "constrain"}
%9 = array.read %arg1[%6, %7, %8] : <5,5,3 x !felt.type<"babybear">>, !felt.type<"babybear"> {product_source = "constrain"}
%10 = felt.mul %5, %9 : !felt.type<"babybear">, !felt.type<"babybear"> {product_source = "constrain"}
%11 = cast.toindex %3 : !felt.type<"babybear"> {product_source = "constrain"}
%12 = array.read %arg3[%11] : <3 x !felt.type<"babybear">>, !felt.type<"babybear"> {product_source = "constrain"}
%13 = felt.add %10, %12 : !felt.type<"babybear">, !felt.type<"babybear"> {product_source = "constrain"}
%14 = cast.toindex %1 : !felt.type<"babybear"> {product_source = "constrain"}
%15 = cast.toindex %2 : !felt.type<"babybear"> {product_source = "constrain"}
%16 = cast.toindex %3 : !felt.type<"babybear"> {product_source = "constrain"}
%17 = array.read %0[%14, %15, %16] : <5,5,3 x !felt.type<"babybear">>, !felt.type<"babybear"> {product_source = "constrain"}
constrain.eq %17, %13 : !felt.type<"babybear">, !felt.type<"babybear"> {product_source = "constrain"}
} {product_source = "constrain"}
} {product_source = "constrain"}
} {product_source = "constrain"}
function.return {product_source = "constrain"}
}
}
}
}

Loading
Loading