text:
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below    *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.EuclideanDivision.
Require bool.Bool.
Require real.Real.
Require real.RealInfix.
Require real.FromInt.

Parameter pow2: Z -> Z.

Axiom Power_0 : ((pow2 0%Z) = 1%Z).

Axiom Power_s : forall (n:Z), (0%Z <= n)%Z ->
  ((pow2 (n + 1%Z)%Z) = (2%Z * (pow2 n))%Z).

Axiom Power_1 : ((pow2 1%Z) = 2%Z).

Axiom Power_sum : forall (n:Z) (m:Z), ((0%Z <= n)%Z /\ (0%Z <= m)%Z) ->
  ((pow2 (n + m)%Z) = ((pow2 n) * (pow2 m))%Z).

Axiom pow2pos : forall (i:Z), (0%Z <= i)%Z -> (0%Z < (pow2 i))%Z.

Axiom pow2_0 : ((pow2 0%Z) = 1%Z).

Axiom pow2_1 : ((pow2 1%Z) = 2%Z).

Axiom pow2_2 : ((pow2 2%Z) = 4%Z).

Axiom pow2_3 : ((pow2 3%Z) = 8%Z).

Axiom pow2_4 : ((pow2 4%Z) = 16%Z).

Axiom pow2_5 : ((pow2 5%Z) = 32%Z).

Axiom pow2_6 : ((pow2 6%Z) = 64%Z).

Axiom pow2_7 : ((pow2 7%Z) = 128%Z).

Axiom pow2_8 : ((pow2 8%Z) = 256%Z).

Axiom pow2_9 : ((pow2 9%Z) = 512%Z).

Axiom pow2_10 : ((pow2 10%Z) = 1024%Z).

Axiom pow2_11 : ((pow2 11%Z) = 2048%Z).

Axiom pow2_12 : ((pow2 12%Z) = 4096%Z).

Axiom pow2_13 : ((pow2 13%Z) = 8192%Z).

Axiom pow2_14 : ((pow2 14%Z) = 16384%Z).

Axiom pow2_15 : ((pow2 15%Z) = 32768%Z).

Axiom pow2_16 : ((pow2 16%Z) = 65536%Z).

Axiom pow2_17 : ((pow2 17%Z) = 131072%Z).

Axiom pow2_18 : ((pow2 18%Z) = 262144%Z).

Axiom pow2_19 : ((pow2 19%Z) = 524288%Z).

Axiom pow2_20 : ((pow2 20%Z) = 1048576%Z).

Axiom pow2_21 : ((pow2 21%Z) = 2097152%Z).

Axiom pow2_22 : ((pow2 22%Z) = 4194304%Z).

Axiom pow2_23 : ((pow2 23%Z) = 8388608%Z).

Axiom pow2_24 : ((pow2 24%Z) = 16777216%Z).

Axiom pow2_25 : ((pow2 25%Z) = 33554432%Z).

Axiom pow2_26 : ((pow2 26%Z) = 67108864%Z).

Axiom pow2_27 : ((pow2 27%Z) = 134217728%Z).

Axiom pow2_28 : ((pow2 28%Z) = 268435456%Z).

Axiom pow2_29 : ((pow2 29%Z) = 536870912%Z).

Axiom pow2_30 : ((pow2 30%Z) = 1073741824%Z).

Axiom pow2_31 : ((pow2 31%Z) = 2147483648%Z).

Axiom pow2_32 : ((pow2 32%Z) = 4294967296%Z).

Axiom pow2_33 : ((pow2 33%Z) = 8589934592%Z).

Axiom pow2_34 : ((pow2 34%Z) = 17179869184%Z).

Axiom pow2_35 : ((pow2 35%Z) = 34359738368%Z).

Axiom pow2_36 : ((pow2 36%Z) = 68719476736%Z).

Axiom pow2_37 : ((pow2 37%Z) = 137438953472%Z).

Axiom pow2_38 : ((pow2 38%Z) = 274877906944%Z).

Axiom pow2_39 : ((pow2 39%Z) = 549755813888%Z).

Axiom pow2_40 : ((pow2 40%Z) = 1099511627776%Z).

Axiom pow2_41 : ((pow2 41%Z) = 2199023255552%Z).

Axiom pow2_42 : ((pow2 42%Z) = 4398046511104%Z).

Axiom pow2_43 : ((pow2 43%Z) = 8796093022208%Z).

Axiom pow2_44 : ((pow2 44%Z) = 17592186044416%Z).

Axiom pow2_45 : ((pow2 45%Z) = 35184372088832%Z).

Axiom pow2_46 : ((pow2 46%Z) = 70368744177664%Z).

Axiom pow2_47 : ((pow2 47%Z) = 140737488355328%Z).

Axiom pow2_48 : ((pow2 48%Z) = 281474976710656%Z).

Axiom pow2_49 : ((pow2 49%Z) = 562949953421312%Z).

Axiom pow2_50 : ((pow2 50%Z) = 1125899906842624%Z).

Axiom pow2_51 : ((pow2 51%Z) = 2251799813685248%Z).

Axiom pow2_52 : ((pow2 52%Z) = 4503599627370496%Z).

Axiom pow2_53 : ((pow2 53%Z) = 9007199254740992%Z).

Axiom pow2_54 : ((pow2 54%Z) = 18014398509481984%Z).

Axiom pow2_55 : ((pow2 55%Z) = 36028797018963968%Z).

Axiom pow2_56 : ((pow2 56%Z) = 72057594037927936%Z).

Axiom pow2_57 : ((pow2 57%Z) = 144115188075855872%Z).

Axiom pow2_58 : ((pow2 58%Z) = 288230376151711744%Z).

Axiom pow2_59 : ((pow2 59%Z) = 576460752303423488%Z).

Axiom pow2_60 : ((pow2 60%Z) = 1152921504606846976%Z).

Axiom pow2_61 : ((pow2 61%Z) = 2305843009213693952%Z).

Axiom pow2_62 : ((pow2 62%Z) = 4611686018427387904%Z).

Axiom pow2_63 : ((pow2 63%Z) = 9223372036854775808%Z).

Axiom Div_double : forall (x:Z) (y:Z), (((0%Z < y)%Z /\ (y <= x)%Z) /\
  (x < (2%Z * y)%Z)%Z) -> ((int.EuclideanDivision.div x y) = 1%Z).

Axiom Div_pow : forall (x:Z) (i:Z), (0%Z < i)%Z ->
  ((((pow2 (i - 1%Z)%Z) <= x)%Z /\ (x < (pow2 i))%Z) ->
  ((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = 1%Z)).

Axiom Div_double_neg : forall (x:Z) (y:Z), (((((-2%Z)%Z * y)%Z <= x)%Z /\
  (x < (-y)%Z)%Z) /\ ((-y)%Z < 0%Z)%Z) -> ((int.EuclideanDivision.div x
  y) = (-2%Z)%Z).

Axiom Div_pow2 : forall (x:Z) (i:Z), (0%Z < i)%Z ->
  ((((-(pow2 i))%Z <= x)%Z /\ (x < (-(pow2 (i - 1%Z)%Z))%Z)%Z) ->
  ((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = (-2%Z)%Z)).

Axiom Mod_pow2_gen : forall (x:Z) (i:Z) (k:Z), ((0%Z <= k)%Z /\ (k < i)%Z) ->
  ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div (x + (pow2 i))%Z
  (pow2 k)) 2%Z) = (int.EuclideanDivision.mod1 (int.EuclideanDivision.div x
  (pow2 k)) 2%Z)).

Parameter pow21: Z -> R.

Axiom Power_01 : ((pow21 0%Z) = 1%R).

Axiom Power_s1 : forall (n:Z), (0%Z <= n)%Z ->
  ((pow21 (n + 1%Z)%Z) = (2%R * (pow21 n))%R).

Axiom Power_p : forall (n:Z), (n <= 0%Z)%Z ->
  ((pow21 (n - 1%Z)%Z) = ((05 / 10)%R * (pow21 n))%R).

Axiom Power_s_all : forall (n:Z),
  ((pow21 (n + 1%Z)%Z) = (2%R * (pow21 n))%R).

Axiom Power_p_all : forall (n:Z),
  ((pow21 (n - 1%Z)%Z) = ((05 / 10)%R * (pow21 n))%R).

Axiom Power_1_2 : ((05 / 10)%R = (Rdiv 1%R 2%R)%R).

Axiom Power_11 : ((pow21 1%Z) = 2%R).

Axiom Power_neg1 : ((pow21 (-1%Z)%Z) = (05 / 10)%R).

Axiom Power_non_null_aux : forall (n:Z), (0%Z <= n)%Z -> ~ ((pow21 n) = 0%R).

Axiom Power_neg_aux : forall (n:Z), (0%Z <= n)%Z ->
  ((pow21 (-n)%Z) = (Rdiv 1%R (pow21 n))%R).

Axiom Power_non_null : forall (n:Z), ~ ((pow21 n) = 0%R).

Axiom Power_neg : forall (n:Z), ((pow21 (-n)%Z) = (Rdiv 1%R (pow21 n))%R).

Axiom Power_sum_aux : forall (n:Z) (m:Z), (0%Z <= m)%Z ->
  ((pow21 (n + m)%Z) = ((pow21 n) * (pow21 m))%R).

Axiom Power_sum1 : forall (n:Z) (m:Z),
  ((pow21 (n + m)%Z) = ((pow21 n) * (pow21 m))%R).

Axiom Pow2_int_real : forall (x:Z), (0%Z <= x)%Z ->
  ((pow21 x) = (IZR (pow2 x))).

Axiom size_positive : (1%Z < 32%Z)%Z.

Axiom bv : Type.
Parameter bv_WhyType : WhyType bv.
Existing Instance bv_WhyType.

Parameter nth: bv -> Z -> bool.

Parameter bvzero: bv.

Axiom Nth_zero : forall (n:Z), ((0%Z <= n)%Z /\ (n < 32%Z)%Z) -> ((nth bvzero
  n) = false).

Parameter bvone: bv.

Axiom Nth_one : forall (n:Z), ((0%Z <= n)%Z /\ (n < 32%Z)%Z) -> ((nth bvone
  n) = true).

(* Why3 assumption *)
Definition eq (v1:bv) (v2:bv): Prop := forall (n:Z), ((0%Z <= n)%Z /\
  (n < 32%Z)%Z) -> ((nth v1 n) = (nth v2 n)).

Axiom extensionality : forall (v1:bv) (v2:bv), (eq v1 v2) -> (v1 = v2).

Parameter bw_and: bv -> bv -> bv.

Axiom Nth_bw_and : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\
  (n < 32%Z)%Z) -> ((nth (bw_and v1 v2) n) = (andb (nth v1 n) (nth v2 n))).

Parameter bw_or: bv -> bv -> bv.

Axiom Nth_bw_or : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\
  (n < 32%Z)%Z) -> ((nth (bw_or v1 v2) n) = (orb (nth v1 n) (nth v2 n))).

Parameter bw_xor: bv -> bv -> bv.

Axiom Nth_bw_xor : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\
  (n < 32%Z)%Z) -> ((nth (bw_xor v1 v2) n) = (xorb (nth v1 n) (nth v2 n))).

Axiom Nth_bw_xor_v1true : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
  (n < 32%Z)%Z) /\ ((nth v1 n) = true)) -> ((nth (bw_xor v1 v2)
  n) = (negb (nth v2 n))).

Axiom Nth_bw_xor_v1false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
  (n < 32%Z)%Z) /\ ((nth v1 n) = false)) -> ((nth (bw_xor v1 v2) n) = (nth v2
  n)).

Axiom Nth_bw_xor_v2true : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
  (n < 32%Z)%Z) /\ ((nth v2 n) = true)) -> ((nth (bw_xor v1 v2)
  n) = (negb (nth v1 n))).

Axiom Nth_bw_xor_v2false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
  (n < 32%Z)%Z) /\ ((nth v2 n) = false)) -> ((nth (bw_xor v1 v2) n) = (nth v1
  n)).

Parameter bw_not: bv -> bv.

Axiom Nth_bw_not : forall (v:bv) (n:Z), ((0%Z <= n)%Z /\ (n < 32%Z)%Z) ->
  ((nth (bw_not v) n) = (negb (nth v n))).

Parameter lsr: bv -> Z -> bv.

Axiom lsr_nth_low : forall (b:bv) (n:Z) (s:Z), (((0%Z <= n)%Z /\
  (n < 32%Z)%Z) /\ (((0%Z <= s)%Z /\ (s < 32%Z)%Z) /\
  ((n + s)%Z < 32%Z)%Z)) -> ((nth (lsr b s) n) = (nth b (n + s)%Z)).

Axiom lsr_nth_high : forall (b:bv) (n:Z) (s:Z), (((0%Z <= n)%Z /\
  (n < 32%Z)%Z) /\ (((0%Z <= s)%Z /\ (s < 32%Z)%Z) /\
  (32%Z <= (n + s)%Z)%Z)) -> ((nth (lsr b s) n) = false).

Parameter asr: bv -> Z -> bv.

Axiom asr_nth_low : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
  (n < 32%Z)%Z) -> ((0%Z <= s)%Z -> (((n + s)%Z < 32%Z)%Z -> ((nth (asr b s)
  n) = (nth b (n + s)%Z)))).

Axiom asr_nth_high : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
  (n < 32%Z)%Z) -> ((0%Z <= s)%Z -> ((32%Z <= (n + s)%Z)%Z -> ((nth (asr b s)
  n) = (nth b (32%Z - 1%Z)%Z)))).

Parameter lsl: bv -> Z -> bv.

Axiom lsl_nth_high : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
  (n < 32%Z)%Z) -> ((0%Z <= s)%Z -> ((0%Z <= (n - s)%Z)%Z -> ((nth (lsl b s)
  n) = (nth b (n - s)%Z)))).

Axiom lsl_nth_low : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
  (n < 32%Z)%Z) -> ((0%Z <= s)%Z -> (((n - s)%Z < 0%Z)%Z -> ((nth (lsl b s)
  n) = false))).

Parameter to_nat_sub: bv -> Z -> Z -> Z.

Axiom to_nat_sub_zero : forall (b:bv) (j:Z) (i:Z), (((0%Z <= i)%Z /\
  (i <= j)%Z) /\ (j < 32%Z)%Z) -> (((nth b j) = false) -> ((to_nat_sub b j
  i) = (to_nat_sub b (j - 1%Z)%Z i))).

Axiom to_nat_sub_one : forall (b:bv) (j:Z) (i:Z), (((0%Z <= i)%Z /\
  (i <= j)%Z) /\ (j < 32%Z)%Z) -> (((nth b j) = true) -> ((to_nat_sub b j
  i) = ((pow2 (j - i)%Z) + (to_nat_sub b (j - 1%Z)%Z i))%Z)).

Axiom to_nat_sub_high : forall (b:bv) (j:Z) (i:Z), (j < i)%Z ->
  ((to_nat_sub b j i) = 0%Z).

Axiom to_nat_of_zero2 : forall (b:bv) (i:Z) (j:Z), (((j < 32%Z)%Z /\
  (i <= j)%Z) /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\
  (i < k)%Z) -> ((nth b k) = false)) -> ((to_nat_sub b j 0%Z) = (to_nat_sub b
  i 0%Z))).

