; ------------------------------------------------------------------------------
; Basic datatypes

(declare-datatypes ()
  ( (InfNat (mk-infnat (value Int) (isFin Bool) (isErr Bool)))
  )
)

(declare-datatypes ()
  ( (MaybeBool (mk-mb (prop Bool) (isErrorProp Bool)))
  )
)

(define-fun cryBool ((x Bool)) MaybeBool
  (mk-mb x false)
)

(define-fun cryErrProp () MaybeBool
  (mk-mb false true)
)

(define-fun cryInf () InfNat
  (mk-infnat 0 false false)
)

(define-fun cryNat ((x Int)) InfNat
  (mk-infnat x true false)
)

(define-fun cryErr () InfNat
  (mk-infnat 0 false true)
)

; ------------------------------------------------------------------------------
; Cryptol version of logic


(define-fun cryEq ((x InfNat) (y InfNat)) MaybeBool
  (ite (or (isErr x) (isErr y)) cryErrProp (cryBool
  (ite (isFin x)
     (ite (isFin y) (= (value x) (value y)) false)
     (not (isFin y))
  )))
)

(define-fun cryNeq ((x InfNat) (y InfNat)) MaybeBool
  (ite (or (isErr x) (isErr y)) cryErrProp (cryBool
  (ite (isFin x)
     (ite (isFin y) (not (= (value x) (value y))) true)
     (isFin y)
  )))
)

(define-fun cryFin ((x InfNat)) MaybeBool
  (ite (isErr x) cryErrProp (cryBool
  (isFin x)))
)

(define-fun cryGeq ((x InfNat) (y InfNat)) MaybeBool
  (ite (or (isErr x) (isErr y)) cryErrProp (cryBool
  (ite (isFin x)
    (ite (isFin y) (>= (value x) (value y)) false)
    true
  )))
)

(define-fun cryAnd ((x MaybeBool) (y MaybeBool)) MaybeBool
  (ite (or (isErrorProp x) (isErrorProp y)) cryErrProp
    (cryBool (and (prop x) (prop y)))
  )
)


(define-fun cryTrue () MaybeBool
  (cryBool true)
)

; ------------------------------------------------------------------------------
; Basic Cryptol assume/assert


(define-fun cryVar ((x InfNat)) Bool
  (and (not (isErr x)) (>= (value x) 0))
)

(define-fun cryAssume ((x MaybeBool)) Bool
  (ite (isErrorProp x) true (prop x))
)

(declare-fun cryUnknown () Bool)

(define-fun cryProve ((x MaybeBool)) Bool
  (ite (isErrorProp x) cryUnknown (not (prop x)))
)



; ------------------------------------------------------------------------------
; Arithmetic


(define-fun cryAdd ((x InfNat) (y InfNat)) InfNat
  (ite (or (isErr x) (isErr y)) cryErr
  (ite (isFin x)
       (ite (isFin y) (cryNat (+ (value x) (value y))) cryInf)
       cryInf
  ))
)

(define-fun crySub ((x InfNat) (y InfNat)) InfNat
  (ite (or (isErr x) (isErr y) (not (isFin y))) cryErr
  (ite (isFin x)
       (ite (>= (value x) (value y)) (cryNat (- (value x) (value y))) cryErr)
       cryInf
  ))
)

(define-fun cryMul ((x InfNat) (y InfNat)) InfNat
  (ite (or (isErr x) (isErr y)) cryErr
  (ite (isFin x)
       (ite (isFin y) (cryNat (* (value x) (value y)))
                      (ite (= (value x) 0) (cryNat 0) cryInf))
       (ite (and (isFin y) (= (value y) 0)) (cryNat 0) cryInf)
  ))
)

(define-fun cryDiv ((x InfNat) (y InfNat)) InfNat
  (ite (or (isErr x) (isErr y) (not (isFin x))) cryErr
  (ite (isFin y)
       (ite (= (value y) 0) cryErr (cryNat (div (value x) (value y))))
       (cryNat 0)
  ))
)

