search

hacspec / hax

A Rust verification tool
https://hacspec.org/blog
Apache License 2.0
179 stars 19 forks source link

Extraction of Halo2 in specs is broken for Coq #158

Open W95Psp opened 1 year ago

cmester0 commented 1 year ago

Should be fixed for coq by #160.

W95Psp commented 9 months ago

Just checked on main, this is still broken, I get the following errors:

error[HAX0001]: (Coq backend) something is not implemented yet.
                [expr] node app global vcar projector tuple
    --> halo2/src/halo2.rs:5509:19
     |
5509 |         let p_x = point.0;
     |                   ^^^^^^^

error[HAX0001]: (Coq backend) something is not implemented yet.
                [expr] node app global vcar projector tuple
    --> halo2/src/halo2.rs:5485:26
     |
5485 |         let y: FpVesta = points[i].1;
     |                          ^^^^^^^^^^^

error[HAX0001]: (Coq backend) something is not implemented yet.
                [expr] node app global vcar projector tuple
    --> halo2/src/halo2.rs:5484:26
     |
5484 |         let x: FpVesta = points[i].0;
     |                          ^^^^^^^^^^^