auipc.smt2

; fixed inputs
(declare-const imm_limbs_1 Int)
(declare-const imm_limbs_2 Int)
(declare-const imm_limbs_3 Int)

(declare-const from_pc Int)

; two versions of every variable and constraint, to check for nondeterminism
(declare-const pc_limbs_1 Int)
(declare-const pc_limbs_2 Int)
(declare-const pc_limbs_3 Int)
(declare-const pc_limbs_hack_1 Int)
(declare-const pc_limbs_hack_2 Int)
(declare-const pc_limbs_hack_3 Int)

(declare-const carry_0 Int)
(declare-const carry_1 Int)
(declare-const carry_2 Int)
(declare-const carry_3 Int)
(declare-const carry_hack_0 Int)
(declare-const carry_hack_1 Int)
(declare-const carry_hack_2 Int)
(declare-const carry_hack_3 Int)

(declare-const data_0 Int)
(declare-const data_1 Int)
(declare-const data_2 Int)
(declare-const data_3 Int)
(declare-const data_0_hack Int)
(declare-const data_1_hack Int)
(declare-const data_2_hack Int)
(declare-const data_3_hack Int)

;; Constants
(define-fun two_pow_8 () Int 256)
(define-fun two_pow_16 () Int 65536)
(define-fun two_pow_24 () Int 16777216)
(define-fun p () Int 2013265921)
(define-fun inv_256 () Int 2005401601)

;; concrete values from test

(assert (= from_pc 2110400))

(assert (= imm_limbs_1 0))
(assert (= imm_limbs_2 0))
(assert (= imm_limbs_3 0))

(assert (= pc_limbs_1 51))
(assert (= pc_limbs_2 32))
(assert (= pc_limbs_3 0))

(assert (= data_0 192))
(assert (= data_1 51))
(assert (= data_2 32))
(assert (= data_3 0))

;; Compute intermed_val
(define-fun intermed_val () Int
(mod
  (+ (* pc_limbs_1 two_pow_8)
     (* pc_limbs_2 two_pow_16)
     (* pc_limbs_3 two_pow_24))
  p
))
(define-fun intermed_val_hack () Int
(mod
  (+ (* pc_limbs_hack_1 two_pow_8)
     (* pc_limbs_hack_2 two_pow_16)
     (* pc_limbs_hack_3 two_pow_24))
  p
))

;; rd_data[0] = from_pc - intermed_val
(assert (= data_0 (mod (- from_pc intermed_val) p)))
(assert (= data_0_hack (mod (- from_pc intermed_val_hack) p)))

;; Range constraints

;; from_pc is 30-bit
(assert (and (<= 0 from_pc) (< from_pc 1073741824)))

(assert (and (<= 0 pc_limbs_1) (<= pc_limbs_1 255)))
; Correct constraints
;(assert (and (<= 0 pc_limbs_2) (<= pc_limbs_2 255)))
;(assert (and (<= 0 pc_limbs_3) (<= pc_limbs_3 63)))
(assert (and (<= 0 pc_limbs_2) (< pc_limbs_2 p)))
(assert (and (<= 0 pc_limbs_3) (< pc_limbs_3 p)))

(assert (and (<= 0 pc_limbs_hack_1) (<= pc_limbs_hack_1 255)))
; Correct constraints
;(assert (and (<= 0 pc_limbs_hack_2) (<= pc_limbs_hack_2 255)))
;(assert (and (<= 0 pc_limbs_hack_3) (<= pc_limbs_hack_3 63)))
(assert (and (<= 0 pc_limbs_hack_2) (< pc_limbs_hack_2 p)))
(assert (and (<= 0 pc_limbs_hack_3) (< pc_limbs_hack_3 p)))

(assert (and (<= 0 imm_limbs_1) (<= imm_limbs_1 255)))
(assert (and (<= 0 imm_limbs_2) (<= imm_limbs_2 255)))
(assert (and (<= 0 imm_limbs_3) (<= imm_limbs_3 255)))

(assert (and (<= 0 data_0) (<= data_0 255)))
(assert (and (<= 0 data_1) (<= data_1 255)))
(assert (and (<= 0 data_2) (<= data_2 255)))
(assert (and (<= 0 data_3) (<= data_3 255)))
(assert (and (<= 0 data_0_hack) (<= data_0_hack 255)))
(assert (and (<= 0 data_1_hack) (<= data_1_hack 255)))
(assert (and (<= 0 data_2_hack) (<= data_2_hack 255)))
(assert (and (<= 0 data_3_hack) (<= data_3_hack 255)))

;; Carry[0] is always 0
(assert (= carry_0 0))
;; Carry constraints (must be Boolean: 0 or 1)
(assert (or (= carry_1 0) (= carry_1 1)))
(assert (or (= carry_2 0) (= carry_2 1)))
(assert (or (= carry_3 0) (= carry_3 1)))

;; Carry[0] is always 0
(assert (= carry_hack_0 0))
;; Carry constraints (must be Boolean: 0 or 1)
(assert (or (= carry_hack_1 0) (= carry_hack_1 1)))
(assert (or (= carry_hack_2 0) (= carry_hack_2 1)))
(assert (or (= carry_hack_3 0) (= carry_hack_3 1)))

;; nondeterminism check

(assert (or
	(not (= data_0 data_0_hack))
	(not (= data_1 data_1_hack))
	(not (= data_2 data_2_hack))
	(not (= data_3 data_3_hack))
))

;; Carry propagation
(assert (= carry_1
  (mod (* (mod (+ (mod (+ pc_limbs_1 imm_limbs_1) p) (- data_1) carry_0) p) inv_256) p)))
(assert (= carry_hack_1
  (mod (* (mod (+ (mod (+ pc_limbs_hack_1 imm_limbs_1) p) (- data_1_hack) carry_hack_0) p) inv_256) p)))

(assert (= carry_2
  (mod (* (mod (+ (mod (+ pc_limbs_2 imm_limbs_2) p) (- data_2) carry_1) p) inv_256) p)))
(assert (= carry_hack_2
  (mod (* (mod (+ (mod (+ pc_limbs_hack_2 imm_limbs_2) p) (- data_2_hack) carry_hack_1) p) inv_256) p)))

(assert (= carry_3
  (mod (* (mod (+ (mod (+ pc_limbs_3 imm_limbs_3) p) (- data_3) carry_2) p) inv_256) p)))
(assert (= carry_hack_3
  (mod (* (mod (+ (mod (+ pc_limbs_hack_3 imm_limbs_3) p) (- data_3_hack) carry_hack_2) p) inv_256) p)))

(check-sat)
(get-model)