(define-fun cryMod ((x InfNat) (y InfNat)) InfNat
  (ite (or (isErr x) (isErr y) (not (isFin x))) cryErr
  (ite (isFin y)
       (ite (= (value y) 0) cryErr (cryNat (mod (value x) (value y))))
       x
  ))
)



(define-fun cryMin ((x InfNat) (y InfNat)) InfNat
  (ite (or (isErr x) (isErr y)) cryErr
  (ite (isFin x)
       (ite (isFin y)
            (ite (<= (value x) (value y)) x y)
            x)
       y
  ))
)

(define-fun cryMax ((x InfNat) (y InfNat)) InfNat
  (ite (or (isErr x) (isErr y)) cryErr
  (ite (isFin x)
       (ite (isFin y)
            (ite (<= (value x) (value y)) y x)
            y)
       x
  ))
)


(declare-fun cryWidthUnknown (Int) Int)

; Some axioms about cryWidthUnknown
(define-fun k_2_to_64 () Int 18446744073709551616)
(define-fun k_2_to_65 () Int 36893488147419103232)

(assert (forall ((x Int)) (or (> (cryWidthUnknown x) 64) (< x k_2_to_64))))
(assert (forall ((x Int)) (or (> x (cryWidthUnknown x))  (< x k_2_to_64))))

; This helps the #548 property
(assert (forall ((x Int)) (or (>= 65 (cryWidthUnknown x)) (>= x k_2_to_65))))


(assert (forall ((x Int) (y Int))
  (=> (>= x y)
      (>= (cryWidthUnknown x) (cryWidthUnknown y)))))


; this helps #548.  It seems to be quite slow, however.
; (assert (forall ((x Int) (y Int))
;   (=>
;     (>  y (cryWidthUnknown x))
;     (>= y (cryWidthUnknown (* 2 x)))
;   )
; ))



