MRVerify/InvertIndex.v at main · PKUTCS-CBS/MRVerify · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
(**

== Representation and verification of InvertIndex ==

This file verifies another MR application.

Author: Bowen Zhang.

Date : 2022.11.1
*)

From SLF (* TLC *) Require Export LibCore TLCbuffer.
From SLF (* Sep *) Require Export Rules AuxLmm.


(* !! Need to read the Language.v firstly !! *)
Export NotationForTrm.
Export NotationForVariables.

Open Scope val_scope.
Open Scope trm_scope.
Open Scope Z_scope.


(*----------------------------- InvertIndex --------------------------------------*)
Definition IIMapper :=
  Fix 'F 'f 'i :=
    Let 'n := 'fsize 'f in
    Let 'be := ('i '= 'n) in
    If_ 'be
    Then (val_Listii nil)
    Else
      Let 'bk := 'nth_blk 'f 'i in
      Let 'i1 := 'i '+ 1 in
      Let 'l := 'locate 'bk in
      Let 'ln := 'iimap 'l in
      Let 'ln1 := 'F 'f 'i1 in
      'ln 'ii:: 'ln1.

Lemma triple_IIMapper: forall Hf Hb (f:floc) (n1 n2:int) (b1 b2:bloc) (L:(list (list idcnt))),
  n1 =? n2 = false /\ b1 =? b2 = false ->
  Hf = ( f ~f~> (b1::b2::nil) ) ->
  Hb = ( (b1 ~b~> (n1::n2::n1::nil)) \b* (b2 ~b~> (n1::nil)) ) ->
  L =  ( ((n1,b1,1)::(n2,b1,1)::(n1,b1,1)::nil) :: ((n1,b2,1)::nil) :: nil ) ->
triple (IIMapper f 0)
    (\R[Hf,Hb])
    (fun r => \[r= val_Listii L] \* \R[Hf,Hb]).
Proof.
  fix_locate.
  rewrite hstar_sep, hfstar_hempty_l. apply himpl_refl.
  rew_read. ext.
  applys triple_let triple_iimap. ext.

  applys triple_let.
  fix_locate.
  rewrite hstar_sep, hfstar_hempty_l,hbstar_comm. apply himpl_refl.
  rew_read. ext.
  applys triple_let triple_iimap. ext.

  applys triple_let.
  exp_fix.
  applys triple_val'. ext.
  apply triple_app_iilist. ext.
  applys triple_conseq triple_app_iilist.
  apply himpl_refl.
  intros r. rew_list.
  rewrite hbstar_comm. apply himpl_refl.
Qed.


Definition IIShuffle :=
  Fun 'f :=
    Let 'L := IIMapper 'f 0 in
    Let 'l := 'iimerge 'L in
      'iishuffle 'l.

Lemma triple_IIShuffle: forall Hf Hb (f:floc) (n1 n2:int) (b1 b2:bloc) (L:(list (list idcnt))),
  n1 =? n2 = false /\ b1 =? b2 = false ->
  Hf = ( f ~f~> (b1::b2::nil) ) ->
  Hb = ( (b1 ~b~> (n1::n2::n1::nil)) \b* (b2 ~b~> (n1::nil)) ) ->
  L =  ( ( ((n1,b1),1)::((n1,b1),1)::nil ) ::
         ( ((n2,b1),1)::nil) ::
         ( ((n1,b2),1)::nil) :: nil ) ->
triple (IIShuffle f)
    (\R[Hf,Hb])
    (fun r => \[r= val_Listii L] \* \R[Hf,Hb]).
Proof.
  intros. subst.
  applys* triple_app_fun. simpl.
  applys triple_let.
  applys triple_conseq_frame.
  applys* triple_IIMapper.
  rewrite hstar_hempty_r'. applys himpl_refl.
  intros r. rewrite hstar_hempty_r.
  applys himpl_refl.
  simpl. intros r. ext.
  applys triple_let.
  applys triple_conseq_frame triple_iimerge.
  rewrite hstar_hempty_r'. applys himpl_refl.
  intros r. rewrite hstar_hempty_r'. applys himpl_refl.
  simpl. intros r. unfold iimerge,merge. ext.
  applys triple_conseq_frame triple_iishuffle.
  rewrite hstar_hempty_r'. applys himpl_refl.
  intros r. rewrite hstar_hempty_r'.
  apply iishuffle_diff in H.
  rewrite <- H. applys himpl_refl.
Qed.

Definition IIReducer :=
  Fun 'f :=
    Let 'L := IIShuffle 'f in
    Let 'l := 'iireduce 'L in
      'iiorgan 'l.

Lemma triple_IIReducer: forall Hf Hb (f:floc) (n1 n2:int) (b1 b2:bloc) (l: list env),
  n1 =? n2 = false /\ b1 =? b2 = false ->
  Hf = ( (f ~f~> (b1::b2::nil)) ) ->
  Hb = ( (b1 ~b~> (n1::n2::n1::nil)) \b* (b2 ~b~> (n1::nil)) ) ->
  l =  ( (n1,((b1,2)::(b2,1)::nil)) :: (n2,((b1,1)::nil)) :: nil ) ->
triple (IIReducer f)
    (\R[Hf,Hb])
    (fun r => \[r= val_listenv l] \* \R[Hf,Hb]).
Proof.
  intros. subst.
  applys* triple_app_fun. simpl.
  applys triple_let.
  applys triple_conseq_frame.
  applys* triple_IIShuffle.
  rewrite hstar_hempty_r'. applys himpl_refl.
  intros r. rewrite hstar_hempty_r.
  applys himpl_refl.
  simpl. intros r. ext.
  applys triple_let.
  applys triple_conseq_frame triple_iireduce.
  rewrite hstar_hempty_r'. applys himpl_refl.
  intros r. rewrite hstar_hempty_r'. applys himpl_refl.
  simpl. intros r. ext.
  applys triple_conseq_frame triple_iiorganize.
  rewrite hstar_hempty_r'. applys himpl_refl.
  intros r. rewrite hstar_hempty_r'.
  apply iiorgan_diff in H.
  rewrite <- H. applys himpl_refl.
Qed.