Axiom to_nat_of_zero : forall (b:bv) (i:Z) (j:Z), ((j < 32%Z)%Z /\
  (0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\ (i <= k)%Z) -> ((nth b
  k) = false)) -> ((to_nat_sub b j i) = 0%Z)).

Axiom to_nat_of_one : forall (b:bv) (i:Z) (j:Z), (((j < 32%Z)%Z /\
  (i <= j)%Z) /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\
  (i <= k)%Z) -> ((nth b k) = true)) -> ((to_nat_sub b j
  i) = ((pow2 ((j - i)%Z + 1%Z)%Z) - 1%Z)%Z)).

Axiom to_nat_sub_footprint : forall (b1:bv) (b2:bv) (j:Z) (i:Z),
  ((j < 32%Z)%Z /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((i <= k)%Z /\
  (k <= j)%Z) -> ((nth b1 k) = (nth b2 k))) -> ((to_nat_sub b1 j
  i) = (to_nat_sub b2 j i))).

Parameter from_int: Z -> bv.

Axiom nth_from_int_high_even : forall (n:Z) (i:Z), (((i < 32%Z)%Z /\
  (0%Z <= i)%Z) /\ ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n
  (pow2 i)) 2%Z) = 0%Z)) -> ((nth (from_int n) i) = false).

Axiom nth_from_int_high_odd : forall (n:Z) (i:Z), (((i < 32%Z)%Z /\
  (0%Z <= i)%Z) /\
  ~ ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n (pow2 i))
  2%Z) = 0%Z)) -> ((nth (from_int n) i) = true).

Axiom nth_from_int_low_even : forall (n:Z), ((int.EuclideanDivision.mod1 n
  2%Z) = 0%Z) -> ((nth (from_int n) 0%Z) = false).

Axiom nth_from_int_low_odd : forall (n:Z), (~ ((int.EuclideanDivision.mod1 n
  2%Z) = 0%Z)) -> ((nth (from_int n) 0%Z) = true).

Axiom nth_from_int_0 : forall (i:Z), ((i < 32%Z)%Z /\ (0%Z <= i)%Z) ->
  ((nth (from_int 0%Z) i) = false).

Parameter from_int2c: Z -> bv.

Axiom nth_sign_positive : forall (n:Z), (0%Z <= n)%Z -> ((nth (from_int2c n)
  (32%Z - 1%Z)%Z) = false).

Axiom nth_sign_negative : forall (n:Z), (n < 0%Z)%Z -> ((nth (from_int2c n)
  (32%Z - 1%Z)%Z) = true).

Axiom nth_from_int2c_high_even : forall (n:Z) (i:Z),
  (((i < (32%Z - 1%Z)%Z)%Z /\ (0%Z <= i)%Z) /\
  ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n (pow2 i))
  2%Z) = 0%Z)) -> ((nth (from_int2c n) i) = false).

Axiom nth_from_int2c_high_odd : forall (n:Z) (i:Z),
  (((i < (32%Z - 1%Z)%Z)%Z /\ (0%Z <= i)%Z) /\
  ~ ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n (pow2 i))
  2%Z) = 0%Z)) -> ((nth (from_int2c n) i) = true).

Axiom nth_from_int2c_low_even : forall (n:Z), ((int.EuclideanDivision.mod1 n
  2%Z) = 0%Z) -> ((nth (from_int2c n) 0%Z) = false).

Axiom nth_from_int2c_low_odd : forall (n:Z),
  (~ ((int.EuclideanDivision.mod1 n 2%Z) = 0%Z)) -> ((nth (from_int2c n)
  0%Z) = true).

Axiom nth_from_int2c_0 : forall (i:Z), ((i < 32%Z)%Z /\ (0%Z <= i)%Z) ->
  ((nth (from_int2c 0%Z) i) = false).

Axiom nth_from_int2c_plus_pow2 : forall (x:Z) (k:Z) (i:Z), (((0%Z <= k)%Z /\
  (k < i)%Z) /\ (k < (32%Z - 1%Z)%Z)%Z) ->
  ((nth (from_int2c (x + (pow2 i))%Z) k) = (nth (from_int2c x) k)).

Axiom size_positive1 : (1%Z < 64%Z)%Z.

Axiom bv1 : Type.
Parameter bv1_WhyType : WhyType bv1.
Existing Instance bv1_WhyType.

Parameter nth1: bv1 -> Z -> bool.

Parameter bvzero1: bv1.

Axiom Nth_zero1 : forall (n:Z), ((0%Z <= n)%Z /\ (n < 64%Z)%Z) ->
  ((nth1 bvzero1 n) = false).

Parameter bvone1: bv1.

Axiom Nth_one1 : forall (n:Z), ((0%Z <= n)%Z /\ (n < 64%Z)%Z) ->
  ((nth1 bvone1 n) = true).

(* Why3 assumption *)
Definition eq1 (v1:bv1) (v2:bv1): Prop := forall (n:Z), ((0%Z <= n)%Z /\
  (n < 64%Z)%Z) -> ((nth1 v1 n) = (nth1 v2 n)).

Axiom extensionality1 : forall (v1:bv1) (v2:bv1), (eq1 v1 v2) -> (v1 = v2).

Parameter bw_and1: bv1 -> bv1 -> bv1.

Axiom Nth_bw_and1 : forall (v1:bv1) (v2:bv1) (n:Z), ((0%Z <= n)%Z /\
  (n < 64%Z)%Z) -> ((nth1 (bw_and1 v1 v2) n) = (andb (nth1 v1 n) (nth1 v2
  n))).

Parameter bw_or1: bv1 -> bv1 -> bv1.

Axiom Nth_bw_or1 : forall (v1:bv1) (v2:bv1) (n:Z), ((0%Z <= n)%Z /\
  (n < 64%Z)%Z) -> ((nth1 (bw_or1 v1 v2) n) = (orb (nth1 v1 n) (nth1 v2 n))).

Parameter bw_xor1: bv1 -> bv1 -> bv1.

Axiom Nth_bw_xor1 : forall (v1:bv1) (v2:bv1) (n:Z), ((0%Z <= n)%Z /\
  (n < 64%Z)%Z) -> ((nth1 (bw_xor1 v1 v2) n) = (xorb (nth1 v1 n) (nth1 v2
  n))).

Axiom Nth_bw_xor_v1true1 : forall (v1:bv1) (v2:bv1) (n:Z), (((0%Z <= n)%Z /\
  (n < 64%Z)%Z) /\ ((nth1 v1 n) = true)) -> ((nth1 (bw_xor1 v1 v2)
  n) = (negb (nth1 v2 n))).

Axiom Nth_bw_xor_v1false1 : forall (v1:bv1) (v2:bv1) (n:Z), (((0%Z <= n)%Z /\
  (n < 64%Z)%Z) /\ ((nth1 v1 n) = false)) -> ((nth1 (bw_xor1 v1 v2)
  n) = (nth1 v2 n)).

Axiom Nth_bw_xor_v2true1 : forall (v1:bv1) (v2:bv1) (n:Z), (((0%Z <= n)%Z /\
  (n < 64%Z)%Z) /\ ((nth1 v2 n) = true)) -> ((nth1 (bw_xor1 v1 v2)
  n) = (negb (nth1 v1 n))).

Axiom Nth_bw_xor_v2false1 : forall (v1:bv1) (v2:bv1) (n:Z), (((0%Z <= n)%Z /\
  (n < 64%Z)%Z) /\ ((nth1 v2 n) = false)) -> ((nth1 (bw_xor1 v1 v2)
  n) = (nth1 v1 n)).

Parameter bw_not1: bv1 -> bv1.

Axiom Nth_bw_not1 : forall (v:bv1) (n:Z), ((0%Z <= n)%Z /\ (n < 64%Z)%Z) ->
  ((nth1 (bw_not1 v) n) = (negb (nth1 v n))).

Parameter lsr1: bv1 -> Z -> bv1.

Axiom lsr_nth_low1 : forall (b:bv1) (n:Z) (s:Z), (((0%Z <= n)%Z /\
  (n < 64%Z)%Z) /\ (((0%Z <= s)%Z /\ (s < 64%Z)%Z) /\
  ((n + s)%Z < 64%Z)%Z)) -> ((nth1 (lsr1 b s) n) = (nth1 b (n + s)%Z)).

Axiom lsr_nth_high1 : forall (b:bv1) (n:Z) (s:Z), (((0%Z <= n)%Z /\
  (n < 64%Z)%Z) /\ (((0%Z <= s)%Z /\ (s < 64%Z)%Z) /\
  (64%Z <= (n + s)%Z)%Z)) -> ((nth1 (lsr1 b s) n) = false).

Parameter asr1: bv1 -> Z -> bv1.

Axiom asr_nth_low1 : forall (b:bv1) (n:Z) (s:Z), ((0%Z <= n)%Z /\
  (n < 64%Z)%Z) -> ((0%Z <= s)%Z -> (((n + s)%Z < 64%Z)%Z -> ((nth1 (asr1 b
  s) n) = (nth1 b (n + s)%Z)))).

Axiom asr_nth_high1 : forall (b:bv1) (n:Z) (s:Z), ((0%Z <= n)%Z /\
  (n < 64%Z)%Z) -> ((0%Z <= s)%Z -> ((64%Z <= (n + s)%Z)%Z -> ((nth1 (asr1 b
  s) n) = (nth1 b (64%Z - 1%Z)%Z)))).

Parameter lsl1: bv1 -> Z -> bv1.

Axiom lsl_nth_high1 : forall (b:bv1) (n:Z) (s:Z), ((0%Z <= n)%Z /\
  (n < 64%Z)%Z) -> ((0%Z <= s)%Z -> ((0%Z <= (n - s)%Z)%Z -> ((nth1 (lsl1 b
  s) n) = (nth1 b (n - s)%Z)))).

Axiom lsl_nth_low1 : forall (b:bv1) (n:Z) (s:Z), ((0%Z <= n)%Z /\
  (n < 64%Z)%Z) -> ((0%Z <= s)%Z -> (((n - s)%Z < 0%Z)%Z -> ((nth1 (lsl1 b s)
  n) = false))).

Parameter to_nat_sub1: bv1 -> Z -> Z -> Z.

Axiom to_nat_sub_zero1 : forall (b:bv1) (j:Z) (i:Z), (((0%Z <= i)%Z /\
  (i <= j)%Z) /\ (j < 64%Z)%Z) -> (((nth1 b j) = false) -> ((to_nat_sub1 b j
  i) = (to_nat_sub1 b (j - 1%Z)%Z i))).

Axiom to_nat_sub_one1 : forall (b:bv1) (j:Z) (i:Z), (((0%Z <= i)%Z /\
  (i <= j)%Z) /\ (j < 64%Z)%Z) -> (((nth1 b j) = true) -> ((to_nat_sub1 b j
  i) = ((pow2 (j - i)%Z) + (to_nat_sub1 b (j - 1%Z)%Z i))%Z)).

Axiom to_nat_sub_high1 : forall (b:bv1) (j:Z) (i:Z), (j < i)%Z ->
  ((to_nat_sub1 b j i) = 0%Z).

Axiom to_nat_of_zero21 : forall (b:bv1) (i:Z) (j:Z), (((j < 64%Z)%Z /\
  (i <= j)%Z) /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\
  (i < k)%Z) -> ((nth1 b k) = false)) -> ((to_nat_sub1 b j
  0%Z) = (to_nat_sub1 b i 0%Z))).

Axiom to_nat_of_zero1 : forall (b:bv1) (i:Z) (j:Z), ((j < 64%Z)%Z /\
  (0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\ (i <= k)%Z) -> ((nth1 b
  k) = false)) -> ((to_nat_sub1 b j i) = 0%Z)).

Axiom to_nat_of_one1 : forall (b:bv1) (i:Z) (j:Z), (((j < 64%Z)%Z /\
  (i <= j)%Z) /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\
  (i <= k)%Z) -> ((nth1 b k) = true)) -> ((to_nat_sub1 b j
  i) = ((pow2 ((j - i)%Z + 1%Z)%Z) - 1%Z)%Z)).

Axiom to_nat_sub_footprint1 : forall (b1:bv1) (b2:bv1) (j:Z) (i:Z),
  ((j < 64%Z)%Z /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((i <= k)%Z /\
  (k <= j)%Z) -> ((nth1 b1 k) = (nth1 b2 k))) -> ((to_nat_sub1 b1 j
  i) = (to_nat_sub1 b2 j i))).

Parameter from_int1: Z -> bv1.

Axiom nth_from_int_high_even1 : forall (n:Z) (i:Z), (((i < 64%Z)%Z /\
  (0%Z <= i)%Z) /\ ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n
  (pow2 i)) 2%Z) = 0%Z)) -> ((nth1 (from_int1 n) i) = false).

Axiom nth_from_int_high_odd1 : forall (n:Z) (i:Z), (((i < 64%Z)%Z /\
  (0%Z <= i)%Z) /\
  ~ ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n (pow2 i))
  2%Z) = 0%Z)) -> ((nth1 (from_int1 n) i) = true).

Axiom nth_from_int_low_even1 : forall (n:Z), ((int.EuclideanDivision.mod1 n
  2%Z) = 0%Z) -> ((nth1 (from_int1 n) 0%Z) = false).

Axiom nth_from_int_low_odd1 : forall (n:Z), (~ ((int.EuclideanDivision.mod1 n
  2%Z) = 0%Z)) -> ((nth1 (from_int1 n) 0%Z) = true).

Axiom nth_from_int_01 : forall (i:Z), ((i < 64%Z)%Z /\ (0%Z <= i)%Z) ->
  ((nth1 (from_int1 0%Z) i) = false).

Parameter from_int2c1: Z -> bv1.

Axiom nth_sign_positive1 : forall (n:Z), (0%Z <= n)%Z ->
  ((nth1 (from_int2c1 n) (64%Z - 1%Z)%Z) = false).

Axiom nth_sign_negative1 : forall (n:Z), (n < 0%Z)%Z ->
  ((nth1 (from_int2c1 n) (64%Z - 1%Z)%Z) = true).

Axiom nth_from_int2c_high_even1 : forall (n:Z) (i:Z),
  (((i < (64%Z - 1%Z)%Z)%Z /\ (0%Z <= i)%Z) /\
  ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n (pow2 i))
  2%Z) = 0%Z)) -> ((nth1 (from_int2c1 n) i) = false).

Axiom nth_from_int2c_high_odd1 : forall (n:Z) (i:Z),
  (((i < (64%Z - 1%Z)%Z)%Z /\ (0%Z <= i)%Z) /\
  ~ ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n (pow2 i))
  2%Z) = 0%Z)) -> ((nth1 (from_int2c1 n) i) = true).

Axiom nth_from_int2c_low_even1 : forall (n:Z), ((int.EuclideanDivision.mod1 n
  2%Z) = 0%Z) -> ((nth1 (from_int2c1 n) 0%Z) = false).

Axiom nth_from_int2c_low_odd1 : forall (n:Z),
  (~ ((int.EuclideanDivision.mod1 n 2%Z) = 0%Z)) -> ((nth1 (from_int2c1 n)
  0%Z) = true).

Axiom nth_from_int2c_01 : forall (i:Z), ((i < 64%Z)%Z /\ (0%Z <= i)%Z) ->
  ((nth1 (from_int2c1 0%Z) i) = false).

