search

mmcloughlin / ec3

Elliptic Curve Cryptography Compiler: an incomplete experiment in code-generation for elliptic curves in Go
BSD 3-Clause "New" or "Revised" License
56 stars 5 forks source link

arith: verify arithmetic programs #101

Open mmcloughlin opened 4 years ago

mmcloughlin commented 4 years ago

Tooling to verify arithmetic programs with Z3.

Related #96 #99

mmcloughlin commented 4 years ago

Hitting a wall with multiplication verification. The following SMT2 defines the problem to verify multiplication of 16-bit values represented as 2x8-bit words. This does not terminate in reasonable time (30 minutes+). Note the precise same problem for 8-bit multiply with 2x4-bit words returns unsat in a few seconds.

(set-logic QF_BV)
(declare-fun y () (_ BitVec 16))
(declare-fun x () (_ BitVec 16))
(assert (let ((a!1 ((_ extract 15 8)
             (bvmul ((_ zero_extend 8) ((_ extract 7 0) x))
                    ((_ zero_extend 8) ((_ extract 15 8) y)))))
      (a!2 ((_ extract 15 8)
             (bvmul ((_ zero_extend 8) ((_ extract 7 0) x))
                    ((_ zero_extend 8) ((_ extract 7 0) y)))))
      (a!4 ((_ extract 7 0)
             (bvmul ((_ zero_extend 8) ((_ extract 7 0) x))
                    ((_ zero_extend 8) ((_ extract 15 8) y)))))
      (a!7 ((_ extract 15 8)
             (bvmul ((_ zero_extend 8) ((_ extract 15 8) x))
                    ((_ zero_extend 8) ((_ extract 7 0) y)))))
      (a!9 ((_ extract 7 0)
             (bvmul ((_ zero_extend 8) ((_ extract 15 8) x))
                    ((_ zero_extend 8) ((_ extract 7 0) y)))))
      (a!13 ((_ extract 15 8)
              (bvmul ((_ zero_extend 8) ((_ extract 15 8) x))
                     ((_ zero_extend 8) ((_ extract 15 8) y)))))
      (a!15 ((_ extract 7 0)
              (bvmul ((_ zero_extend 8) ((_ extract 15 8) x))
                     ((_ zero_extend 8) ((_ extract 15 8) y)))))
      (a!17 ((_ extract 7 0)
              (bvmul ((_ zero_extend 8) ((_ extract 7 0) x))
                     ((_ zero_extend 8) ((_ extract 7 0) y))))))
(let ((a!3 ((_ zero_extend 1)
             ((_ extract 7 0)
               (bvadd ((_ zero_extend 1) #x00)
                      ((_ zero_extend 1) a!2)
                      ((_ zero_extend 8) #b0))))))
(let ((a!5 ((_ zero_extend 8)
             ((_ extract 8 8)
               (bvadd a!3 ((_ zero_extend 1) a!4) ((_ zero_extend 8) #b0)))))
      (a!8 ((_ zero_extend 1)
             ((_ extract 7 0)
               (bvadd a!3 ((_ zero_extend 1) a!4) ((_ zero_extend 8) #b0))))))
(let ((a!6 ((_ zero_extend 1)
             ((_ extract 7 0)
               (bvadd ((_ zero_extend 1) #x00) ((_ zero_extend 1) a!1) a!5))))
      (a!10 ((_ zero_extend 8)
              ((_ extract 8 8)
                (bvadd a!8 ((_ zero_extend 1) a!9) ((_ zero_extend 8) #b0)))))
      (a!18 (concat ((_ extract 7 0)
                      (bvadd a!8
                             ((_ zero_extend 1) a!9)
                             ((_ zero_extend 8) #b0)))
                    ((_ extract 7 0)
                      (bvadd ((_ zero_extend 1) #x00)
                             ((_ zero_extend 1) a!17)
                             ((_ zero_extend 8) #b0))))))
(let ((a!11 ((_ zero_extend 8)
              ((_ extract 8 8) (bvadd a!6 ((_ zero_extend 1) a!7) a!10))))
      (a!14 ((_ zero_extend 1)
              ((_ extract 7 0) (bvadd a!6 ((_ zero_extend 1) a!7) a!10)))))
(let ((a!12 ((_ zero_extend 1)
              ((_ extract 7 0)
                (bvadd ((_ zero_extend 1) #x00) ((_ zero_extend 1) #x00) a!11))))
      (a!16 ((_ zero_extend 8)
              ((_ extract 8 8)
                (bvadd a!14 ((_ zero_extend 1) a!15) ((_ zero_extend 8) #b0)))))
      (a!19 (concat ((_ extract 7 0)
                      (bvadd a!14
                             ((_ zero_extend 1) a!15)
                             ((_ zero_extend 8) #b0)))
                    a!18)))
(let ((a!20 (concat ((_ extract 7 0) (bvadd a!12 ((_ zero_extend 1) a!13) a!16))
                    a!19)))
(let ((a!21 (and true
                 (= a!20 (bvmul ((_ zero_extend 16) x) ((_ zero_extend 16) y))))))
  (not a!21))))))))))
(check-sat)

Things to try:

mmcloughlin commented 3 years ago

In retrospect, this is excellent advice:

I would recommend that anyone interested in this does what I didn't do and learn SMTLIB2 format rather than the motley collection of programmatic interfaces. SMTLIB2 will allow you to talk to all the solvers. but AFAIK there aren't any APIs that cover more than a handful.

https://twitter.com/geofflangdale/status/1325551569035620352

mmcloughlin commented 3 years ago

See also: