github/Picus
1
1
Fork 0
mirror of https://github.com/Veridise/Picus.git synced 2026-04-19 03:00:11 -04:00
Code Issues Packages Projects Releases Wiki Activity

Delete r1cs-z3-AB0-optimizer.rkt

Browse Source
This commit is contained in:
Yanju Chen
2023-08-16 17:21:13 -07:00
parent 44ea29ab89
commit a08dceb4cb
1 changed files with 0 additions and 56 deletions
Download Patch File Download Diff File Expand all files Collapse all files

56
picus/optimizers/r1cs-z3-AB0-optimizer.rkt
View File

@@ -1,56 +0,0 @@
#lang racket
; (note) this is applied in optimization phase 0
; this implements the following lemma
; A * B = 0 => A = 0 or B = 0
(require
(prefix-in tokamak: "../tokamak.rkt")
(prefix-in utils: "../utils.rkt")
(prefix-in config: "../config.rkt")
(prefix-in r1cs: "../r1cs/r1cs-grammar.rkt")
)
(provide (rename-out
[optimize-r1cs optimize-r1cs]
))
(define (optimize-r1cs arg-r1cs)
(match arg-r1cs
; command level
[(r1cs:rcmds vs) (r1cs:rcmds (for/list ([v vs]) (optimize-r1cs v)))]
[(r1cs:rassert v) (r1cs:rassert (optimize-r1cs v))]
; (note) yes, this is the specific shape in standard form about A*B=0
[(r1cs:req
(r1cs:rmod (r1cs:rmul (list vs ...)) _)
(r1cs:rmod (r1cs:radd (list (r1cs:rint 0))) _)
)
; rewrite
(r1cs:ror
(for/list ([v vs])
(r1cs:req
(r1cs:rint 0)
(r1cs:rmod v (r1cs:rint config:p))
)
)
)
]
[(r1cs:req
(r1cs:rmod (r1cs:radd (list (r1cs:rint 0))) _)
(r1cs:rmod (r1cs:rmul (list vs ...)) _)
)
; rewrite
(r1cs:ror
(for/list ([v vs])
(r1cs:req
(r1cs:rint 0)
(r1cs:rmod v (r1cs:rint config:p))
)
)
)
]
; otherwise, do not rewrite
[_ arg-r1cs]
)
)