## lustrec / optim / oversampling / out / typed / g_step_assert_2.coq @ 6a93d814

History | View | Annotate | Download (1.95 KB)

1 |
(* ---------------------------------------------------------- *) |
---|---|

2 |
(* --- Assertion (file oversampling0_4.c, line 342) --- *) |

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_g_mem_pack. |

19 |
Require Import Memory. |

20 |
Require Import Compound. |

21 |
Require Import Axiomatic. |

22 |
Require Import Cint. |

23 | |

24 |
Goal |

25 |
forall (t : array Z), |

26 |
forall (t_2 t_1 : farray addr Z), |

27 |
forall (t_3 : farray addr addr), |

28 |
forall (a_1 a : addr), |

29 |
forall (g_1 g : S_g_mem_pack), |

30 |
let a_2 := t_3.[ (shiftfield_F_g_mem_ni_1 a_1) ] in |

31 |
let a_3 := t_3.[ (shiftfield_F_g_mem_ni_0 a_1) ] in |

32 |
let a_4 := t_3.[ (shiftfield_F_f_mem_ni_2 a_3) ] in |

33 |
let a_5 := (shiftfield_F__arrow_reg__first |

34 |
((shiftfield_F__arrow_mem__reg a_2))) in |

35 |
let x := (t_2.[ a_5 ])%Z in |

36 |
((IsS_g_mem_pack g)) -> |

37 |
((IsS_g_mem_pack g_1)) -> |

38 |
((framed t_3)) -> |

39 |
((linked t)) -> |

40 |
(a <> a_2) -> |

41 |
((valid_rw t a 1%Z)) -> |

42 |
((P_valid_g t t_3 a_1)) -> |

43 |
((((region ((base a))%Z)) <= 0)%Z) -> |

44 |
((((region ((base a_1))%Z)) <= 0)%Z) -> |

45 |
((separated a_1 3%Z a 1%Z)) -> |

46 |
((P_g_pack1 t_3 t_1 g a_1)) -> |

47 |
((P_g_pack3 t_3 t_2 g_1 a_1)) -> |

48 |
(a <> a_4) -> |

49 |
(a_2 <> a_4) -> |

50 |
((separated a 1%Z a_3 2%Z)) -> |

51 |
((separated a_1 3%Z a_3 2%Z)) -> |

52 |
((separated a_1 3%Z a_2 1%Z)) -> |

53 |
((separated a_3 2%Z a_2 1%Z)) -> |

54 |
((is_uint32 x)) -> |

55 |
((separated a_1 3%Z a_4 1%Z)) -> |

56 |
((separated a_3 2%Z a_4 1%Z)) -> |

57 |
(itep ((0 = x)%Z) (t_1 = t_2) (t_1 = (t_2.[ a_5 <- (0)%Z ]))) -> |

58 |
(forall (g_2 : S_g_mem_pack), ((IsS_g_mem_pack g_2)) -> |

59 |
(forall (g_3 : S_g_mem_pack), (P_g_pack0) -> ((IsS_g_mem_pack g_3)) -> |

60 |
((P_g_pack3 t_3 t_2 g_2 a_1)) -> (P_trans_gA))) -> |

61 |
((P_trans_gB g_1 g x)). |

62 |