(define-fun cryWidthTable ((x Int)) Int
  (ite (< x 1) 0
  (ite (< x 2) 1
  (ite (< x 4) 2
  (ite (< x 8) 3
  (ite (< x 16) 4
  (ite (< x 32) 5
  (ite (< x 64) 6
  (ite (< x 128) 7
  (ite (< x 256) 8
  (ite (< x 512) 9
  (ite (< x 1024) 10
  (ite (< x 2048) 11
  (ite (< x 4096) 12
  (ite (< x 8192) 13
  (ite (< x 16384) 14
  (ite (< x 32768) 15
  (ite (< x 65536) 16
  (ite (< x 131072) 17
  (ite (< x 262144) 18
  (ite (< x 524288) 19
  (ite (< x 1048576) 20
  (ite (< x 2097152) 21
  (ite (< x 4194304) 22
  (ite (< x 8388608) 23
  (ite (< x 16777216) 24
  (ite (< x 33554432) 25
  (ite (< x 67108864) 26
  (ite (< x 134217728) 27
  (ite (< x 268435456) 28
  (ite (< x 536870912) 29
  (ite (< x 1073741824) 30
  (ite (< x 2147483648) 31
  (ite (< x 4294967296) 32
  (ite (< x 8589934592) 33
  (ite (< x 17179869184) 34
  (ite (< x 34359738368) 35
  (ite (< x 68719476736) 36
  (ite (< x 137438953472) 37
  (ite (< x 274877906944) 38
  (ite (< x 549755813888) 39
  (ite (< x 1099511627776) 40
  (ite (< x 2199023255552) 41
  (ite (< x 4398046511104) 42
  (ite (< x 8796093022208) 43
  (ite (< x 17592186044416) 44
  (ite (< x 35184372088832) 45
  (ite (< x 70368744177664) 46
  (ite (< x 140737488355328) 47
  (ite (< x 281474976710656) 48
  (ite (< x 562949953421312) 49
  (ite (< x 1125899906842624) 50
  (ite (< x 2251799813685248) 51
  (ite (< x 4503599627370496) 52
  (ite (< x 9007199254740992) 53
  (ite (< x 18014398509481984) 54
  (ite (< x 36028797018963968) 55
  (ite (< x 72057594037927936) 56
  (ite (< x 144115188075855872) 57
  (ite (< x 288230376151711744) 58
  (ite (< x 576460752303423488) 59
  (ite (< x 1152921504606846976) 60
  (ite (< x 2305843009213693952) 61
  (ite (< x 4611686018427387904) 62
  (ite (< x 9223372036854775808) 63
  (ite (< x 18446744073709551616) 64
  (cryWidthUnknown x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
)

(define-fun cryWidth ((x InfNat)) InfNat
  (ite (isErr x) cryErr
  (ite (isFin x) (cryNat (cryWidthTable (value x)))
       cryInf
  ))
)

(declare-fun cryExpUnknown (Int Int) Int)

(assert (forall ((x Int) (y Int))
  (=> (and (> y 0) (> x 0))
      (>= (cryExpUnknown x y) x))))

(define-fun cryExpTable ((x Int) (y Int)) Int
  (ite (= y 0) 1
  (ite (= y 1) x
  (ite (= x 0) 0
  (cryExpUnknown x y))))
)

(define-fun cryExp ((x InfNat) (y InfNat)) InfNat
  (ite (or (isErr x) (isErr y)) cryErr
    (ite (isFin x)
         (ite (isFin y)
              (cryNat (cryExpTable (value x) (value y)))
              (ite (< (value x) 2) x cryInf))
         (ite (isFin y)
              (ite (= (value y) 0) (cryNat 1) cryInf)
              cryInf)
  ))
)

(define-fun cryCeilDiv ((x InfNat) (y InfNat)) InfNat
  (ite (or (isErr x) (isErr y) (not (isFin y))) cryErr
  (ite (= (value y) 0) cryErr
  (ite (not (isFin x)) cryInf
    (cryNat (- (div (- (value x)) (value y))))
  )))
)

(define-fun cryCeilMod ((x InfNat) (y InfNat)) InfNat
  (ite (or (isErr x) (isErr y) (not (isFin y))) cryErr
  (ite (= (value y) 0) cryErr
  (ite (not (isFin x)) (cryNat 0)
    (cryNat (mod (- (value x)) (value y)))
  )))
)

(define-fun cryLenFromThenTo ((x InfNat) (y InfNat) (z InfNat)) InfNat
  (ite (or (isErr x) (not (isFin x))
           (isErr y) (not (isFin y))
           (isErr z) (not (isFin z))
           (= (value x) (value y))) cryErr (cryNat
  (ite (> (value x) (value y))
       (ite (> (value z) (value x)) 0 (+ (div (- (value x) (value z))
                                              (- (value x) (value y))) 1))
       (ite (< (value z) (value x)) 0 (+ (div (- (value z) (value x))
                                              (- (value y) (value x))) 1))
  )))
)


; ---


; (declare-fun L () InfNat)
; (declare-fun w () InfNat)
; 
; (assert (cryVar L))
; (assert (cryVar w))
; 
; (assert (cryAssume (cryFin w)))
; (assert (cryAssume (cryGeq w (cryNat 1))))
; (assert (cryAssume (cryGeq (cryMul (cryNat 2) w) (cryWidth L))))
; 
; (assert (cryProve
;   (cryGeq
;     (cryMul
;       (cryCeilDiv
;         (cryAdd (cryNat 1) (cryAdd L (cryMul (cryNat 2) w)))
;         (cryMul (cryNat 16) w))
;       (cryMul (cryNat 16) w))
;     (cryAdd (cryNat 1) (cryAdd L (cryMul (cryNat 2) w))))))
; 
; (check-sat)