0x03.smt

(set-logic QF_BV)

; Convention here is add a label to the end of the register
; to mark a step in the program for which the value applies.
; e.g.
; rdx0 is the first value of rdx, rdx1 is the value at the
; next step of the program, rdxN is the value at the Nth
; step.
;
; Essentially, we're turning an assembly program into SSA form
(declare-fun rdx0 () ( _ BitVec 64))
(declare-fun rdx1 () ( _ BitVec 64))

(declare-fun rcx0 () ( _ BitVec 64))
(declare-fun rcx1 () ( _ BitVec 64))
(declare-fun rcx2 () ( _ BitVec 64))

(declare-fun rax0 () ( _ BitVec 64))
(declare-fun rax3 () ( _ BitVec 64))

; The carry flag
(declare-fun cf () (_ Bool))

; sub sets the carry flag if unsigned subtraction will result in
; an overflow i.e. rax0 > rdx0
(assert ( = cf (bvult rdx0 rax0)))
(assert ( = rdx1 (bvsub rdx0 rax0)))

; sbb is 'subtract with carry'. If the carry flag is set, we take
; away one from the result of sub
(assert ( = rcx1
(ite (= cf true)
 (bvsub (bvsub rcx0 rcx0) #x0000000000000001)
 (bvsub rcx0 rcx0))
))

; and rxc1,rdx1
(assert ( = rcx2 (bvand rcx1 rdx1)))
; add rax0,rcv2
(assert ( = rax3 (bvadd rax0 rcx2)))

; assert conditions which should fail if this is indeed a minimum
; function. In the case below, we assert that rax0 <= rdx0 and
; rax3 != rax0 (which we suspect is false) and so if we get 'unsat'
; as the result, then we've proved rax0 <= rdx0 => rax3 == rax0

; note the use of push here. Allows us to reuse the work above by
; popping the asserts below from the stack
(push 1)
    (assert ( or (bvult rax0 rdx0) (not (distinct rax0 rdx0))))
        (check-sat)
        (push 1)
            (assert ( distinct rax3 rax0))
            (check-sat)
(pop 2)

; We show here that rax0 > rdx0 (along with our previous assertions) can
; can be satisfied. We then show that adding rax3 != rdx0 leads to
; unsat, which means that rax3 == rdx0
(assert (bvugt rax0 rdx0))
(check-sat)
(assert ( distinct rax3 rdx0))

(check-sat)