Improve conditional matrix mult with 3 opts (#116)

We received a benchmark from Lef which essentially checked the
following:

   (cond ? A*B : A*C)[i] == v

where A, B, C are 4 by 4 matrices, cond is a bool, i is an index, and v
a value.

The expected number of constraints is n^3: order 64 , but compile time
and constraint count were in the thousands.

I investigated finding a number of things:
* the Z# front-end entered a conditional branch for the ternary, causing
  the MM to happen in a conditional context
* while the MM has an oblivious access pattern, since `i` is variable,
  the oblivious pass wasn't really helping
* there were some weird non-constant indices floating around like
  (ite cond 0 0)

The three optimizations fix these problems:
* If the Z# frontend isn't in assertion isolation mode, don't enter a
  conditional branch for an ITE
* Constant folding: add the rewrite (ite cond a a) -> a
* Linear-scan array eliminator: for each operation, check if the index
  is constant. If so, skip the scan (for that access only)
This commit is contained in:
Alex Ozdemir
2022-10-27 13:02:44 -07:00
committed by GitHub
parent f1dbab65ab
commit a8f512aff3
5 changed files with 146 additions and 62 deletions

View File

@@ -0,0 +1,18 @@
def matmult(field[16] a, field[16] b) -> field[16]:
field[16] c = [0,0,0,0, 0,0,0,0, 0,0,0,0, 0,0,0,0]
for field i in 0..4 do
for field j in 0..4 do
field s = 0
for field k in 0..4 do
s = s + a[i*4 + k] * b[k*4 + j]
endfor
c[i*4 +j] = s
endfor
endfor
return c
def main(public field[16] a, public field[16] b, public field[2] ab, public field init, public field final, private field doc) -> bool:
field[16] s = [1,0,0,0, 0,1,0,0, 0,0,1,0, 0,0,0,1]
s = if (doc == 0) then matmult(s, a) else matmult(s, b) fi
return if s[init*4 + final] == 1 then true else false fi