Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / optim / oversampling / out / typed / f_step_assert_5_Coq.v @ 6a93d814

History | View | Annotate | Download (2.83 KB)

1
(* ---------------------------------------------------------- *)
2
(* --- Assertion (file oversampling0_4.c, line 173)       --- *)
3
(* ---------------------------------------------------------- *)
4
Require Import ZArith.
5
Require Import Reals.
6
Require Import BuiltIn.
7
Require Import bool.Bool.
8
Require Import int.Int.
9
Require Import int.Abs.
10
Require Import int.ComputerDivision.
11
Require Import real.Real.
12
Require Import real.RealInfix.
13
Require Import real.FromInt.
14
Require Import map.Map.
15
Require Import Qedlib.
16
Require Import Qed.
17

    
18
Require Import S_f_mem_pack.
19
Require Import Memory.
20
Require Import Cint.
21
Require Import Compound.
22
Require Import Axiomatic.
23

    
24
Goal
25
  forall (i_1 i : Z),
26
  forall (t : array Z),
27
  forall (t_2 t_1 : farray addr Z),
28
  forall (t_3 : farray addr addr),
29
  forall (a_2 a_1 a : addr),
30
  forall (f_1 f : S_f_mem_pack),
31
  let a_3 := t_3.[ (shiftfield_F_f_mem_ni_2 a_2) ] in
32
  let x := (1%Z + i%Z)%Z in
33
  let m := t_1.[ a <- x ] in
34
  let x_1 := (1%Z + i_1%Z)%Z in
35
  let m_1 := t_2.[ a_1 <- x_1 ] in
36
  let a_4 := (shiftfield_F__arrow_reg__first
37
               ((shiftfield_F__arrow_mem__reg a_3))) in
38
  let x_2 := (m_1.[ a_4 ])%Z in
39
  let x_3 := (t_1.[ a_1 ])%Z in
40
  (a <> a_1) ->
41
  ((IsS_f_mem_pack f)) ->
42
  ((IsS_f_mem_pack f_1)) ->
43
  ((framed t_3)) ->
44
  ((linked t)) ->
45
  ((is_sint32 i%Z)) ->
46
  ((is_sint32 i_1%Z)) ->
47
  (a <> a_3) ->
48
  (a_1 <> a_3) ->
49
  ((valid_rw t a 1%Z)) ->
50
  ((valid_rw t a_1 1%Z)) ->
51
  ((P_valid_f t t_3 a_2)) ->
52
  ((((region ((base a))%Z)) <= 0)%Z) ->
53
  ((((region ((base a_1))%Z)) <= 0)%Z) ->
54
  ((((region ((base a_2))%Z)) <= 0)%Z) ->
55
  ((separated a_2 2%Z a 1%Z)) ->
56
  ((separated a_2 2%Z a_1 1%Z)) ->
57
  ((P_f_pack2 t_3 t_2 f_1 a_2)) ->
58
  ((separated a_2 2%Z a_3 1%Z)) ->
59
  ((P_f_pack1 t_3 m f a_2)) ->
60
  ((is_uint32 x_2)) ->
61
  (itep ((0 = x_2)%Z) (t_1 = m_1) (t_1 = (m_1.[ a_4 <- (0)%Z ]))) ->
62
  (itep ((0 = x_2)%Z)
63
   ((i
64
     = (t_1.[ (shiftfield_F_f_reg___f_2 ((shiftfield_F_f_mem__reg a_2))) ]))%Z)
65
   ((0 = i)%Z)) ->
66
  (forall (f_2 : S_f_mem_pack), ((IsS_f_mem_pack f_2)) ->
67
   (forall (f_3 : S_f_mem_pack), (P_f_pack0) -> ((IsS_f_mem_pack f_3)) ->
68
    ((P_f_pack2 t_3 t_2 f_2 a_2)) -> (P_trans_fA))) ->
69
  (forall (f_2 : S_f_mem_pack), ((IsS_f_mem_pack f_2)) ->
70
   (forall (f_3 : S_f_mem_pack), (P_f_pack0) -> ((IsS_f_mem_pack f_3)) ->
71
    ((P_f_pack2 t_3 t_2 f_2 a_2)) -> ((P_trans_fB i_1%Z x_1)))) ->
72
  (forall (f_2 : S_f_mem_pack), ((IsS_f_mem_pack f_2)) ->
73
   (forall (f_3 : S_f_mem_pack), ((IsS_f_mem_pack f_3)) ->
74
    ((P_f_pack1 t_3 t_1 f_3 a_2)) -> ((P_f_pack2 t_3 t_2 f_2 a_2)) ->
75
    ((P_trans_fD i_1%Z f_2 f_3 x_3 i%Z)))) ->
76
  (forall (f_2 : S_f_mem_pack), ((IsS_f_mem_pack f_2)) ->
77
   (forall (f_3 : S_f_mem_pack), ((IsS_f_mem_pack f_3)) ->
78
    ((P_f_pack1 t_3 t_1 f_3 a_2)) -> ((P_f_pack2 t_3 t_2 f_2 a_2)) ->
79
    ((P_trans_fC i_1%Z f_2 f_3 x_3 x_2)))) ->
80
  ((P_trans_fE i_1%Z f_1 f (m.[ a_1 ])%Z x)).
81

    
82
Proof.
83
  auto with zarith.
84
Qed.
85