search

quantstamp / halo2-analyzer

SMT 2023 Submission; license pending
52 stars 10 forks source link

Update rotations #4

Closed jgorzny closed 1 year ago

jgorzny commented 1 year ago

Hopefully it is this simple, but I could be wrong :)

Does not account for over/underflows (if those are possible in rust); good enough for now, I think.

May not want to merge until other changes regarding integration with CVC5 are done. It would also change the variable names there, but I don't anticipate that being complicated work

FatemehHeidari commented 1 year ago

The indices are not calculated correctly. as an example this kind of cases can become a problem: let n = format!("I-{}", (*column_index as i32) + rotation.0); This will generate the same variable for, for example, column_index = 1 and rotation = 10 with the case column_index = 10 and rotation = 1 . We will have I-11 for both.