Consensys / corset

4 stars 10 forks source link

Bug in translation of `if` ? #87

Closed DavePearce closed 1 month ago

DavePearce commented 1 month ago

The following constraints appear to be mis-translated:

(module test)
(defcolumns (A :binary@loob) B)
(defconstraint test () (eq! (if A B) 10))

I'm expecting this to mean: if A = 0 then B = 10 However, it appears to translate as follows:

(1 - NORM(A)) * (B)

This does not appear to be correct? I suppose I would have expected this translation:

(1 - NORM(A)) * (B-10)
DavePearce commented 1 month ago

@powerslider We will have to think carefully about what the correct translation is here.

DavePearce commented 1 month ago

Some more tests:

DavePearce commented 1 month ago

So, this section of code from transformer/ifs.rs within function raise_ifs appears to be at fault:

let new_then = func
                                .call(
                                    &args
                                        .iter()
                                        .take(i)
                                        .chain(std::iter::once(&args_if[1]))
                                        .cloned()
                                        .collect::<Vec<_>>(),
                                )
                                .unwrap();

Specifically, it takes the first i elements then adds args_if[1] but fails to add the remainder of args.

DavePearce commented 1 month ago

Here's a fixed version which avoids complex iterator chaining as above:

let mut then_args = args.clone();
then_args[i] = args_if[1].clone();
let new_then = func.call(&then_args).unwrap();

Much simpler!

DavePearce commented 1 month ago

On the else branch we have this:

if let Some(arg_else) = args_if.get(2).cloned() {
                                new_args.push(
                                    func.call(
                                        &args
                                            .iter()
                                            .take(i)
                                            .cloned()
                                            .chain(std::iter::once(arg_else))
                                            .filter(|e| !matches!(e.e(), Expression::Void))
                                            .collect::<Vec<_>>(),
                                    )
                                    .unwrap(),
                                )
                            }

I'm confused what the filter is doing. Basically removing anything which is Void ... how would that arise ?

DavePearce commented 1 month ago

Here's a reasonable selection of tests:

;; Right
(defconstraint test1 () (+ (if-zero A B) 10))
(defconstraint test2 () (+ (if-zero A B C) 10))
;; Left
(defconstraint test3 () (+ 10 (if-zero A B)))
(defconstraint test4 () (+ 10 (if-zero A B C)))
;; Middle
(defconstraint test5 () (+ 10 (if-zero A B) 123))
(defconstraint test6 () (+ 10 (if-zero A B C) 123))
;; Double Right
(defconstraint test7 () (+ (if-zero A B) (if-zero C D) 10))
(defconstraint test8 () (+ (if-zero A B C) (if-zero C D) 10))
;; Double Left
(defconstraint test9 () (+ 10 (if-zero A B) (if-zero C D)))
(defconstraint test10 () (+ 10 (if-zero A B C) (if-zero C D)))
;; Double Middle
(defconstraint test11 () (+ 10 (if-zero A B) (if-zero C D) 10))
(defconstraint test12 () (+ 10 (if-zero A B C) (if-zero C D) 10))