Axiom nth_from_int2c_plus_pow21 : forall (x:Z) (k:Z) (i:Z), (((0%Z <= k)%Z /\
  (k < i)%Z) /\ (k < (64%Z - 1%Z)%Z)%Z) ->
  ((nth1 (from_int2c1 (x + (pow2 i))%Z) k) = (nth1 (from_int2c1 x) k)).

Parameter concat: bv -> bv -> bv1.

Axiom concat_low : forall (b1:bv) (b2:bv), forall (i:Z), ((0%Z <= i)%Z /\
  (i < 32%Z)%Z) -> ((nth1 (concat b1 b2) i) = (nth b2 i)).

Axiom concat_high : forall (b1:bv) (b2:bv), forall (i:Z), ((32%Z <= i)%Z /\
  (i < 64%Z)%Z) -> ((nth1 (concat b1 b2) i) = (nth b1 (i - 32%Z)%Z)).

Parameter double_of_bv64: bv1 -> R.

Parameter sign_value: bool -> R.

Axiom sign_value_false : ((sign_value false) = 1%R).

Axiom sign_value_true : ((sign_value true) = (-1%R)%R).

Axiom zero : forall (b:bv1), (((to_nat_sub1 b 62%Z 52%Z) = 0%Z) /\
  ((to_nat_sub1 b 51%Z 0%Z) = 0%Z)) -> ((double_of_bv64 b) = 0%R).

Axiom sign_of_double_positive : forall (b:bv1), ((nth1 b 63%Z) = false) ->
  (0%R <= (double_of_bv64 b))%R.

Axiom sign_of_double_negative : forall (b:bv1), ((nth1 b 63%Z) = true) ->
  ((double_of_bv64 b) <= 0%R)%R.

Axiom double_of_bv64_value : forall (b:bv1), ((0%Z < (to_nat_sub1 b 62%Z
  52%Z))%Z /\ ((to_nat_sub1 b 62%Z 52%Z) < 2047%Z)%Z) ->
  ((double_of_bv64 b) = (((sign_value (nth1 b 63%Z)) * (pow21 ((to_nat_sub1 b
  62%Z 52%Z) - 1023%Z)%Z))%R * (1%R + ((IZR (to_nat_sub1 b 51%Z
  0%Z)) * (pow21 (-52%Z)%Z))%R)%R)%R).

Axiom nth_j1 : forall (i:Z), ((0%Z <= i)%Z /\ (i <= 19%Z)%Z) ->
  ((nth (from_int 1127219200%Z) i) = false).

Axiom nth_j2 : forall (i:Z), ((20%Z <= i)%Z /\ (i <= 21%Z)%Z) ->
  ((nth (from_int 1127219200%Z) i) = true).

Axiom nth_j3 : forall (i:Z), ((22%Z <= i)%Z /\ (i <= 23%Z)%Z) ->
  ((nth (from_int 1127219200%Z) i) = false).

Axiom nth_j4 : forall (i:Z), ((24%Z <= i)%Z /\ (i <= 25%Z)%Z) ->
  ((nth (from_int 1127219200%Z) i) = true).

Axiom nth_j5 : forall (i:Z), ((26%Z <= i)%Z /\ (i <= 29%Z)%Z) ->
  ((nth (from_int 1127219200%Z) i) = false).

Axiom nth_j6 : ((nth (from_int 1127219200%Z) 30%Z) = true).

Axiom nth_j7 : ((nth (from_int 1127219200%Z) 31%Z) = false).

Axiom jp0_30 : forall (i:Z), ((0%Z <= i)%Z /\ (i < 30%Z)%Z) ->
  ((nth (from_int 2147483648%Z) i) = false).

Axiom nth_const1 : forall (i:Z), ((0%Z <= i)%Z /\ (i <= 30%Z)%Z) ->
  ((nth1 (concat (from_int 1127219200%Z) (from_int 2147483648%Z))
  i) = false).

Axiom nth_const2 : ((nth1 (concat (from_int 1127219200%Z)
  (from_int 2147483648%Z)) 31%Z) = true).

Axiom nth_const3 : forall (i:Z), ((32%Z <= i)%Z /\ (i <= 51%Z)%Z) ->
  ((nth1 (concat (from_int 1127219200%Z) (from_int 2147483648%Z))
  i) = false).

Axiom nth_const4 : forall (i:Z), ((52%Z <= i)%Z /\ (i <= 53%Z)%Z) ->
  ((nth1 (concat (from_int 1127219200%Z) (from_int 2147483648%Z)) i) = true).

Axiom nth_const5 : forall (i:Z), ((54%Z <= i)%Z /\ (i <= 55%Z)%Z) ->
  ((nth1 (concat (from_int 1127219200%Z) (from_int 2147483648%Z))
  i) = false).

Axiom nth_const6 : forall (i:Z), ((56%Z <= i)%Z /\ (i <= 57%Z)%Z) ->
  ((nth1 (concat (from_int 1127219200%Z) (from_int 2147483648%Z)) i) = true).

Axiom nth_const7 : forall (i:Z), ((58%Z <= i)%Z /\ (i <= 61%Z)%Z) ->
  ((nth1 (concat (from_int 1127219200%Z) (from_int 2147483648%Z))
  i) = false).

Axiom nth_const8 : ((nth1 (concat (from_int 1127219200%Z)
  (from_int 2147483648%Z)) 62%Z) = true).

Axiom nth_const9 : ((nth1 (concat (from_int 1127219200%Z)
  (from_int 2147483648%Z)) 63%Z) = false).

Axiom sign_const : ((nth1 (concat (from_int 1127219200%Z)
  (from_int 2147483648%Z)) 63%Z) = false).

Axiom exp_const : ((to_nat_sub1 (concat (from_int 1127219200%Z)
  (from_int 2147483648%Z)) 62%Z 52%Z) = 1075%Z).

Axiom to_nat_mantissa_1 : ((to_nat_sub1 (concat (from_int 1127219200%Z)
  (from_int 2147483648%Z)) 30%Z 0%Z) = 0%Z).

Axiom mantissa_const_nth2 : forall (i:Z), ((32%Z <= i)%Z /\ (i <= 51%Z)%Z) ->
  ((nth1 (concat (from_int 1127219200%Z) (from_int 2147483648%Z))
  i) = false).

Axiom mantissa_const_to_nat51 : ((to_nat_sub1 (concat (from_int 1127219200%Z)
  (from_int 2147483648%Z)) 51%Z
  0%Z) = (to_nat_sub1 (concat (from_int 1127219200%Z)
  (from_int 2147483648%Z)) 31%Z 0%Z)).

Axiom mantissa_const : ((to_nat_sub1 (concat (from_int 1127219200%Z)
  (from_int 2147483648%Z)) 51%Z 0%Z) = (pow2 31%Z)).

Axiom real1075m1023 : ((IZR (1075%Z - 1023%Z)%Z) = 52%R).

Axiom real1075m1023_2 : ((1075%R - 1023%R)%R = 52%R).

Axiom real52_a_m52 : ((((pow21 (1075%Z - 1023%Z)%Z) * (pow21 31%Z))%R * (pow21 (-52%Z)%Z))%R = (pow21 31%Z)).

Axiom const_value0 : ((double_of_bv64 (concat (from_int 1127219200%Z)
  (from_int 2147483648%Z))) = ((1%R * (pow21 (1075%Z - 1023%Z)%Z))%R * (1%R + ((pow21 31%Z) * (pow21 (-52%Z)%Z))%R)%R)%R).

Axiom const_value : ((double_of_bv64 (concat (from_int 1127219200%Z)
  (from_int 2147483648%Z))) = ((pow21 52%Z) + (pow21 31%Z))%R).

(* Why3 assumption *)
Definition jpxor (i:Z): bv := (bw_xor (from_int 2147483648%Z)
  (from_int2c i)).

(* Why3 assumption *)
Definition var (i:Z): bv1 := (concat (from_int 1127219200%Z) (jpxor i)).

(* Why3 assumption *)
Definition var_as_double (x:Z): R := (double_of_bv64 (var x)).

(* Why3 assumption *)
Definition is_int32 (x:Z): Prop := ((-(pow2 31%Z))%Z <= x)%Z /\
  (x < (pow2 31%Z))%Z.

Axiom nth_0_30 : forall (x:Z), forall (i:Z), ((is_int32 x) /\
  ((0%Z <= i)%Z /\ (i <= 30%Z)%Z)) -> ((nth (bw_xor (from_int 2147483648%Z)
  (from_int2c x)) i) = (nth (from_int2c x) i)).

Axiom nth_jpxor_0_30 : forall (x:Z), forall (i:Z), ((is_int32 x) /\
  ((0%Z <= i)%Z /\ (i <= 30%Z)%Z)) -> ((nth (jpxor x)
  i) = (nth (from_int2c x) i)).

Axiom nth_var31 : forall (x:Z), ((nth (jpxor x)
  31%Z) = (negb (nth (from_int2c x) 31%Z))).

Axiom to_nat_sub_0_30 : forall (x:Z), (is_int32 x) ->
  ((to_nat_sub (bw_xor (from_int 2147483648%Z) (from_int2c x)) 30%Z
  0%Z) = (to_nat_sub (from_int2c x) 30%Z 0%Z)).

Axiom jpxorx_pos : forall (x:Z), (0%Z <= x)%Z ->
  ((nth (bw_xor (from_int 2147483648%Z) (from_int2c x)) 31%Z) = true).

Axiom from_int2c_to_nat_sub_pos : forall (i:Z), ((0%Z <= i)%Z /\
  (i <= 31%Z)%Z) -> forall (x:Z), ((0%Z <= x)%Z /\ (x < (pow2 i))%Z) ->
  ((to_nat_sub (from_int2c x) (i - 1%Z)%Z 0%Z) = x).

Axiom lemma1_pos : forall (x:Z), ((is_int32 x) /\ (0%Z <= x)%Z) ->
  ((to_nat_sub (jpxor x) 31%Z 0%Z) = ((pow2 31%Z) + x)%Z).

Axiom jpxorx_neg : forall (x:Z), (x < 0%Z)%Z ->
  ((nth (bw_xor (from_int 2147483648%Z) (from_int2c x)) 31%Z) = false).

Axiom from_int2c_to_nat_sub_neg : forall (i:Z), ((0%Z <= i)%Z /\
  (i <= 31%Z)%Z) -> forall (x:Z), (((-(pow2 i))%Z <= x)%Z /\ (x < 0%Z)%Z) ->
  ((to_nat_sub (from_int2c x) (i - 1%Z)%Z 0%Z) = ((pow2 i) + x)%Z).

Axiom lemma1_neg : forall (x:Z), ((is_int32 x) /\ (x < 0%Z)%Z) ->
  ((to_nat_sub (jpxor x) 31%Z 0%Z) = ((pow2 31%Z) + x)%Z).

Axiom lemma1 : forall (x:Z), (is_int32 x) -> ((to_nat_sub (jpxor x) 31%Z
  0%Z) = ((pow2 31%Z) + x)%Z).

Axiom nth_var_0_31 : forall (x:Z), forall (i:Z), ((is_int32 x) /\
  ((0%Z <= i)%Z /\ (i <= 31%Z)%Z)) -> ((nth1 (var x) i) = (nth (jpxor x) i)).

Open Scope Z_scope.
Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 10.

(* Why3 goal *)
Theorem to_nat_bv32_bv64_aux : forall (b1:bv), forall (b2:bv), forall (j:Z),
  ((0%Z <= j)%Z /\ (j < 32%Z)%Z) -> ((to_nat_sub1 (concat b1 b2) j
  0%Z) = (to_nat_sub b2 j 0%Z)).
(* Why3 intros b1 b2 j (h1,h2). *)
intros b1  b2 j (h1 & h2).
generalize h1 h2.
pattern j; apply Z_lt_induction; auto.
clear j h1 h2.
intros j Hind h1 h2.
assert (h:j = 0 \/ j > 0) by omega.
destruct h.
ae.

assert (h:(nth1 (concat b1 b2) j = nth b2 j)).
apply concat_low;auto with zarith.

assert (h3:(nth1 (concat b1 b2) j) = true \/ (nth1 (concat b1 b2) j) = false).
destruct (nth1 (concat b1 b2) j);auto.
destruct h3.
rewrite to_nat_sub_one1;auto with zarith.
ae.

rewrite to_nat_sub_zero1;auto with zarith.
ae.

Qed.

author: kit-ty-kate


text:
Require Import List.
Require Import ZArith.
Require Import Lia.
Require Import Utils.
Require Import Instr.
Set Implicit Arguments.
Local Open Scope Z_scope.

(** Basic definitions for the concrete machine.

The concrete machine is very similar to the 2 other machines, but uses
integer tags on its atoms instead of elements drawn from some abstract
lattice. Special kernel code takes care of managing those tags through
a cache, unlike in the other machines, where the label management is
built into the semantics. *)

Section CMach.

(** Stack elements of the concrete machine are mostly the same as
before, but add a field on return frames to record whether a call was
made in kernel mode or user mode. *)

Inductive CStkElmt :=
| CData : @Atom Z -> CStkElmt
| CRet : @Atom Z -> bool -> bool -> CStkElmt.

(** The state of the concrete machine, [CS], adds three fields to the
state of the abstract machine: the kernel memory ([cache]), which
contains the cache, the kernel code ([fhdl], for fault handler), and
[priv], which signals the current operation mode (user or kernel). *)

Record CS  := CState {
  cache: list (@Atom Z);
  mem : list (@Atom Z);
  fhdl:  list Instr;
  imem : list Instr;
  stk : list CStkElmt;
  pc : @Atom Z;
  priv : bool
}.

Inductive CEvent :=
| CEInt : @Atom Z -> CEvent.

(** An encoding of opcodes as integers *)

Definition opCodeToZ (opcode : OpCode) : Z :=
match opcode with
| OpNoop     => 0
| OpAdd      => 1
| OpSub      => 2
| OpPush     => 3
| OpPop      => 4
| OpLoad     => 5
| OpStore    => 6
| OpJump     => 7
| OpBranchNZ => 8
| OpCall     => 9
| OpRet      => 10
| OpVRet     => 11
| OpOutput   => 12
end.

