; -------------------------------------------------------------------------
; Boogie universal background predicate
; Copyright (c), Microsoft Corp.
(DEFPRED (<: t u))

(BG_PUSH (AND

  ; select/store axioms, 1 index argument

  (FORALL (A i v)
    (EQ (select1 (store1 A i v) i) v))

  (FORALL (A i j v)
    (IMPLIES (NEQ i j)
      (EQ
        (select1 (store1 A i v) j)
        (select1 A j))))

  ; select/store axioms, 2 index arguments

  (FORALL (A o f v)
    (EQ (select2 (store2 A o f v) o f) v))

  (FORALL (A o f p g v)
    (IMPLIES (NEQ o p)
      (EQ
        (select2 (store2 A o f v) p g)
        (select2 A p g))))

  (FORALL (A o f p g v)
    (IMPLIES (NEQ f g)
      (EQ
        (select2 (store2 A o f v) p g)
        (select2 A p g))))

  ; formula/term axioms

  (FORALL (x y)
    (IFF
      (EQ (boolIff x y) |@true|)
      (IFF (EQ x |@true|) (EQ y |@true|))))

  (FORALL (x y)
    (IFF
      (EQ (boolImplies x y) |@true|)
      (IMPLIES (EQ x |@true|) (EQ y |@true|))))

  (FORALL (x y)
    (IFF
      (EQ (boolAnd x y) |@true|)
      (AND (EQ x |@true|) (EQ y |@true|))))

  (FORALL (x y)
    (IFF
      (EQ (boolOr x y) |@true|)
      (OR (EQ x |@true|) (EQ y |@true|))))

  (FORALL (x)
    (PATS (boolNot x))
    (IFF
      (EQ (boolNot x) |@true|)
      (NEQ x |@true|)))

  (FORALL (x y)
    (IFF
      (EQ (anyEqual x y) |@true|)
      (EQ x y)))

  (FORALL (x y)
    (PATS (anyNeq x y))
    (IFF
      (EQ (anyNeq x y) |@true|)
      (NEQ x y)))

  (FORALL (x y)
    (IFF
      (EQ (intLess x y) |@true|)
      (< x y)))

  (FORALL (x y)
    (IFF
      (EQ (intAtMost x y) |@true|)
      (<= x y)))

  (FORALL (x y)
    (IFF
      (EQ (intAtLeast x y) |@true|)
      (>= x y)))

  (FORALL (x y)
    (IFF
      (EQ (intGreater x y) |@true|)
      (> x y)))

  ; false is not true

  (DISTINCT |@false| |@true|)

  ; <: is a partial order:  it is reflexive, transitive, and anti-symmetric

  (FORALL (t)
    (PATS (<: t t))
    (<: t t))

  (FORALL (t u v)
    (PATS (MPAT (<: t u) (<: u v)))
    (IMPLIES
      (AND (<: t u ) (<: u v))
      (<: t v)))

  (FORALL (t u)
    (PATS (MPAT (<: t u) (<: u t)))
    (IMPLIES
      (AND (<: t u) (<: u t))
      (EQ t u)))

  ;; The following axiom gives a way to typed produce verification conditions,
  ;; that is, verification conditions where the terms are typable.  To use these,
  ;; the VCExpressionGenerator.{CastTo,CastFrom} methods must be overridden.
  ;; Look for USE_SORTED_LOGIC in VCGeneration/VCExpr.ssc.
  ; (FORALL (val T U)
  ;   (PATS (TypeConvert (TypeConvert val T U) U T))
  ;   (EQ (TypeConvert (TypeConvert val T U) U T) val))

))  ;; AND, BG_PUSH
; End Boogie universal background predicate
; -------------------------------------------------------------------------