(** Any number that doesn't occur in the above list. *)

Definition invalidOpCodeZ := 13.

(** The first seven positions of the kernel memory form the tag cache.
The first five positions are checked on every instruction to see
whether a particular combination of tags on operands is allowed; this
is called the "input" part of the cache. The two remaining positions
give tags to use on results when the instruction is allowed to
execute. We list each position below:

(WARNING TO READERS: The presentation in the paper is a little
inconsistent with the presentation here: In the paper, the PC slot in
the input and output parts of the cache line come first; here, they
come last.  This would be easy but a bit tedious to fix.) *)

(* Instruction opcode *)
Definition addrOpLabel  := 0.
(* Tag on first operand *)
Definition addrTag1     := 1.
(* Tag on second operand *)
Definition addrTag2     := 2.
(* Tag on third operand *)
Definition addrTag3     := 3.
(* Tag on the PC *)
Definition addrTagPC    := 4.
(* Tag that should be put on result *)
Definition addrTagRes   := 5.
(* Tag that should be put on the next PC *)
Definition addrTagResPC := 6.

(** Special tags. [handlerTag] is the kernel tag; [dontCare] is used as
a default tag when an instruction doesn't have enough operands

These can be completely arbitrary integers,
since they will never be inspected. *)

Definition handlerTag := 42%Z.
Definition dontCare := (-1)%Z.

Section WithListNotations.

Import ListNotations.

(** Build and update a cache from its input fields, filling its output
fields with [dontCare]. NB: Ordering of parameters in memory must
match addr* definitions above. *)

Definition build_cache (opcode: Z) (tags: Z * Z * Z) (pctag:Z): list (@Atom Z) :=
let '(tag1,tag2,tag3) := tags in
[(opcode,handlerTag); (tag1,handlerTag); (tag2,handlerTag); (tag3,handlerTag);
 (pctag,handlerTag); (dontCare,handlerTag); (dontCare,handlerTag)].

Definition update_cache opcode tags pctag cache :=
  update_list_list (build_cache opcode tags pctag) cache.

End WithListNotations.

(** Tag lives at address in memory, tagged with handlerTag *)
Inductive tag_in_mem (m: list (@Atom Z)) addr tagv : Prop :=
| tim_intro : index_list_Z addr m = Some (tagv,handlerTag) ->
              tag_in_mem m addr tagv.

(** Tag lives at address in memory, tagged with anything *)
Inductive tag_in_mem' (m: list (@Atom Z)) addr tagv : Prop :=
| tim_intro' : forall t, index_list_Z addr m = Some (tagv,t) ->
               tag_in_mem' m addr tagv.

(** Tests the cache line *)
Inductive cache_hit (m: list (@Atom Z)) opcode tags pctag : Prop :=
| ch_intro: forall tag1 tag2 tag3 tagr tagrpc
                     (UNPACK : tags = (tag1,tag2,tag3))
                     (OP: tag_in_mem m addrOpLabel opcode)
                     (TAG1: tag_in_mem m addrTag1 tag1)
                     (TAG2: tag_in_mem m addrTag2 tag2)
                     (TAG3: tag_in_mem m addrTag3 tag3)
                     (TAGPC: tag_in_mem m addrTagPC pctag)
                     (TAGR: tag_in_mem' m addrTagRes tagr)
                     (TAGRPC: tag_in_mem' m addrTagResPC tagrpc),
                cache_hit m opcode tags pctag.

Lemma build_cache_hit: forall opcode tags pctag,
     cache_hit (build_cache opcode tags pctag) opcode tags pctag.
Proof.
  intros. unfold build_cache.
  destruct tags as [[tag1 tag2] tag3] eqn:?.
  econstructor; eauto;
  try unfold addrOpLabel; try unfold addrTag1; try unfold addrTag2; try unfold addrTag3;
  try unfold addrTagPC; unfold index_list_Z; econstructor; reflexivity.
Qed.

(** Reads the cache line *)
Inductive cache_hit_read (m: list (@Atom Z)) : Z -> Z -> Prop :=
| chr_uppriv: forall tagr tagrpc,
              forall (TAG_Res: tag_in_mem' m addrTagRes tagr)
                     (TAG_ResPC: tag_in_mem' m addrTagResPC tagrpc),
                cache_hit_read m tagr tagrpc.

Definition update_cache_spec_mvec (m m': list (@Atom Z)) :=
  forall addr,
    addr <> addrOpLabel ->  addr <> addrTagPC ->
    addr <> addrTag1 -> addr <> addrTag2 -> addr <> addrTag3 ->
    index_list_Z addr m = index_list_Z addr m'.

Definition update_cache_spec_rvec (m m': list (@Atom Z)) :=
  forall addr,
  addr <> addrTagRes ->
  addr <> addrTagResPC ->
  index_list_Z addr m = index_list_Z addr m'.

(** [c_pop_to_return] is analogous to [pop_to_return], used in the
abstract machine to define the semantics of the return instructions. *)

Inductive c_pop_to_return : list CStkElmt -> list CStkElmt -> Prop :=
| cptr_done: forall a b p s,
   c_pop_to_return ((CRet a b p)::s) ((CRet a b p)::s)
| cptr_pop: forall a s s',
    c_pop_to_return s s' ->
    c_pop_to_return ((CData a)::s) s'.

Lemma c_pop_to_return_ret : forall s1 s2,
  c_pop_to_return s1 s2 ->
  exists a b p s, s2 = (CRet a b p)::s.
Proof.
  induction 1; intros; simpl; eauto.
Qed.

Lemma c_pop_to_return_spec : forall s1 s2,
  c_pop_to_return s1 s2 ->
  exists dstk, exists stk a b p,
    s1 = dstk++(CRet a b p)::stk
    /\ (forall e, In e dstk -> exists a, e = CData a).
Proof.
  induction 1; intros; simpl in *.
  exists nil ; exists s ; exists a ; exists b ; exists p.
  simpl ; split ; eauto.
  intuition.

  destruct IHc_pop_to_return as [dstk [stk [a0 [b0 [p0 [Hs Hdstk]]]]]].
  subst.
  exists ((CData a)::dstk).
  exists stk ; eauto.
  exists a0 ; exists b0 ; exists p0 ; split ; eauto.
  intros. inv H0.
  eauto.
  eapply Hdstk; auto.
Qed.

Lemma c_pop_to_return_spec2: forall  s1 s2 p1 p2 b1 b2 a1 a2 dstk,
 c_pop_to_return (dstk ++ CRet a1 b1 p1 :: s2) (CRet a2 b2 p2 :: s1) ->
 (forall e, In e dstk -> exists a : @Atom Z, e = CData a) ->
 CRet a1 b1 p1 =  CRet a2 b2 p2.
Proof.
  induction dstk; intros.
  inv H. auto.
  simpl in *.
  inv H. destruct (H0 (CRet a2 b2 p2)). intuition. inv H.
  eapply IHdstk; eauto.
Qed.

Lemma c_pop_to_return_spec3: forall s1 s2 b1 b2 p1 p2 a1 a2 dstk,
 c_pop_to_return (dstk ++ CRet a1 b1 p1 :: s2) (CRet a2 b2 p2 :: s1) ->
 (forall e, In e dstk -> exists a : @Atom Z, e = CData a) ->
 s1 = s2.
Proof.
  induction dstk; intros.
  inv H. auto.
  simpl in *.
  inv H. destruct (H0 (CRet a2 b2 p2)). intuition. inv H.
  eapply IHdstk; eauto.
Qed.

Lemma c_pop_to_return_pops_data: forall cdstk a b p cs,
     (forall a : CStkElmt, In a cdstk -> exists d : Atom, a = CData d) ->
     c_pop_to_return (cdstk ++ CRet a b p :: cs) (CRet a b p :: cs).
Proof.
  induction cdstk; intros.
  simpl; auto. constructor.
  simpl. destruct a.
  constructor. eapply IHcdstk; eauto.
  intros; (eapply H ; eauto ; constructor 2; auto).
  exploit (H (CRet a b0 b1)); eauto.
  constructor; auto.
  intros [d Hcont]. inv Hcont.
Qed.

End CMach.

Notation read_m := index_list_Z.
Notation upd_m := update_list_Z.
Notation "a ::: b" := ((CData a) :: b)  (at level 60, right associativity).
Hint Constructors cache_hit cache_hit_read : core.

author: micro-policies

repo: verified-ifc


text:
Require Import Undecidability.Shared.Libs.PSL.Base Undecidability.Shared.Libs.PSL.FiniteTypes Undecidability.TM.Util.Prelim.
Require Import Undecidability.Shared.Libs.PSL.Vectors.Vectors.

(* * Relations *)

Definition Rel (X : Type) (Y : Type) := X -> Y -> Prop.

Definition rcomp X Y Z (R : Rel X Y) (S : Rel Y Z) : Rel X Z :=
  fun x z => exists y, R x y /\ S y z.
Notation "R1 '∘' R2" := (rcomp R1 R2) (at level 40, left associativity).
Arguments rcomp {X Y Z} (R S) x y /.

Definition runion X Y (R : Rel X Y) (S : Rel X Y) : Rel X Y := fun x y => R x y \/ S x y.
Notation "R '∪' S" := (runion R S) (at level 42).
Arguments runion { X Y } ( R S ) x y /.

Definition rintersection X Y (R : Rel X Y) (S : Rel X Y) : Rel X Y := fun x y => R x y /\ S x y.
Notation "R '∩' S" := (rintersection R S) (at level 41).
Arguments rintersection { X Y } ( R S ) x y /.

Definition rimplication X Y (R : Rel X Y) (S : Rel X Y) : Rel X Y := fun x y => R x y -> S x y.
Notation "R '⊂' S" := (rimplication R S) (at level 41).
Arguments rimplication { X Y } ( R S ) x y /.

Definition ignoreParam X Y Z (R : Rel X Z) : Rel X (Y * Z)  := fun x '(y,z) => R x z.
Arguments ignoreParam {X Y Z} ( R ) x y /.

Definition rUnion (X Y : Type) (F : Type) (R : F -> Rel X Y) : Rel X Y :=
  fun x y => exists f, R f x y.
Notation "'⋃_' f R" := (rUnion (fun f => R)) (at level 50, f at level 9, R at next level, format "'⋃_' f  R"). (* Todo: This does not work if f is higher than 9. Why? *)
Arguments rUnion { X Y F } ( R ) x y /.

Definition rIntersection (X Y : Type) (F : Type) (R : F -> Rel X Y) : Rel X Y :=
  fun x y => forall f, R f x y.
Notation "'⋂_' f R" := (rIntersection (fun f => R)) (at level 50, f at level 9, R at next level, format "'⋂_' f  R"). (* Todo: This does not work if f is higher than 9. Why? *)
Arguments rIntersection { X Y F } ( R ) x y /.

Definition surjective X Z (R : Rel X Z) :=
  forall x, exists y, R x y.

Definition functional X Z (R : Rel X Z) :=
  forall x z1 z2, R x z1 -> R x z2 -> z1 = z2.

Definition subrel X Y (R S: Rel X Y) := (forall x y, R x y -> S x y).
Notation "R1 <<=2 R2" := (subrel R1 R2) (at level 60).

Instance eqrel_pre X Y : PreOrder (subrel (X := X) (Y := Y)).
Proof. constructor; firstorder. Qed.

Fact subrel_and X Y (R1 R2 R3 : Rel X Y) :
  R1 <<=2 R3 \/ R2 <<=2 R3 -> R1 ∩ R2 <<=2 R3.
Proof. firstorder. Qed.

Fact subrel_or X Y (R1 R2 R3 : Rel X Y) :
  R1 <<=2 R3 /\ R2 <<=2 R3 -> R1 ∪ R2 <<=2 R3.
Proof. firstorder. Qed.

Fact subrel_and2 X Y (R1 R2 R3 R4 : Rel X Y) :
  R1 <<=2 R3 /\ R2 <<=2 R4 -> R1 ∩ R2 <<=2 R3 ∩ R4.
Proof. firstorder. Qed.

Fact subrel_or2 X Y (R1 R2 R3 R4 : Rel X Y) :
  R1 <<=2 R3 /\ R2 <<=2 R4 -> R1 ∪ R2 <<=2 R3 ∪ R4.
Proof. firstorder. Qed.

Definition eqrel X Y (R S: Rel X Y) := (R <<=2 S /\ S <<=2 R) .

Notation "R '=2' S"  := (eqrel R S) (at level 70).

Instance eqrel_eq X Y : Equivalence (eqrel (X := X) (Y := Y)).
Proof. constructor; firstorder. Qed.

(* ** Relational operators on labelled relations *)

(* Restrict the label of a labelled relation and return an unlabelled relation *)
Definition restrict X Y Z (R : Rel X (Y * Z)) f : Rel X Z := (fun x1 x2 => R x1 (f, x2)).
Notation "R '|_' f" := (restrict R f) (at level 30, format "R '|_' f").
Arguments restrict { X Y Z } ( R f ) x y /.

(* Introduce a label that is fixed to a value *)
Definition rfix X Y Z (R : Rel X Z) (p : Y) : Rel X (Y*Z) := (fun x '(y, z) =>
y = p /\ R x z).
Notation "R '||_' f" := (rfix R f) (at level 30, format "R '||_' f").
Arguments rfix { X Y Z } ( R p ) x y /.

(* ** Relations over Vectors *)
Export VectorNotations2.
Section Fix_X2.
  Variable X Y Z : Type.
  Variable n : nat.

  Local Notation "'V' Z" := (Vector.t Z n) (at level 10).

  Definition Eq_in (f : Fin.t n -> Prop) : Rel (V X) (V X) :=
    fun vx vy => forall i : Fin.t n, f i -> vy[@i] = vx[@i].

  Global Instance Eq_in_equivalence (f : Fin.t n -> Prop) :
    Equivalence (@Eq_in f).
  Proof.
    econstructor.
    - econstructor.
    - hnf. intros. hnf in *. intros. rewrite <- H; eauto.
    - hnf. intros. hnf in *. intros. rewrite <- H, <- H0; eauto.
  Qed.

End Fix_X2.

Arguments Eq_in { X n } P x y / : rename.

(* ** Reflexive transitive closure and relational power *)
Section Star_Pow.
  Variable X : Type.
  Variable R : Rel X X.

  Inductive pow : nat -> Rel X X :=
  | pow_0 x : pow 0 x x
  | pow_S k x y z : R x y -> pow k y z -> pow (S k) x z.

  Inductive star : Rel X X :=
  | starR x : star x x
  | starC x y z : R x y -> star y z -> star x z.

  Lemma star_trans : transitive _ star.
  Proof. induction 1; eauto using star. Qed.

  Global Instance star_preorder : PreOrder star.
  Proof. constructor. constructor. apply star_trans. Qed.

  Lemma pow_plus k1 k2 x y z :
    pow k1 x y -> pow k2 y z -> pow (k1 + k2) x z.
  Proof. induction 1; cbn; eauto using pow. Qed.

  Lemma star_pow x y :
    star x y <-> exists n, pow n x y.
  Proof.
    split.
    - induction 1; firstorder eauto using pow.
    - intros (n&H). induction H; eauto using star.
  Qed.

End Star_Pow.

author: uds-psl

repo: time-invariance-thesis-for-L


text:
Load LFindLoad.
From lfind Require Import LFind.
From adtind Require Import goal33.

Set Printing Depth 1000.
Definition lfind_eval :=
@eq.

Compute lfind_eval .

Compute lfind_eval .

Compute lfind_eval .

Compute lfind_eval .

Compute lfind_eval .

Compute lfind_eval .

Compute lfind_eval .

Compute lfind_eval .

Compute lfind_eval .

Compute lfind_eval .

Compute lfind_eval .

Compute lfind_eval .

Compute lfind_eval .

Compute lfind_eval .

Compute lfind_eval .

Compute lfind_eval .

Compute lfind_eval .

Compute lfind_eval .

Compute lfind_eval .

Compute lfind_eval .

Compute lfind_eval .

Compute lfind_eval .

author: yalhessi

repo: lemmaranker

save_path: github-repos/coq/yalhessi-lemmaranker


text:
From iris.heap_lang Require Export lang.
Set Default Proof Using "Type".
Import heap_lang.

(** We define an alternative representation of expressions in which the
embedding of values and closed expressions is explicit. By reification of
expressions into this type we can implementation substitution, closedness
checking, atomic checking, and conversion into values, by computation. *)
Module W.
Inductive expr :=
  (* Value together with the original expression *)
  | Val (v : val) (e : heap_lang.expr) (H : to_val e = Some v)
  | ClosedExpr (e : heap_lang.expr) `{!Closed [] e}
  (* Base lambda calculus *)
  | Var (x : string)
  | Rec (f x : binder) (e : expr)
  | App (e1 e2 : expr)
  (* Base types and their operations *)
  | Lit (l : base_lit)
  | UnOp (op : un_op) (e : expr)
  | BinOp (op : bin_op) (e1 e2 : expr)
  | If (e0 e1 e2 : expr)
  (* Products *)
  | Pair (e1 e2 : expr)
  | Fst (e : expr)
  | Snd (e : expr)
  (* Sums *)
  | InjL (e : expr)
  | InjR (e : expr)
  | Case (e0 : expr) (e1 : expr) (e2 : expr)
  (* Concurrency *)
  | Fork (e : expr)
  (* Heap *)
  | Alloc (e : expr)
  | Load (e : expr)
  | Store (e1 : expr) (e2 : expr)
  | CAS (e0 : expr) (e1 : expr) (e2 : expr)
  | FAA (e1 : expr) (e2 : expr).

Fixpoint to_expr (e : expr) : heap_lang.expr :=
  match e with
  | Val v e' _ => e'
  | ClosedExpr e => e
  | Var x => heap_lang.Var x
  | Rec f x e => heap_lang.Rec f x (to_expr e)
  | App e1 e2 => heap_lang.App (to_expr e1) (to_expr e2)
  | Lit l => heap_lang.Lit l
  | UnOp op e => heap_lang.UnOp op (to_expr e)
  | BinOp op e1 e2 => heap_lang.BinOp op (to_expr e1) (to_expr e2)
  | If e0 e1 e2 => heap_lang.If (to_expr e0) (to_expr e1) (to_expr e2)
  | Pair e1 e2 => heap_lang.Pair (to_expr e1) (to_expr e2)
  | Fst e => heap_lang.Fst (to_expr e)
  | Snd e => heap_lang.Snd (to_expr e)
  | InjL e => heap_lang.InjL (to_expr e)
  | InjR e => heap_lang.InjR (to_expr e)
  | Case e0 e1 e2 => heap_lang.Case (to_expr e0) (to_expr e1) (to_expr e2)
  | Fork e => heap_lang.Fork (to_expr e)
  | Alloc e => heap_lang.Alloc (to_expr e)
  | Load e => heap_lang.Load (to_expr e)
  | Store e1 e2 => heap_lang.Store (to_expr e1) (to_expr e2)
  | CAS e0 e1 e2 => heap_lang.CAS (to_expr e0) (to_expr e1) (to_expr e2)
  | FAA e1 e2 => heap_lang.FAA (to_expr e1) (to_expr e2)
  end.

Ltac of_expr e :=
  lazymatch e with
  | heap_lang.Var ?x => constr:(Var x)
  | heap_lang.Rec ?f ?x ?e => let e := of_expr e in constr:(Rec f x e)
  | heap_lang.App ?e1 ?e2 =>
     let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(App e1 e2)
  | heap_lang.Lit ?l => constr:(Lit l)
  | heap_lang.UnOp ?op ?e => let e := of_expr e in constr:(UnOp op e)
  | heap_lang.BinOp ?op ?e1 ?e2 =>
     let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(BinOp op e1 e2)
  | heap_lang.If ?e0 ?e1 ?e2 =>
     let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
     constr:(If e0 e1 e2)
  | heap_lang.Pair ?e1 ?e2 =>
     let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(Pair e1 e2)
  | heap_lang.Fst ?e => let e := of_expr e in constr:(Fst e)
  | heap_lang.Snd ?e => let e := of_expr e in constr:(Snd e)
  | heap_lang.InjL ?e => let e := of_expr e in constr:(InjL e)
  | heap_lang.InjR ?e => let e := of_expr e in constr:(InjR e)
  | heap_lang.Case ?e0 ?e1 ?e2 =>
     let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
     constr:(Case e0 e1 e2)
  | heap_lang.Fork ?e => let e := of_expr e in constr:(Fork e)
  | heap_lang.Alloc ?e => let e := of_expr e in constr:(Alloc e)
  | heap_lang.Load ?e => let e := of_expr e in constr:(Load e)
  | heap_lang.Store ?e1 ?e2 =>
     let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(Store e1 e2)
  | heap_lang.CAS ?e0 ?e1 ?e2 =>
     let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
     constr:(CAS e0 e1 e2)
  | heap_lang.FAA ?e1 ?e2 =>
     let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(FAA e1 e2)
  | to_expr ?e => e
  | of_val ?v => constr:(Val v (of_val v) (to_of_val v))
  | language.of_val ?v => constr:(Val v (of_val v) (to_of_val v))
  | _ => match goal with
         | H : to_val e = Some ?v |- _ => constr:(Val v e H)
         | H : Closed [] e |- _ => constr:(@ClosedExpr e H)
         end
  end.

Fixpoint is_closed (X : list string) (e : expr) : bool :=
  match e with
  | Val _ _ _ | ClosedExpr _ => true
  | Var x => bool_decide (x ∈ X)
  | Rec f x e => is_closed (f :b: x :b: X) e
  | Lit _ => true
  | UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e | Load e =>
     is_closed X e
  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | FAA e1 e2 =>
     is_closed X e1 && is_closed X e2
  | If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 =>
     is_closed X e0 && is_closed X e1 && is_closed X e2
  end.
Lemma is_closed_correct X e : is_closed X e → heap_lang.is_closed X (to_expr e).
Proof.
  revert X.
  induction e; naive_solver eauto using is_closed_to_val, is_closed_weaken_nil.
Qed.

(* We define [to_val (ClosedExpr _)] to be [None] since [ClosedExpr]
constructors are only generated for closed expressions of which we know nothing
about apart from being closed. Notice that the reverse implication of
[to_val_Some] thus does not hold. *)
Fixpoint to_val (e : expr) : option val :=
  match e with
  | Val v _ _ => Some v
  | Rec f x e =>
     if decide (is_closed (f :b: x :b: []) e) is left H
     then Some (@RecV f x (to_expr e) (is_closed_correct _ _ H)) else None
  | Lit l => Some (LitV l)
  | Pair e1 e2 => v1 ← to_val e1; v2 ← to_val e2; Some (PairV v1 v2)
  | InjL e => InjLV <$> to_val e
  | InjR e => InjRV <$> to_val e
  | _ => None
  end.
Lemma to_val_Some e v :
  to_val e = Some v → heap_lang.of_val v = W.to_expr e.
Proof.
  revert v. induction e; intros; simplify_option_eq; try f_equal; auto using of_to_val.
Qed.
Lemma to_val_is_Some e :
  is_Some (to_val e) → ∃ v, heap_lang.of_val v = to_expr e.
Proof. intros [v ?]; exists v; eauto using to_val_Some. Qed.

Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
  match e with
  | Val v e H => Val v e H
  | ClosedExpr e => ClosedExpr e
  | Var y => if decide (x = y) then es else Var y
  | Rec f y e =>
     Rec f y $ if decide (BNamed x ≠ f ∧ BNamed x ≠ y) then subst x es e else e
  | App e1 e2 => App (subst x es e1) (subst x es e2)
  | Lit l => Lit l
  | UnOp op e => UnOp op (subst x es e)
  | BinOp op e1 e2 => BinOp op (subst x es e1) (subst x es e2)
  | If e0 e1 e2 => If (subst x es e0) (subst x es e1) (subst x es e2)
  | Pair e1 e2 => Pair (subst x es e1) (subst x es e2)
  | Fst e => Fst (subst x es e)
  | Snd e => Snd (subst x es e)
  | InjL e => InjL (subst x es e)
  | InjR e => InjR (subst x es e)
  | Case e0 e1 e2 => Case (subst x es e0) (subst x es e1) (subst x es e2)
  | Fork e => Fork (subst x es e)
  | Alloc e => Alloc (subst x es e)
  | Load e => Load (subst x es e)
  | Store e1 e2 => Store (subst x es e1) (subst x es e2)
  | CAS e0 e1 e2 => CAS (subst x es e0) (subst x es e1) (subst x es e2)
  | FAA e1 e2 => FAA (subst x es e1) (subst x es e2)
  end.
Lemma to_expr_subst x er e :
  to_expr (subst x er e) = heap_lang.subst x (to_expr er) (to_expr e).
Proof.
  induction e; simpl; repeat case_decide;
    f_equal; eauto using subst_is_closed_nil, is_closed_to_val, eq_sym.
Qed.

Definition is_atomic (e : expr) :=
  match e with
  | Alloc e => bool_decide (is_Some (to_val e))
  | Load e => bool_decide (is_Some (to_val e))
  | Store e1 e2 => bool_decide (is_Some (to_val e1) ∧ is_Some (to_val e2))
  | CAS e0 e1 e2 =>
     bool_decide (is_Some (to_val e0) ∧ is_Some (to_val e1) ∧ is_Some (to_val e2))
  | FAA e1 e2 => bool_decide (is_Some (to_val e1) ∧ is_Some (to_val e2))
  | Fork _ => true
  (* Make "skip" atomic *)
  | App (Rec _ _ (Lit _)) (Lit _) => true
  | _ => false
  end.
Lemma is_atomic_correct s e : is_atomic e → Atomic s (to_expr e).
Proof.
  intros He. apply strongly_atomic_atomic, ectx_language_atomic.
  - intros σ e' σ' ef Hstep; simpl in *. revert Hstep.
    destruct e=> //=; repeat (simplify_eq/=; case_match=>//);
      inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto.
    unfold subst'; repeat (simplify_eq/=; case_match=>//); eauto.
  - apply ectxi_language_sub_redexes_are_values=> /= Ki e' Hfill.
    destruct e=> //; destruct Ki; repeat (simplify_eq/=; case_match=>//); try
      naive_solver eauto using as_val_is_Some, to_val_is_Some.
Qed.
End W.

Ltac solve_closed :=
  match goal with
  | |- Closed ?X ?e =>
     let e' := W.of_expr e in change (Closed X (W.to_expr e'));
     apply W.is_closed_correct; vm_compute; exact I
  end.
Hint Extern 0 (Closed _ _) => solve_closed : typeclass_instances.

Ltac solve_into_val :=
  match goal with
  | |- IntoVal ?e ?v =>
     let e' := W.of_expr e in change (of_val v = W.to_expr e');
     apply W.to_val_Some; simpl; unfold W.to_expr; reflexivity
  end.
Hint Extern 10 (IntoVal _ _) => solve_into_val : typeclass_instances.

Ltac solve_as_val :=
  match goal with
  | |- AsVal ?e =>
     let e' := W.of_expr e in change (∃ v, of_val v = W.to_expr e');
     apply W.to_val_is_Some, (bool_decide_unpack _); vm_compute; exact I
  end.
Hint Extern 10 (AsVal _) => solve_as_val : typeclass_instances.

Ltac solve_atomic :=
  match goal with
  | |- Atomic ?s ?e =>
     let e' := W.of_expr e in change (Atomic s (W.to_expr e'));
     apply W.is_atomic_correct; vm_compute; exact I
  end.
Hint Extern 10 (Atomic _ _) => solve_atomic : typeclass_instances.

(** Substitution *)
Ltac simpl_subst :=
  simpl;
  repeat match goal with
  | |- context [subst ?x ?er ?e] =>
      let er' := W.of_expr er in let e' := W.of_expr e in
      change (subst x er e) with (subst x (W.to_expr er') (W.to_expr e'));
      rewrite <-(W.to_expr_subst x); simpl (* ssr rewrite is slower *)
  end;
  unfold W.to_expr.
Arguments W.to_expr : simpl never.
Arguments subst : simpl never.

(** The tactic [reshape_expr e tac] decomposes the expression [e] into an
evaluation context [K] and a subexpression [e']. It calls the tactic [tac K e']
for each possible decomposition until [tac] succeeds. *)
Ltac reshape_val e tac :=
  let rec go e :=
  lazymatch e with
  | of_val ?v => v
  | Rec ?f ?x ?e => constr:(RecV f x e)
  | Lit ?l => constr:(LitV l)
  | Pair ?e1 ?e2 =>
    let v1 := go e1 in let v2 := go e2 in constr:(PairV v1 v2)
  | InjL ?e => let v := go e in constr:(InjLV v)
  | InjR ?e => let v := go e in constr:(InjRV v)
  end in let v := go e in tac v.

Ltac reshape_expr e tac :=
  let rec go K e :=
  match e with
  | _ => tac K e
  | App ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (AppRCtx v1 :: K) e2)
  | App ?e1 ?e2 => go (AppLCtx e2 :: K) e1
  | UnOp ?op ?e => go (UnOpCtx op :: K) e
  | BinOp ?op ?e1 ?e2 =>
     reshape_val e1 ltac:(fun v1 => go (BinOpRCtx op v1 :: K) e2)
  | BinOp ?op ?e1 ?e2 => go (BinOpLCtx op e2 :: K) e1
  | If ?e0 ?e1 ?e2 => go (IfCtx e1 e2 :: K) e0
  | Pair ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (PairRCtx v1 :: K) e2)
  | Pair ?e1 ?e2 => go (PairLCtx e2 :: K) e1
  | Fst ?e => go (FstCtx :: K) e
  | Snd ?e => go (SndCtx :: K) e
  | InjL ?e => go (InjLCtx :: K) e
  | InjR ?e => go (InjRCtx :: K) e
  | Case ?e0 ?e1 ?e2 => go (CaseCtx e1 e2 :: K) e0
  | Alloc ?e => go (AllocCtx :: K) e
  | Load ?e => go (LoadCtx :: K) e
  | Store ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (StoreRCtx v1 :: K) e2)
  | Store ?e1 ?e2 => go (StoreLCtx e2 :: K) e1
  | CAS ?e0 ?e1 ?e2 => reshape_val e0 ltac:(fun v0 => first
     [ reshape_val e1 ltac:(fun v1 => go (CasRCtx v0 v1 :: K) e2)
     | go (CasMCtx v0 e2 :: K) e1 ])
  | CAS ?e0 ?e1 ?e2 => go (CasLCtx e1 e2 :: K) e0
  | FAA ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (FaaRCtx v1 :: K) e2)
  | FAA ?e1 ?e2 => go (FaaLCtx e2 :: K) e1
  end in go (@nil ectx_item) e.

author: JasonGross

repo: iris-coq

save_path: github-repos/coq/JasonGross-iris-coq


text:
(**
SimSoC-Cert, a toolkit for generating certified processor simulators.

See the COPYRIGHTS and LICENSE files.

Formalization of the ARM architecture version 6 following the:

ARM Architecture Reference Manual, Issue I, July 2005.

Page numbers refer to ARMv6.pdf.

*)

Set Implicit Arguments.

Require Import Coqlib Util Bitvec Arm6 Integers Arm6_Message Arm6_State
  Semantics.

(****************************************************************************)
(** Functions used in the pseudocode, in alphabetical order. *)

(****************************************************************************)
(** Table A4-1 Bit mask constants (p. 227) *)

(*IMPROVE: use some hexadecimal notation instead of integers*)
Definition UnallocMask : word := repr 116456448.
Definition UserMask : word := repr 4161733120.
Definition PrivMask : word := repr 479.
Definition StateMask : word := repr 16777248.

(****************************************************************************)
(** Arithmetic_Shift_Right (p. 1121)

Performs a right shift, repeatedly inserting the original left-most
bit (the sign bit) in the vacated bit positions on the left. *)
(****************************************************************************)

Definition Arithmetic_Shift_Right := shr.

(****************************************************************************)
(** bit position of most significant '1' assuming that the argument is
not 0 (p. 175) *)
(****************************************************************************)

Fixpoint bit_position_of_most_significant_1_list (bs : list bool) : Z :=
  match bs with
    | nil => 0
    | true :: tl => Z_of_nat (length tl)
    | false :: tl => bit_position_of_most_significant_1_list tl
  end.

Definition bit_position_of_most_significant_1 (w : word) : word :=
  repr (bit_position_of_most_significant_1_list (bools_of_word w)).

(****************************************************************************)
(** BorrowFrom (p. 1123)

Returns 1 if the subtraction specified as its parameter caused a borrow
(the true result is less than 0, where the operands are treated as unsigned
integers), and returns 0 in all other cases. This delivers further
information about a subtraction which occurred earlier in the pseudo-code.
The subtraction is not repeated. *)
(****************************************************************************)

Definition BorrowFrom_sub2 (x y : word) : bool :=
  zlt (unsigned x - unsigned y) 0.

Definition BorrowFrom_sub3 (x y z : word) : bool :=
  zlt (unsigned x - unsigned y - unsigned z) 0.

(****************************************************************************)
(** CarryFrom (p. 1124)

Returns 1 if the addition specified as its parameter caused a carry
(true result is bigger than 2^32-1, where the operands are treated as
unsigned integers), and returns 0 in all other cases. This delivers
further information about an addition which occurred earlier in the
pseudo-code. The addition is not repeated. *)
(****************************************************************************)

Definition CarryFrom_add2 (x y : word) : bool :=
  zgt (unsigned x + unsigned y) max_unsigned.

Definition CarryFrom_add3 (x y z : word) : bool :=
  zgt (unsigned x + unsigned y + unsigned z) max_unsigned.

(****************************************************************************)
(** CarryFrom16 (p. 1124)

Returns 1 if the addition specified as its parameter caused a carry
(true result is bigger than 2^16−1, where the operands are treated as
unsigned integers), and returns 0 in all other cases. This delivers further
information about an addition which occurred earlier in the pseudo-code.
The addition is not repeated. *)
(****************************************************************************)

Definition CarryFrom16_add2 (x y : word) : bool :=
  zgt (unsigned x + unsigned y) (two_power_nat 16 - 1).

(****************************************************************************)
(** CarryFrom8 (UADD8, p. 383)

Not defined in the Glossary. We guess:
Returns 1 if the addition specified as its parameter caused a carry
(true result is bigger than 2^8−1, where the operands are treated as
unsigned integers), and returns 0 in all other cases. This delivers further
information about an addition which occurred earlier in the pseudo-code.
The addition is not repeated. *)
(****************************************************************************)

Definition CarryFrom8_add2 (x y : word) : bool :=
  zgt (unsigned x + unsigned y) (two_power_nat 8 - 1).

(****************************************************************************)
(** ConditionPassed (p. 1124)

Returns TRUE if the state of the N, Z, C and V flags fulfils the
condition encoded in the cond argument, and returns FALSE in all other
cases.

A3.2 The condition field (p. 111) *)
(****************************************************************************)

Definition ConditionPassed (w : word) (op : opcode) : bool :=
  match op with
    | EQ => (* Z set *) is_set Zbit w
    | NE => (* Z clear *) negb (is_set Zbit w)
    | CS => (* C set *) is_set Cbit w
    | CC => (* C clear *) negb (is_set Cbit w)
    | MI => (* N set *) is_set Cbit w
    | PL => (* N clear *) negb (is_set Cbit w)
    | VS => (* V set *) is_set Vbit w
    | VC => (* V clear *) negb (is_set Vbit w)
    | HI => (* C set and Z clear *)
      andb (is_set Cbit w) (negb (is_set Zbit w))
    | LS => (* C clear or Z set *)
      orb (negb (is_set Cbit w)) (is_set Zbit w)
    | GE => (* N set and V set, or N clear and V clear (N==V) *)
      beq (is_set Nbit w) (is_set Vbit w)
    | LT => (* N set and V clear, or N clear and V set (N!=V) *)
      negb (beq (is_set Nbit w) (is_set Vbit w))
    | GT => (* Z clear, and either N set and V set,
         or N clear and V clear (Z==0,N==V) *)
      andb (negb (is_set Zbit w)) (beq (is_set Nbit w) (is_set Vbit w))
    | LE => (* Z set, or N set and V clear, or N clear and V set
         (Z==1 or N!=V) *)
      orb (is_set Zbit w) (negb (beq (is_set Nbit w) (is_set Vbit w)))
    | AL => true
  end.

(****************************************************************************)
(** CurrentModeHasSPSR() (p. 1125)

Returns TRUE if the current processor mode is not User mode or
System mode, and returns FALSE if the current mode is User mode or
System mode. *)
(****************************************************************************)

Definition CurrentModeHasSPSR (m : proc_mode) : bool :=
  match m with
    | usr | sys => false
    | _ => true
  end.

(****************************************************************************)
(** InAPrivilegedMode() (p. 1128)

Returns TRUE if the current processor mode is not User mode,
and returns FALSE if the current mode is User mode. *)
(****************************************************************************)

Definition InAPrivilegedMode (m : proc_mode) : bool :=
  match m with
    | usr => false
    | _ => true
  end.

(****************************************************************************)
(** is even-numbered (LDRD p. 200, STRD p. 349) *)
(****************************************************************************)

Definition is_even (x : Z) : bool := zeq (Zmod x 2) 0.

(****************************************************************************)
(** Logical_Shift_Left (p. 1129)

Performs a left shift, inserting zeros in the vacated bit positions
on the right. *)
(****************************************************************************)

Definition Logical_Shift_Left := shl.

(****************************************************************************)
(** Logical_Shift_Right (p. 1129)

Performs a right shift, inserting zeros in the vacated bit
positions on the left. *)
(****************************************************************************)

Definition Logical_Shift_Right := shru.

(****************************************************************************)
(** Number_Of_Set_Bits_In (p. 1130)

Performs a population count on (counts the set bits in) the bitfield
argument. *)
(****************************************************************************)

Fixpoint Number_Of_Set_Bits_In_list (bs : list bool) : Z :=
  match bs with
    | nil => 0
    | true :: tl => 1 + Number_Of_Set_Bits_In_list tl
    | false :: tl => Number_Of_Set_Bits_In_list tl
  end.

Definition Number_Of_Set_Bits_In (w : word) : word :=
  repr (Number_Of_Set_Bits_In_list (bools_of_word w)).

(****************************************************************************)
(** OverflowFrom (p. 1131)

Returns 1 if the addition or subtraction specified as its parameter
caused a 32-bit signed overflow. Addition generates an overflow if
both operands have the same sign (bit[31]), and the sign of the result
is different to the sign of both operands. Subtraction causes an
overflow if the operands have different signs, and the first operand
and the result have different signs. This delivers further
information about an addition or subtraction which occurred earlier in
the pseudo-code. The addition or subtraction is not repeated. *)
(****************************************************************************)

Definition OverflowFrom_add2 (x y : word) : bool :=
  let r := signed x + signed y in
    zlt r min_signed || zgt r max_signed.

Definition OverflowFrom_add3 (x y z : word) : bool :=
  let r := signed x + signed y + signed z in
    zlt r min_signed || zgt r max_signed.

Definition OverflowFrom_sub2 (x y : word) : bool :=
  let r := signed x - signed y in
    zlt r min_signed || zgt r max_signed.

Definition OverflowFrom_sub3 (x y z : word) : bool :=
  let r := signed x - signed y - signed z in
    zlt r min_signed || zgt r max_signed.

(****************************************************************************)
(** Rotate_Right (p. 1132)

Performs a right rotate, where each bit that is shifted off the
right is inserted on the left. *)
(****************************************************************************)

Definition Rotate_Right := ror.

(****************************************************************************)
(** SignedDoesSat(x,n) (p. 1134)

Returns 0 if x lies inside the range of an n-bit signed integer (that is,
if –2^(n–1) ≤ x ≤ 2^(n–1) – 1), and 1 otherwise.
This operation delivers further information about a SignedSat(x, n)
operation which occurred earlier in the pseudo-code.
Any operations used to calculate x or n are not repeated. *)
(****************************************************************************)

Definition SignedDoesSatZ (x : Z) (n : nat) : bool :=
  let k := two_power_nat (n-1) in
    negb (zle (-k) x && zle x (k-1)).

Definition SignedDoesSat (x : word) (n : nat) : bool :=
  SignedDoesSatZ (signed x) n.

(****************************************************************************)
(** SignExtend(arg) (p. 1134)

Sign-extends (propagates the sign bit) its argument to 32 bits. *)
(****************************************************************************)

Definition SignExtend8 (w : word) : word := sign_ext 8 w.
Definition SignExtend16 (w : word) : word := sign_ext 16 w.

(****************************************************************************)
(** SignExtend_30 (B, BL p. 160)

Not defined in the Glossary. We guess:
Sign-extends (propagates the sign bit) its 24-bits argument to 30 bits. *)
(****************************************************************************)

Definition SignExtend_30 (w : word) : word := sign_ext 24 w.

(****************************************************************************)
(** SignedSat(x,n) (p. 1134)

Returns x saturated to the range of an n-bit signed integer. That is,
 it returns:
–2^(n–1)  if             x < –2^(n–1)
x         if –2^(n–1) <= x <= 2^(n–1)–1
2^(n–1)–1 if             x > 2^(n–1)–1 *)
(****************************************************************************)

Definition SignedSatZ (x : Z) (n : nat) : word :=
  let k := two_power_nat (n-1) in
    if zlt x (-k) then repr (-k)
      else if zle (-k) x && zle x (k-1) then repr x
        else repr (k-1).

Definition SignedSat (x : word) (n : nat) : word :=
  SignedSatZ (signed x) n.

(****************************************************************************)
(** SignedSat32_add(x,y)

Compute SignedSat(x+y,32), but without truncating the result of x+y before
calling SignedSat. *)
(****************************************************************************)

Definition SignedSat32_add (x y : word) : word :=
  SignedSatZ (signed x + signed y) 32.

(****************************************************************************)
(** SignedDoesSat32_add(x,y)

Compute SignedDoesSat(x+y,32), but without truncating the result of x+y before
calling SignedDoesSat. *)
(****************************************************************************)

Definition SignedDoesSat32_add (x y : word) : bool :=
  SignedDoesSatZ (signed x + signed y) 32.

(****************************************************************************)
(** SignedSat32_sub(x,y)

Compute SignedSat(x-y,32), but without truncating the result of x-y before
calling SignedSat. *)
(****************************************************************************)

Definition SignedSat32_sub (x y : word) : word :=
  SignedSatZ (signed x - signed y) 32.

(****************************************************************************)
(** SignedDoesSat32_sub(x,y)

Compute SignedDoesSat(x-y,32), but without truncating the result of x-y before
calling SignedDoesSat. *)
(****************************************************************************)

Definition SignedDoesSat32_sub (x y : word) : bool :=
  SignedDoesSatZ (signed x - signed y) 32.

(****************************************************************************)
(** SignedSat32_double(x)

Compute SignedSat(x*2,32), but without truncating the result of x*2 before
calling SignedSat. *)
(****************************************************************************)

Definition SignedSat32_double (x : word) : word :=
  SignedSat32_add x x.

(****************************************************************************)
(** SignedDoesSat32_double(x)

Compute SignedDoesSat(x*2,32), but without truncating the result of x*2 before
calling SignedDoesSat. *)
(****************************************************************************)

Definition SignedDoesSat32_double (x : word) : bool :=
  SignedDoesSat32_add x x.

(****************************************************************************)
(** UnSignedDoesSat(x,n) (p. 1136)

Returns 0 if x lies within the range of an n-bit unsigned integer (that is,
if 0 ≤ x < 2^n) and 1 otherwise. This operation delivers further information
about an UnsignedSat(x,n) operation that occurred earlier in the pseudo-code.
Any operations used to calculate x or n are not repeated. *)
(****************************************************************************)

Definition UnsignedDoesSat (x : word) (n : nat) : bool :=
  zgt 0 x || zge x (two_power_nat n).

(****************************************************************************)
(** UnsignedSat(x,n) (p. 1136)

Returns x saturated to the range of an n-bit unsigned integer. That is,
 it returns:
0     if      x < 0
x     if 0 <= x < 2^n
2^n–1 if      x > 2^n – 1 *)
(****************************************************************************)

Definition UnsignedSat (x : word) (n : nat) : word :=
  if lt_0 x then repr 0
    else let k := two_power_nat n in
      if zlt x k then x
      else repr (k-1).

(****************************************************************************)
(** ZeroExtend(arg) (LDRH p. 205, USAD8 p. 412, USADA8 p. 414, LDRH(1)
p. 573, LDRH(2) p. 575)

Not defined in the Glossary. We guess:
Zero-extends (propagates the zero bit) its argument to 32 bits. *)
(****************************************************************************)

Definition ZeroExtend (w : word) : word := zero_ext 32 w.

(****************************************************************************)
(****************************************************************************)

Module State.
  Definition CurrentModeHasSPSR (s : state) : bool := CurrentModeHasSPSR (mode s).

  Definition InAPrivilegedMode (s : state) : bool := InAPrivilegedMode (mode s).

  Definition ConditionPassed (s : state) (op : opcode) : bool :=
    ConditionPassed (cpsr s) op.
End State.

Module Semantics.

  Module _Arm <: PROC.
    Definition exception := exception.
    Definition instruction_set := instruction_set.
    Definition UndIns := UndIns.
    Definition PC := PC.
    Definition inst_set := inst_set.
  End _Arm.

  Module _Arm_State <: STATE _Arm.
    Definition state := state.
    Definition set_cpsr := set_cpsr.
    Definition set_cpsr_bit := set_cpsr_bit.
    Definition set_reg := set_reg.
    Definition reg_content := reg_content.
    Definition cpsr := cpsr.
    Definition add_exn := add_exn.
    Definition read := read.
    Definition address_of_current_instruction := address_of_current_instruction.
  End _Arm_State.

  Module _Arm_Message <: MESSAGE.
    Definition message := message.
    Definition ComplexSemantics := ComplexSemantics.
    Definition InvalidInstructionSet := InvalidInstructionSet.
    Definition DecodingReturnsUnpredictable := DecodingReturnsUnpredictable.
  End _Arm_Message.

  Module Export S := Semantics.Make _Arm _Arm_State _Arm_Message. (* COQFIX "The kernel does not recognize yet that a parameter can be instantiated by an inductive type." *)

  Definition if_CurrentModeHasSPSR {A} (f : exn_mode -> semfun A) : semfun A :=
    fun lb_s =>
    match mode (st lb_s) with
      | usr | sys => unpredictable EmptyMessage lb_s
      | exn em => f em lb_s
    end.

  Definition set_spsr m v := map_st (fun st => set_spsr st m v).

  Definition set_reg_mode m k v :=
    map_st (fun st => (*FIXME?*) set_reg_mode st m k v).
  Definition write a n w := map_st (fun st => write st a n w).

  Definition fExclusive f (addr : word) pid size :=
    map_st (fun st => f st addr (nat_of_Z pid)
      (nat_of_Z size)).

  Definition MarkExclusiveGlobal := fExclusive MarkExclusiveGlobal.
  Definition MarkExclusiveLocal := fExclusive MarkExclusiveLocal.
  Definition ClearExclusiveByAddress := fExclusive ClearExclusiveByAddress.

  Definition ClearExclusiveLocal pid :=
    map_st (fun st => ClearExclusiveLocal st (nat_of_Z pid)).

  Definition IsExclusiveGlobal (s : state) (addr : word) (pid : word)
    (size : nat) : bool := false.

  Definition IsExclusiveLocal (s : state) (addr : word) (pid : word)
    (size : nat) : bool := false.

  (* b true means that the last instruction executed was not a jump *)
  (* Because the PC register contains the address of the current instruction
   * plus 8 (cf A2.4.3), we add 8 to the PC if a jump occured (b false) *)
  (* The implementation assumes that the processor is in ARM mode *)
  Definition incr_PC lbs' :=
    let s := st lbs' in
    ok_semstate tt (loc lbs') (bo lbs') (_Arm_State.set_reg s PC (add (reg_content s PC) (repr (if (bo lbs') then 4 else 8)))).

  Module Decoder.

    Definition decode_cond (w : word) (inst : Type) (g : opcode -> inst) :
      @decoder_result inst :=
      match condition w with
        | Some oc => DecInst _ (g oc)
        | None => @DecUndefined_with_num inst 1
      end.

    Definition decode_cond_mode (mode : Type) (f : word -> @decoder_result mode)
      (w : word) (inst : Type) (g : mode -> opcode -> inst) :
      @decoder_result inst :=
      match condition w  return @decoder_result inst with
        | Some oc =>
          match f w return @decoder_result inst with
            | DecInst i => DecInst _ (g i oc)
            | DecError m => @DecError inst m
            | DecUnpredictable => @DecUnpredictable inst
            | DecUndefined => @DecUndefined_with_num inst 2
          end
        | None => @DecUndefined_with_num inst 3
      end.

    Definition decode_mode (mode : Type) (f : word -> decoder_result mode)
      (w : word) (inst : Type) (g : mode -> inst) :
      decoder_result inst :=
      match f w with
        | DecInst i => DecInst _ (g i)
        | DecError m => @DecError inst m
        | DecUnpredictable => @DecUnpredictable inst
        | DecUndefined => @DecUndefined_with_num inst 2
      end.

    Definition next {A} f_ko (f_ok : A) x :=
      match x with
        | Jazelle => f_ko JazelleInstructionSetNotImplemented
        | Thumb => f_ko ThumbInstructionSetNotImplemented
        | Arm => f_ok
      end.
  End Decoder.

End Semantics.

author: git-inria

repo: simsoc-cert

save_path: github-repos/coq/git-inria-simsoc-cert


text:
From Tealeaves Require Export
  Classes.Monoid
  Applicative.

Import Monoid.Notations.

#[local] Generalizable Variables W M N ϕ.

(** * Inductive definition of the constant functor *)
(******************************************************************************)
Inductive Const V (tag : Type) : Type :=
| mkConst : V -> Const V tag.

Arguments mkConst {V tag}%type_scope v : rename.

Definition unconst {V tag} : Const V tag -> V :=
  fun '(mkConst c) => c.

Lemma unconst_mkConst {V A} : forall (v : V), unconst (mkConst (tag := A) v) = v.
Proof.
  now intros.
Qed.

Lemma mkConst_unconst {V A} : forall (x : @Const V A), mkConst (unconst x) = x.
Proof.
  now intros [?].
Qed.

Definition retag {V A B} : Const V A -> Const V B :=
  mkConst ∘ unconst.

#[global] Instance Fmap_Const {V} : Fmap (Const V) :=
  fun A B f x => mkConst (unconst x).

#[global, program] Instance End_Const {V} : Functor (Const V).

Solve All Obligations with
    (intros; now ext [?]).

#[local] Hint Immediate unconst_mkConst mkConst_unconst : tea_applicative.

#[global] Hint Rewrite (@unconst_mkConst) (@mkConst_unconst) : tea_applicative.

Lemma fmap_Const_1 : forall V (A B : Type) (f : A -> B) (x : Const V A),
    unconst (fmap (Const V) f x) = unconst x.
Proof.
  introv. now destruct x.
Qed.

Definition mapConst {A B} (f : A -> B) {C} : Const A C -> Const B C :=
  fun '(mkConst a) => mkConst (f a).

Theorem mapConst_1 {A B} (f : A -> B) {C} (x : Const A C) :
  f (unconst x) = unconst (mapConst f x).
Proof.
  destruct x; cbn. reflexivity.
Qed.

Theorem mapConst_2 {A B} (f : A -> B) {C} :
  f ∘ unconst (tag := C) = unconst ∘ mapConst f.
Proof.
  ext [?]. cbn. apply mapConst_1.
Qed.

(** * Constant applicative functors *)
(******************************************************************************)
Section const_ops.

  Context
    `{Monoid M}.

  #[global] Instance Pure_Const : Pure (Const M) :=
    fun (A : Type) (a : A) => mkConst (tag := A) Ƶ.

  #[global] Instance Mult_Const : Mult (Const M) :=
    fun A B (p : Const M A * Const M B) =>
      mkConst (tag := A * B) (unconst (fst p) ● unconst (snd p)).

  #[global, program] Instance Applicative_Const `{Monoid M} : Applicative (Const M).

  Solve Obligations with
      (intros; unfold transparent tcs in *; cbn; simpl_monoid;
      now auto with tea_applicative).

End const_ops.

#[global] Instance ApplicativeMorphism_Monoid_Morphism `(f : M1 -> M2) `{Monoid_Morphism M1 M2 f} :
  ApplicativeMorphism (Const M1) (Const M2) (@mapConst M1 M2 f).
Proof.
  match goal with H : Monoid_Morphism f |- _ => inversion H end.
  constructor; try typeclasses eauto.
  - introv. destruct x. reflexivity.
  - intros. cbn. rewrite (monmor_unit). reflexivity.
  - intros. destruct x, y. cbn. rewrite (monmor_op). reflexivity.
Qed.

(** * Computational definition of the constant functor *)
(******************************************************************************)
Section constant_functor.

  Definition retag_const {A X Y : Type} :
    const A X -> const A Y := @id A.

  (** First we establish that (const M) is an applicative functor. *)
  Section with_monoid.

    Context
      `{Monoid M}.

    #[global] Instance Fmap_const : Fmap (const M) :=
      fun X Y f t => t.

    Theorem fmap_const_spec : forall (X Y : Type) (f : X -> Y),
        fmap (const M) f = id.
    Proof.
      reflexivity.
    Qed.

    #[global] Instance Pure_const : Pure (const M) :=
      fun X x => Ƶ.

    #[global] Instance Mult_const : Mult (const M) :=
      fun X Y '(x, y) => x ● y.

    #[global] Instance Applicative_const :
      Applicative (const M).
    Proof.
      constructor; intros; try reflexivity.
      - constructor; reflexivity.
      - cbn. now Monoid.simpl_monoid.
      - cbn. unfold_ops @Pure_const. now Monoid.simpl_monoid.
      - cbn. unfold_ops @Pure_const. now Monoid.simpl_monoid.
      - cbn. unfold_ops @Pure_const. now Monoid.simpl_monoid.
    Qed.

    #[global] Instance ApplicativeMorphism_unconst :
      ApplicativeMorphism (Const M) (const M)
        (fun X => unconst).
    Proof.
      constructor; try typeclasses eauto; reflexivity.
    Qed.

  End with_monoid.

  #[global] Instance ApplicativeMorphism_monoid_morphism `{hom : Monoid_Morphism ϕ (A := M) (B := N)} :
    ApplicativeMorphism (const M) (const N) (const ϕ).
  Proof.
    inversion hom.
    constructor; now try typeclasses eauto.
  Qed.

End constant_functor.

author: dunnl

repo: tealeaves

save_path: github-repos/coq/dunnl-tealeaves


text:
Require Import Coq.ZArith.BinInt.
Require Import coqutil.Z.Lia.
Require Import Coq.ZArith.ZArith.

Local Open Scope Z_scope.

Module Z.

  Lemma mod2_cases: forall (n: Z), n mod 2 = 0 \/ n mod 2 = 1.
  Proof.
    intros. pose proof (Z.mod_pos_bound n 2). blia.
  Qed.

  Lemma div_mul_undo: forall a b,
      b <> 0 ->
      a mod b = 0 ->
      a / b * b = a.
  Proof.
    intros.
    pose proof Z.div_mul_cancel_l as A. specialize (A a 1 b).
    replace (b * 1) with b in A by blia.
    rewrite Z.div_1_r in A.
    rewrite Z.mul_comm.
    rewrite <- Z.divide_div_mul_exact; try assumption.
    - apply A; congruence.
    - apply Z.mod_divide; assumption.
  Qed.

  Lemma mod_0_r: forall (m: Z),
      m mod 0 =
      ltac:(match eval hnf in (1 mod 0) with | 0 => exact 0 | _ => exact m end).
  Proof.
    intros. destruct m; reflexivity.
  Qed.

  Lemma sub_mod_0: forall (a b m: Z),
      a mod m = 0 ->
      b mod m = 0 ->
      (a - b) mod m = 0.
  Proof.
    intros *. intros E1 E2.
    rewrite Zminus_mod.
    rewrite E1. rewrite E2.
    reflexivity.
  Qed.

  Lemma add_mod_0: forall a b m : Z,
      a mod m = 0 ->
      b mod m = 0 ->
      (a + b) mod m = 0.
  Proof.
    intros *. intros E1 E2.
    rewrite Zplus_mod.
    rewrite E1. rewrite E2.
    reflexivity.
  Qed.

  Lemma Z_mod_mult': forall a b : Z,
      (a * b) mod a = 0.
  Proof.
    intros. rewrite Z.mul_comm. apply Z_mod_mult.
  Qed.

  Lemma mod_add_r: forall a b,
      b <> 0 ->
      (a + b) mod b = a mod b.
  Proof.
    intros. rewrite <- Z.add_mod_idemp_r by blia.
    rewrite Z.mod_same by blia.
    rewrite Z.add_0_r.
    reflexivity.
  Qed.

  Lemma mod_pow2_same_cases: forall a n,
      a mod 2 ^ n = a ->
      2 ^ n = 0 \/ 0 <= a < 2 ^ n.
  Proof.
    intros.
    assert (n < 0 \/ 0 <= n) as C by blia. destruct C as [C | C].
    - left. rewrite (Z.pow_neg_r 2 n C) in *. rewrite mod_0_r in H. auto.
    - right.
      rewrite <- H. apply Z.mod_pos_bound.
      apply Z.pow_pos_nonneg; blia.
  Qed.

  Lemma mod_pow2_same_bounds: forall a n,
      a mod 2 ^ n = a ->
      0 <= n ->
      0 <= a < 2 ^ n.
  Proof.
    intros. rewrite <- H. apply Z.mod_pos_bound.
    apply Z.pow_pos_nonneg; blia.
  Qed.

  Lemma pow2_nonneg: forall n,
      0 <= 2 ^ n.
  Proof.
    intros. apply Z.pow_nonneg. blia.
  Qed.

  Lemma pow2_pos: forall n,
      0 <= n ->
      0 < 2 ^ n.
  Proof.
    intros. apply Z.pow_pos_nonneg; blia.
  Qed.

  Lemma pow2_times2: forall i,
      0 < i ->
      2 ^ i = 2 * 2 ^ (i - 1).
  Proof.
    intros.
    rewrite <- Z.pow_succ_r by blia.
    f_equal.
    blia.
  Qed.

  Lemma pow2_div2: forall i,
      0 <= i ->
      2 ^ (i - 1) = 2 ^ i / 2.
  Proof.
    intros.
    assert (i = 0 \/ 0 < i) as C by blia. destruct C as [C | C].
    - subst. reflexivity.
    - rewrite Z.pow_sub_r by blia.
      reflexivity.
  Qed.

  Lemma div_mul_undo_le: forall a b,
      0 < b ->
      a / b * b <= a.
  Proof.
    intros.
    pose proof (Zmod_eq_full a b) as P.
    pose proof (Z.mod_pos_bound a b) as Q.
    blia.
  Qed.

  Lemma testbit_true_nonneg: forall a i,
      0 <= a ->
      0 <= i ->
      Z.testbit a i = true ->
      2 ^ i <= a.
  Proof.
    intros.
    apply Z.testbit_true in H1; [|assumption].
    pose proof (pow2_pos i H0).
    eapply Z.le_trans; [| apply (div_mul_undo_le a (2 ^ i)); blia].
    replace (2 ^ i) with (1 * 2 ^ i) at 1 by blia.
    apply Z.mul_le_mono_nonneg_r; [blia|].
    pose proof (Z.div_pos a (2 ^ i)).
    assert (a / 2 ^ i <> 0); [|blia].
    intro E. rewrite E in H1. cbv in H1. discriminate H1.
  Qed.

  Lemma range_div_pos: forall a b c d,
      0 < d ->
      a <= b <= c ->
      a / d <= b / d <= c / d.
  Proof.
    intuition idtac.
    - apply (Z.div_le_mono _ _ _ H H1).
    - apply (Z.div_le_mono _ _ _ H H2).
  Qed.

  Lemma testbit_true_nonneg': forall a i,
      0 <= i ->
      2 ^ i <= a < 2 ^ (i + 1) ->
      Z.testbit a i = true.
  Proof.
    intros.
    apply Z.testbit_true; [assumption|].
    destruct H0 as [A B].
    pose proof (pow2_pos i H) as Q.
    apply (Z.div_le_mono _ _ _ Q) in A.
    rewrite Z_div_same in A by blia.
    pose proof (Z.div_lt_upper_bound a (2 ^ i) 2 Q) as P.
    rewrite Z.mul_comm in P.
    replace i with (i + 1 - 1) in P by blia.
    rewrite <- pow2_times2 in P by blia.
    specialize (P B).
    replace (i + 1 - 1) with i in P by blia.
    replace (a / 2 ^ i) with 1 by blia.
    reflexivity.
  Qed.

  Lemma testbit_false_nonneg: forall a i,
      0 <= a < 2 ^ i ->
      0 < i ->
      Z.testbit a (i - 1) = false ->
      a < 2 ^ (i - 1).
  Proof.
    intros.
    assert (2 ^ (i - 1) <= a < 2 ^ i \/ a < 2 ^ (i - 1)) as C by blia.
    destruct C as [C | C]; [exfalso|assumption].
    assert (Z.testbit a (i - 1) = true); [|congruence].
    replace i with (i - 1 + 1) in C at 2 by blia.
    apply testbit_true_nonneg'; blia.
  Qed.

  Lemma testbit_minus1 i (H:0<=i) : Z.testbit (-1) i = true.
  Proof. destruct i; try blia; exact eq_refl. Qed.

  Lemma testbit_mod_pow2 a n i (H:0<=n)
    : Z.testbit (a mod 2 ^ n) i = ((i <? n) && Z.testbit a i)%bool.
  Proof.
    destruct (Z.ltb_spec i n); rewrite
      ?Z.mod_pow2_bits_low, ?Z.mod_pow2_bits_high by auto; auto.
  Qed.

  Lemma testbit_ones n i (H : 0 <= n) : Z.testbit (Z.ones n) i = ((0 <=? i) && (i <? n))%bool.
  Proof.
    destruct (Z.leb_spec 0 i), (Z.ltb_spec i n); cbn;
      rewrite ?Z.testbit_neg_r, ?Z.ones_spec_low, ?Z.ones_spec_high by blia; trivial.
  Qed.

  Lemma testbit_ones_nonneg n i (Hn : 0 <= n) (Hi: 0 <= i) : Z.testbit (Z.ones n) i = (i <? n)%bool.
  Proof.
    rewrite testbit_ones by blia.
    destruct (Z.leb_spec 0 i); cbn; solve [trivial | blia].
  Qed.

  Lemma shiftl_minus_one_neg: forall n,
      n <= 0 -> Z.shiftl (-1) n = -1.
  Proof.
    unfold Z.shiftl. intros. destruct n; try Lia.lia. clear H.
    induction p; cbn; rewrite ?IHp; try reflexivity.
  Qed.

  Lemma signed_bounds_to_sz_pos: forall sz n,
      - 2 ^ (sz - 1) <= n < 2 ^ (sz - 1) ->
      0 < sz.
  Proof.
    intros.
    assert (0 < sz \/ sz - 1 < 0) as C by blia.
    destruct C as [C | C]; [assumption|exfalso].
    rewrite Z.pow_neg_r in H by assumption.
    blia.
  Qed.

  Lemma two_digits_encoding_inj_lo: forall base a b c d: Z,
      0 <= b < base ->
      0 <= d < base ->
      base * a + b = base * c + d ->
      b = d.
  Proof.
    intros.
    pose proof Z.mod_unique as P.
    specialize P with (b := base) (q := c) (r := d).
    specialize P with (2 := H1).
    rewrite P by blia.
    rewrite <- Z.add_mod_idemp_l by blia.
    rewrite Z.mul_comm.
    rewrite Z.mod_mul by blia.
    rewrite Z.add_0_l.
    rewrite Z.mod_small by blia.
    reflexivity.
  Qed.

  Lemma two_digits_encoding_inj_hi: forall base a b c d: Z,
      0 <= b < base ->
      0 <= d < base ->
      base * a + b = base * c + d ->
      a = c.
  Proof.
    intros. Lia.nia.
  Qed.

  Lemma Z_to_nat_neg: forall (n: Z),
      n < 0 ->
      Z.to_nat n = 0%nat.
  Proof.
    intros. destruct n; (blia || apply Z2Nat.inj_neg).
  Qed.

  (* Create HintDb z_bitwise discriminated. *) (* DON'T do this, COQBUG(5381) *)
  #[global] Hint Rewrite
       Z.shiftl_spec_low Z.lxor_spec Z.lor_spec Z.land_spec Z.lnot_spec Z.ldiff_spec Z.shiftl_spec Z.shiftr_spec Z.ones_spec_high Z.shiftl_spec_alt Z.ones_spec_low Z.shiftr_spec_aux Z.shiftl_spec_high Z.ones_spec_iff Z.testbit_spec
       Z.div_pow2_bits Z.pow2_bits_eqb Z.bits_opp Z.testbit_0_l
       Z.testbit_mod_pow2 Z.testbit_ones_nonneg Z.testbit_minus1
       using solve [auto with zarith] : z_bitwise.
  #[global] Hint Rewrite <-Z.ones_equiv
       using solve [auto with zarith] : z_bitwise.

End Z.

author: mit-plv

repo: coqutil

save_path: github-repos/coq/mit-plv-coqutil


text:
Require Coq.Classes.EquivDec.
Require Coq.Lists.List.
Import List.ListNotations.
Require Import Coq.Program.Program.

Require Import Leapfrog.Syntax.
Require Import Leapfrog.FinType.
Require Import Leapfrog.Sum.
Require Import Leapfrog.Syntax.
Require Import Leapfrog.Notations.
Require Import Leapfrog.BisimChecker.

Open Scope p4a.

Module Reference.
  Inductive state: Set :=
  | SPref
  | SDest
  | SSrc
  | SProto.

  Scheme Equality for state.
  Global Instance state_eqdec: EquivDec.EqDec state eq := state_eq_dec.
  Global Instance state_finite: @Finite state _ state_eq_dec.
  Proof.
    solve_finiteness.
  Defined.

  Inductive header :=
  | HPref
  | HDest
  | HSrc
  | HProto.

  Definition sz (h: header): nat :=
    match h with
    | HPref => 64
    | HDest => 48
    | HSrc => 48
    | HProto => 16
    end.

  Scheme Equality for header.
  Global Instance header_eqdec: EquivDec.EqDec header eq := header_eq_dec.
  Global Instance header_finite: @Finite header _ header_eq_dec.
  Proof.
    solve_finiteness.
  Defined.

  Definition states (s: state) : Syntax.state state sz :=
    match s with
    | SPref => {| st_op := extract(HPref);
                  st_trans := transition (inl SDest) |}
    | SDest => {| st_op := extract(HDest);
                  st_trans := transition (inl SSrc) |}
    | SSrc => {| st_op := extract(HSrc);
                  st_trans := transition (inl SProto) |}
    | SProto => {| st_op := extract(HProto);
                  st_trans := transition select (| EHdr HProto |) {{
                    [| exact #b|1|0|0|0|0|0|0|0|0|0|0|0|0|0|0|0 |] ==> accept ;;;
                      reject
                  }}
                |}
    end.

  Program Definition aut: Syntax.t state sz :=
    {| t_states := states |}.
  Solve Obligations with (destruct s || destruct h; cbv; Lia.lia).

End Reference.

Module Combined.
  Inductive state :=
  | Parse.

  Equations state_eq_dec (h1 h2: state) : {h1 = h2} + {h1 <> h2} :=
  { state_eq_dec Parse Parse := left eq_refl }.
  Global Instance state_eqdec: EquivDec.EqDec state eq := state_eq_dec.
  Global Instance state_finite: @Finite state _ state_eq_dec.
  Proof.
    solve_finiteness.
  Defined.

  Inductive header :=
  | HdrVar.

  Equations header_eq_dec (h1 h2: header) : {h1 = h2} + {h1 <> h2} :=
  { header_eq_dec HdrVar HdrVar := left eq_refl }.
  Global Instance header_eqdec: EquivDec.EqDec header eq := header_eq_dec.
  Global Instance header_finite: @Finite header _ header_eq_dec.
  Proof.
    solve_finiteness.
  Defined.

  Definition sz (h: header): nat :=
    match h with
    | HdrVar => 176
    end.

  Definition states (s: state) : Syntax.state state sz :=
    match s with
    | Parse =>
      {| st_op := extract(HdrVar);
        st_trans := transition select (| (EHdr (Hdr_sz := sz) HdrVar)[176 -- 160] |) {{
          [| exact #b|1|0|0|0|0|0|0|0|0|0|0|0|0|0|0|0 |] ==> accept ;;;
            @reject state
        }}
      |}
    end.

  Program Definition aut: Syntax.t state sz :=
    {| t_states := states |}.
  Solve Obligations with (destruct s || destruct h; cbv; Lia.lia).

End Combined.

Module RefComb.
  Definition aut := sum Reference.aut Combined.aut.
End RefComb.

author: verified-network-toolchain

repo: leapfrog


text:
From iris.algebra Require Import frac.
From iris.proofmode Require Import proofmode.
From cap_machine Require Import logrel addr_reg_sample fundamental rules proofmode.

(* Assert routine *)

(* Maintains a flag storing whether an assert has failed. *)

Section Assert.
  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ}
          {nainv: logrel_na_invs Σ}
          `{MP: MachineParameters}.

  (* assert (r4 == r5) *)
  Definition assert_subroutine_instrs :=
    encodeInstrsW [
      Sub r_t4 r_t4 r_t5;
      Mov r_t5 PC;
      Lea r_t5 6;
      Jnz r_t5 r_t4;
      (* success case *)
      Mov r_t4 0;
      Mov r_t5 0;
      Jmp r_t0; (* return *)
      (* failure case *)
      Lea r_t5 6; (* pointer to cap: *)
      Load r_t5 r_t5;
      Store r_t5 1;
      Mov r_t4 0;
      Mov r_t5 0;
      Jmp r_t0 (* return *)
    ].
  (* followed in memory by:
    cap: (RW, flag, end, flag)
    flag: <0 or 1>
    end:
  *)

  Definition assert_inv (b a_flag e : Addr) : iProp Σ :=
    (∃ cap_addr,
       codefrag b assert_subroutine_instrs ∗
       ⌜(b + length assert_subroutine_instrs)%a = Some cap_addr⌝ ∗
       ⌜(cap_addr + 1)%a = Some a_flag⌝ ∗
       ⌜(a_flag + 1)%a = Some e⌝ ∗
       cap_addr ↦ₐ WCap RW a_flag e a_flag).

  Lemma assert_subroutine_spec b a_flag e cont n1 n2 flag N E φ :
    ↑N ⊆ E →
    (  na_inv logrel_nais N (assert_inv b a_flag e)
     ∗ na_own logrel_nais E
     ∗ PC ↦ᵣ WCap RX b e b
     ∗ r_t0 ↦ᵣ cont
     ∗ r_t4 ↦ᵣ WInt n1
     ∗ r_t5 ↦ᵣ WInt n2
     ∗ a_flag ↦ₐ WInt flag
     ∗ ▷ (na_own logrel_nais E
          ∗ PC ↦ᵣ updatePcPerm cont
          ∗ r_t0 ↦ᵣ cont
          ∗ r_t4 ↦ᵣ WInt 0
          ∗ r_t5 ↦ᵣ WInt 0
          ∗ a_flag ↦ₐ WInt (if (n1 =? n2)%Z then flag else 1%Z)
          -∗ WP Seq (Instr Executable) {{ φ }})
     ⊢ WP Seq (Instr Executable) {{ φ }})%I.
  Proof.
    iIntros (HNE) "(#Hinv & Hna & HPC & Hr0 & Hr1 & Hr2 & Hflag & Hφ)".
    iMod (na_inv_acc with "Hinv Hna") as "(>Hassert & Hna & Hinv_close)"; auto.
    iDestruct "Hassert" as (cap_addr) "(Hprog & %Hcap & %Hflag & %He & Hcap)".
    rewrite /assert_subroutine_instrs. codefrag_facts "Hprog".
    assert (SubBounds b e b (b ^+ length assert_subroutine_instrs)%a) by solve_addr.
    do 3 iInstr "Hprog".
    destruct (decide (n1 = n2)).
    { (* n1 = n2 *)
      subst n2. rewrite (_: n1 - n1 = 0)%Z; last lia.
      iGo "Hprog".
      iMod ("Hinv_close" with "[Hprog Hcap $Hna]") as "Hna".
      { iExists _. iNext. iFrame. iPureIntro. repeat split; solve_addr. }
      iApply "Hφ". iFrame. rewrite Z.eqb_refl //. }
    { (* n1 ≠ n2 *)
      iInstr "Hprog". { assert (n1 - n2 ≠ 0)%Z by lia. congruence. }
      iInstr "Hprog". rewrite (_: (b ^+ 13)%a = cap_addr). 2: solve_addr.
      iInstr "Hprog". solve_addr.
      iInstr "Hprog". solve_addr.
      iGo "Hprog".
      iMod ("Hinv_close" with "[Hprog Hcap $Hna]") as "Hna".
      { iExists _. iNext. iFrame. iPureIntro. repeat split; solve_addr. }
      iApply "Hφ". iFrame. rewrite (_: (n1 =? n2)%Z = false) //.
      by apply Z.eqb_neq. }
  Qed.

  Lemma assert_success_spec b a_flag e cont n1 n2 N E φ :
    ↑N ⊆ E →
    n1 = n2 →
    (  na_inv logrel_nais N (assert_inv b a_flag e)
     ∗ na_own logrel_nais E
     ∗ PC ↦ᵣ WCap RX b e b
     ∗ r_t0 ↦ᵣ cont
     ∗ r_t4 ↦ᵣ WInt n1
     ∗ r_t5 ↦ᵣ WInt n2
     ∗ ▷ (na_own logrel_nais E
          ∗ PC ↦ᵣ updatePcPerm cont
          ∗ r_t0 ↦ᵣ cont
          ∗ r_t4 ↦ᵣ WInt 0
          ∗ r_t5 ↦ᵣ WInt 0
          -∗ WP Seq (Instr Executable) {{ φ }})
     ⊢ WP Seq (Instr Executable) {{ φ }})%I.
  Proof.
    iIntros (HNE Heq) "(#Hinv & Hna & HPC & Hr0 & Hr1 & Hr2 & Hφ)".
    iMod (na_inv_acc with "Hinv Hna") as "(>Hassert & Hna & Hinv_close)"; auto.
    iDestruct "Hassert" as (cap_addr) "(Hprog & %Hcap & %Hflag & %He & Hcap)".
    rewrite /assert_subroutine_instrs. codefrag_facts "Hprog".
    assert (SubBounds b e b (b ^+ length assert_subroutine_instrs)%a) by solve_addr.
    do 3 iInstr "Hprog". rewrite (_: n1 - n2 = 0)%Z; last lia.
    iGo "Hprog".
    iMod ("Hinv_close" with "[Hprog Hcap $Hna]") as "Hna".
    { iExists _. iNext. iFrame. iPureIntro. repeat split; solve_addr. }
    iApply "Hφ". iFrame.
  Qed.

End Assert.

author: logsem

repo: cerise

save_path: github-repos/coq/logsem-cerise


text:
From Coq Require Import String List ZArith.
From compcert Require Import Coqlib Integers Floats Values AST Ctypes Cop Csyntax.
From ch2o_compcert Require Import Csyntaxdefs.
Import Csyntaxdefs.CsyntaxNotations.
Local Open Scope Z_scope.
Local Open Scope string_scope.
Local Open Scope csyntax_scope.

Module Info.
  Definition version := "3.9".
  Definition build_number := "".
  Definition build_tag := "".
  Definition build_branch := "".
  Definition arch := "x86".
  Definition model := "64".
  Definition abi := "macos".
  Definition bitsize := 64.
  Definition big_endian := false.
  Definition source_file := "locals_example.c".
End Info.

Definition _main : ident := $"main".
Definition _x : ident := $"x".
Definition _y : ident := $"y".
Definition _z : ident := $"z".

Definition f_main := {|
  fn_return := tint;
  fn_callconv := cc_default;
  fn_params := nil;
  fn_vars := ((_x, tint) :: (_y, tint) :: (_z, tint) :: nil);
  fn_body :=
(Ssequence
  (Ssequence
    (Sdo (Eassign (Evar _x tint)
           (Ebinop Odiv (Eval (Vint (Int.repr 17)) tint)
             (Eval (Vint (Int.repr 2)) tint) tint) tint))
    (Ssequence
      (Sdo (Eassign (Evar _y tint)
             (Ebinop Odiv (Eval (Vint (Int.repr 15)) tint)
               (Eval (Vint (Int.repr 5)) tint) tint) tint))
      (Ssequence
        (Sdo (Eassign (Evar _z tint)
               (Ebinop Odiv (Evalof (Evar _x tint) tint)
                 (Evalof (Evar _y tint) tint) tint) tint))
        (Sreturn (Some (Evalof (Evar _z tint) tint))))))
  (Sreturn (Some (Eval (Vint (Int.repr 0)) tint))))
|}.

Definition composites : list composite_definition :=
nil.

Definition global_definitions : list (ident * globdef fundef type) :=
((_main, Gfun(Internal f_main)) :: nil).

Definition public_idents : list ident :=
(_main :: nil).

Definition prog : Csyntax.program :=
  mkprogram composites global_definitions public_idents _main Logic.I.

author: btj