LambdaStructLifted.v 19.5 KB
Newer Older
charguer's avatar
cleanup  
charguer committed
1 2 3 4 5 6 7 8 9 10 11
(**

This file formalizes basic examples from standard Separation Logic, 
as described in Arthur Charguéraud's lecture notes.

Author: Arthur Charguéraud.
License: MIT.

*)

Set Implicit Arguments.
charguer's avatar
stable  
charguer committed
12
Require Export LambdaStruct LambdaCFLifted.
charguer's avatar
cleanup  
charguer committed
13 14 15 16 17 18 19
Open Scope trm_scope.
Open Scope charac.
Generalizable Variables A.

Ltac auto_star ::= jauto.


charguer's avatar
charguer committed
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

(* ********************************************************************** *)
(* * Derived basic functions, useful for metaprogramming *)

(* ---------------------------------------------------------------------- *)
(* ** Rewriting lemmas for [Subst] *)

Lemma Subst_seq : forall x V t1 t2,
  Subst x V (trm_seq t1 t2) = trm_seq (Subst x V t1) (Subst x V t2).
Proof using. auto. Qed.

(* LATER: complete *)


(* ---------------------------------------------------------------------- *)
(* ** Rewriting lemmas for [Substs] *)

Lemma Substs_cons : forall x xs V Vs t,
  Substs (x::xs) (V::Vs) t = Substs xs Vs (Subst x V t).
Proof using. auto. Qed.

Lemma Substs_val : forall xs Vs (v:val),
  length Vs = length xs ->
  Substs xs Vs v = v.
Proof using.
  unfold Substs. intros xs. induction xs as [|x xs']; introv E. { auto. }
  destruct Vs as [|V Vs']; rew_list in *. { false. }
  (* todo: induction principle on two lists of the same length *)
  simpl. rewrite~ IHxs'.
Qed.

Lemma Substs_var_neq : forall xs (Vs:dyns) x,
  var_fresh x xs ->
  length Vs = length xs ->
  Substs xs Vs (trm_var x) = trm_var x.
Proof using.
  intros xs. unfold Substs. induction xs as [|x xs']. { auto. }
  introv HF EL. destruct Vs as [|V Vs']; rew_list in *. { false. }
  (* todo: induction principle on two lists of the same length *)
  simpls. case_if in HF. case_if. rewrite~ IHxs'.
Qed.

Lemma Substs_seq : forall xs Vs t1 t2,
  length xs = length Vs ->
  Substs xs Vs (trm_seq t1 t2) = trm_seq (Substs xs Vs t1) (Substs xs Vs t2).
Proof using.
  intros xs. induction xs as [|x xs']; introv E.
  { auto. }
  { destruct Vs as [|V Vs']. { rew_list in E. false. }
    do 3 rewrite Substs_cons. rewrite Subst_seq.
    rew_list in E. rewrite~ IHxs'. }
Qed.

Lemma Substs_let : forall xs (Vs:dyns) x t1 t2,
  var_fresh x xs ->
  length Vs = length xs ->
  Substs xs Vs (trm_let x t1 t2) = trm_let x (Substs xs Vs t1) (Substs xs Vs t2).
Proof using.
  intros xs. unfold Substs. induction xs as [|x xs']. { auto. }
  introv HF EL. destruct Vs as [|V Vs']; rew_list in *. { false. }
  (* todo: induction principle on two lists of the same length *)
  simpls. case_if in HF. case_if. rewrite~ IHxs'.
Qed.

Lemma Substs_app : forall xs (Vs:dyns) t1 t2,
  length Vs = length xs ->
  Substs xs Vs (trm_app t1 t2) = trm_app (Substs xs Vs t1) (Substs xs Vs t2).
Proof using.
  intros xs. unfold Substs. induction xs as [|x xs']. { auto. }
  introv EL. destruct Vs as [|V Vs']; rew_list in *. { false. }
  (* todo: induction principle on two lists of the same length *)
  simpls. rewrite~ IHxs'.
Qed.

(* LATER: complete *)


charguer's avatar
cleanup  
charguer committed
97 98 99 100 101 102 103 104
(* ********************************************************************** *)
(* * Derived basic functions *)

(* ---------------------------------------------------------------------- *)
(* ** Increment *)

Lemma Rule_incr : forall (p:loc) (n:int), 
  Triple (val_incr `p)
charguer's avatar
rename  
charguer committed
105 106
    PRE (p ~~> n) 
    POST (fun (r:unit) => p ~~> (n+1)).
charguer's avatar
cleanup  
charguer committed
107
Proof using.
charguer's avatar
charguer committed
108
  xcf. xapps. xapps. xapps. hsimpl~.
charguer's avatar
stable  
charguer committed
109
Qed. 
charguer's avatar
cleanup  
charguer committed
110

charguer's avatar
charguer committed
111
Hint Extern 1 (Register_Spec val_incr) => Provide Rule_incr.
charguer's avatar
cleanup  
charguer committed
112 113 114 115 116 117 118


(* ---------------------------------------------------------------------- *)
(* ** Negation *)

Lemma Rule_not : forall (b:bool), 
  Triple (val_not b)
charguer's avatar
stable  
charguer committed
119 120
    PRE \[] 
    POST (fun b' => \[b' = !b]).
charguer's avatar
cleanup  
charguer committed
121 122 123 124 125 126 127 128 129 130 131 132 133 134
Proof using.
  intros. unfold Triple, Post. xapply rule_not. (*todo: xapplys bug *)
  hsimpl. hpull. intros. subst. hsimpl~ (!b).
Qed.

Hint Extern 1 (Register_Spec val_not) => Provide Rule_not.


(* ---------------------------------------------------------------------- *)
(* ** Disequality *)

Lemma Rule_neq : forall `{EA:Enc A} (v1 v2:A), 
  Enc_injective EA ->
  Triple (val_neq `v1 `v2)
charguer's avatar
stable  
charguer committed
135 136
    PRE \[] 
    POST (fun (b:bool) => \[b = isTrue (v1 <> v2)]).
charguer's avatar
charguer committed
137 138 139
Proof using. 
  intros. xcf.
  xapps~. (* Details: xlet. xapp~.xpull ;=> X E. subst. *)
charguer's avatar
compile  
charguer committed
140
  xapps. isubst. hsimpl. rew_isTrue~.
charguer's avatar
cleanup  
charguer committed
141 142 143 144 145 146
Qed.

Hint Extern 1 (Register_Spec val_neq) => Provide Rule_neq.


(* ********************************************************************** *)
charguer's avatar
charguer committed
147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166
(* * Lifted records *)

(* ---------------------------------------------------------------------- *)
(* ** Record representation *)

(** Representation predicate [r ~> Record L], where [L]
    is an association list from fields to values. *)

Definition Record_field : Type := field * dyn.
Definition Record_fields : Type := list Record_field.

Fixpoint Record (L:Record_fields) (r:loc) : hprop :=
  match L with
  | nil => \[]
  | (f, Dyn V)::L' => (r `.` f ~~> V) \* (r ~> Record L')
  end. 

(* TODO: currently restricted due to [r `.` f ~> V] not ensuring [r<>null] *)
Lemma hRecord_not_null : forall (r:loc) (L:Record_fields),
  (* L <> nil -> *)
charguer's avatar
compile  
charguer committed
167
  mem (0%nat:field) (List.map fst L) ->
charguer's avatar
charguer committed
168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223
  (r ~> Record L) ==> (r ~> Record L) \* \[r <> null].
Proof using.
  introv M. induction L as [|(f,[A EA v]) L'].
  { inverts M. }
  { xunfold Record. inverts M.
    { hchange~ (Hfield_not_null r). hsimpl~. }
    { hchange~ IHL'. hsimpl~. } }
Qed.

(** Lemmas for unfolding the definition *)

Lemma Record_nil : forall p,
  p ~> Record nil = \[].
Proof using. auto. Qed.

Lemma Record_cons : forall p x (V:dyn) L,
  (p ~> Record ((x, V)::L)) =
  (p`.`x ~~> (`V) \* p ~> Record L).
Proof using. intros. destruct~ V. Qed.

Lemma Record_not_null : forall (r:loc) (L:Record_fields),
  L <> nil ->
  (r ~> Record L) ==+> \[r <> null].
Proof using.
  intros. destruct L as [|(f,v) L']. { false. } 
  rewrite Record_cons. hchanges~ Hfield_not_null.
Qed.


(** Notation for record contents (only supported up to arity 5) *)

Notation "`{ f1 := x1 }" := 
  ((f1, Dyn x1)::nil)
  (at level 0, f1 at level 0) 
  : fields_scope.
Notation "`{ f1 := x1 ; f2 := x2 }" :=
  ((f1, Dyn x1)::(f2, Dyn x2)::nil)
  (at level 0, f1 at level 0, f2 at level 0) 
  : fields_scope.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 }" :=
  ((f1, Dyn x1)::(f2, Dyn x2)::(f3, Dyn x3)::nil)
  (at level 0, f1 at level 0, f2 at level 0, f3 at level 0) 
  : fields_scope.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 }" :=
  ((f1, Dyn x1)::(f2, Dyn x2)::(f3, Dyn x3)::(f4, Dyn x4)::nil)
  (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0)
  : fields_scope.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 }" :=
  ((f1, Dyn x1)::(f2, Dyn x2)::(f3, Dyn x3)::(f4, Dyn x4)::(f5, Dyn x5)::nil)
  (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0, f5 at level 0)
  : fields_scope.

Open Scope fields_scope.
Bind Scope fields_scope with Record_fields.
Delimit Scope fields_scope with fields.

charguer's avatar
cleanup  
charguer committed
224 225 226 227 228 229 230 231 232

(* ---------------------------------------------------------------------- *)
(* ** Derived small-footprint lifted specifications for records *)

Section Rule_fields.
Transparent Hfield.

Lemma Rule_get_field : forall (l:loc) f `{EA:Enc A} (V:A),
  Triple ((val_get_field f) l)
charguer's avatar
charguer committed
233 234
    PRE (l `.` f ~~> V) 
    POST (fun r => \[r = V] \* (l `.` f ~~> V)).
charguer's avatar
cleanup  
charguer committed
235
Proof using. 
charguer's avatar
charguer committed
236
  intros. unfold Triple, Post. rewrite Hfield_to_hfield. xapplys~ rule_get_field.
charguer's avatar
cleanup  
charguer committed
237 238 239 240
Qed.

Lemma Rule_set_field : forall `{EA1:Enc A1} (V1:A1) (l:loc) f `{EA2:Enc A2} (V2:A2),
  Triple ((val_set_field f) l `V2)
charguer's avatar
charguer committed
241 242
    PRE (l `.` f ~~> V1) 
    POST (fun (r:unit) => l `.` f ~~> V2).
charguer's avatar
cleanup  
charguer committed
243
Proof using. 
charguer's avatar
charguer committed
244
  intros. unfold Triple, Post. rewrite Hfield_to_hfield. xapply~ rule_set_field.
charguer's avatar
cleanup  
charguer committed
245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280
  hsimpl. hsimpl~ tt.
Qed.

End Rule_fields.


(* ---------------------------------------------------------------------- *)
(* ** Derived large-footprint lifted specifications for records *)

Definition field_eq_dec := Nat.eq_dec.

Fixpoint record_get_compute_dyn (f:field) (L:Record_fields) : option dyn :=
  match L with
  | nil => None
  | (f',d')::T' => 
     if field_eq_dec f f' 
       then Some d' 
       else record_get_compute_dyn f T'
  end.

Definition record_get_compute_spec (f:field) (L:Record_fields) : option Prop :=
  match record_get_compute_dyn f L with
  | None => None 
  | Some (Dyn V) => Some (forall r,
     Triple (val_get_field f `r) (r ~> Record L) (fun x => \[x = V] \* r ~> Record L))
  end.

Lemma record_get_compute_spec_correct : forall (f:field) L (P:Prop),
  record_get_compute_spec f L = Some P -> 
  P.
Proof using.
  introv M. unfolds record_get_compute_spec. 
  sets_eq <- vo E: (record_get_compute_dyn f L).
  destruct vo as [[T ET v]|]; inverts M. intros r.
  induction L as [|[F D] L']; [false|].
  destruct D as [A EA V]. simpl in E.
charguer's avatar
compile  
charguer committed
281 282
  xunfold Record at 1. xunfold Record at 2. case_if. (*--todo fix subst *)
  { subst. inverts E. xapplys~ Rule_get_field. }
charguer's avatar
cleanup  
charguer committed
283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313
  { specializes IHL' (rm E). xapplys~ IHL'. }
Qed.

Fixpoint record_set_compute_dyn (f:nat) (d:dyn) (L:Record_fields) : option Record_fields :=
  match L with
  | nil => None
  | (f',d')::T' => 
     if field_eq_dec f f' 
       then Some ((f,d)::T') 
       else match record_set_compute_dyn f d T' with
            | None => None
            | Some L' => Some ((f',d')::L')
            end
  end.

Definition record_set_compute_spec (f:field) `{EA:Enc A} (W:A) (L:Record_fields) : option Prop :=
  match record_set_compute_dyn f (Dyn W) L with
  | None => None 
  | Some L' => Some (forall r,
     Triple (val_set_field f `r `W) (r ~> Record L) (fun (_:unit) => r ~> Record L'))
  end.

Lemma record_set_compute_spec_correct : forall (f:field) `{EA:Enc A} (W:A) L (P:Prop),
  record_set_compute_spec f W L = Some P ->
  P.
Proof using.
  introv M. unfolds record_set_compute_spec. 
  sets_eq <- do E: (record_set_compute_dyn f (Dyn W) L).
  destruct do as [L'|]; inverts M. 
  gen L'. induction L as [|[f' D] T]; intros; [false|].
  destruct D as [A' EA' V]. simpl in E.
charguer's avatar
compile  
charguer committed
314 315 316
  xunfold Record at 1. simpl. case_if. (*--todo fix subst *)
  { subst. inverts E. xapply~ Rule_set_field. intros _. xunfold Record at 2. simpl. hsimpl. }
  { cases (record_set_compute_dyn f (Dyn W) T) as C'; [|false].
charguer's avatar
cleanup  
charguer committed
317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383
    inverts E. specializes~ IHT r. xapply IHT. hsimpl.
    intros. xunfold Record at 2. simpl. hsimpl~. }
Qed.

Global Opaque Record.


(* ---------------------------------------------------------------------- *)
(* ** Tactics for generating specifications for get and set on records *)

(** Auxiliary tactic to read the record state from the pre-condition *)

Ltac xspec_record_repr_compute r H :=
  match H with context [ r ~> Record ?L ] => constr:(L) end.

(** Tactic [xget] derives a record [get] specification *)

Ltac xspec_record_get_compute_for f L :=
  let G := fresh in
  forwards G: (record_get_compute_spec_correct f L);
  [ reflexivity | revert G ].

Ltac xspec_record_get_loc v :=
  match v with
  | val_loc ?r => constr:(r)
  | @enc loc Enc_loc ?r => constr:(r)
  end.

Ltac xspec_record_get_compute tt :=
  match goal with |- Triple (trm_apps (trm_val (val_get_field ?f)) ((trm_val ?v)::nil)) ?H _ =>
    let r := xspec_record_get_loc v in
    let L := xspec_record_repr_compute r H in
    xspec_record_get_compute_for f L end.

(** Tactic [sget] derives a record [set] specification *)

Ltac xspec_record_get_arg w :=
  match w with
  | @enc _ _ ?W => constr:(W)
  | _ => constr:(w)
  end.

Ltac xspec_record_set_compute_for f W L :=
  let G := fresh in
  forwards G: (record_set_compute_spec_correct f W L);
  [ reflexivity | revert G ].

Ltac xspec_record_set_compute tt :=
  match goal with |- Triple (trm_apps (trm_val (val_set_field ?f)) ((trm_val ?v)::(trm_val ?w)::nil)) ?H _ =>
    let r := xspec_record_get_loc v in  
    let W := xspec_record_get_arg w in
    let L := xspec_record_repr_compute r H in
    xspec_record_set_compute_for f W L end.


(*--------------------------------------------------------*)
(* ** [xspec] extended to get and set functions *)

Ltac xspec_base tt ::=
  match goal with
  | |- Triple (trm_apps (trm_val (val_get_field ?f)) _) _ _ =>
     xspec_record_get_compute tt
  | |- Triple (trm_apps (trm_val (val_set_field ?f)) _) _ _ =>
     xspec_record_set_compute tt
  | |- ?G => xspec_database G
  end.

charguer's avatar
charguer committed
384

charguer's avatar
charguer committed
385
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
386
(* ** Conversion between allocated segments and record representation *)
charguer's avatar
charguer committed
387

charguer's avatar
charguer committed
388 389
Section Alloc_to_Record.
Transparent Record repr loc.
charguer's avatar
charguer committed
390

charguer's avatar
charguer committed
391
(** Special case of arity 2 *)
charguer's avatar
charguer committed
392

charguer's avatar
charguer committed
393
Lemma Alloc2_to_Record : forall p, p <> null ->
charguer's avatar
charguer committed
394 395 396 397
  Alloc (abs 2) p ==> 
    Hexists (v1:val) (v2:val),
    (p ~> Record `{ (0%nat) := v1; (1%nat) := v2}).
Proof using.
charguer's avatar
charguer committed
398 399 400
  introv Np. change (abs 2) with 2%nat. rew_Alloc.
  hpull ;=> v1 v2. xunfold Record. unfold repr.
  rewrite Hfield_eq_fun_Hsingle. xunfold Hsingle.
charguer's avatar
charguer committed
401 402
  replace (p+0)%nat with p; [ | unfolds loc; math ].
  replace (p+1)%nat with (S p); [ | unfolds loc; math ].
charguer's avatar
charguer committed
403
  hsimpl~.
charguer's avatar
charguer committed
404 405
Qed.

charguer's avatar
charguer committed
406 407
(** General case *)

charguer's avatar
charguer committed
408 409
Lemma Alloc_to_Record : forall (p:loc) (start:nat) (n:nat),
  p <> null ->
charguer's avatar
charguer committed
410
  let xs := nat_seq start n in
charguer's avatar
charguer committed
411 412
      Alloc n (p+start)%nat 
  ==> Hexists (Vs:dyns), \[length Vs = n] \* p ~> Record (combine xs Vs).
charguer's avatar
charguer committed
413
Proof using.
charguer's avatar
charguer committed
414
  introv Np. gen start. induction n; intros; rew_Alloc.
charguer's avatar
charguer committed
415
  { subst. hsimpl (@nil dyn). rew_list~. }
charguer's avatar
charguer committed
416 417
  { hpull ;=> v. forwards K: (rm IHn) (S start).  
    math_rewrite ((p + S start)%nat = S (p+start)) in K.
charguer's avatar
charguer committed
418
    hchange K. hpull ;=> Vs LVs. applys (himpl_hexists_r ((Dyn v)::Vs)).
charguer's avatar
charguer committed
419
    simpl List.combine. xunfold Record.
charguer's avatar
charguer committed
420 421 422
    rewrite Hfield_to_hfield.
    rewrite hfield_eq_fun_hsingle. rew_enc.
    unfold repr. hsimpl~. rew_list; math. }
charguer's avatar
charguer committed
423 424 425 426 427 428 429 430
Qed.

End Alloc_to_Record.


(* ---------------------------------------------------------------------- *)
(* ** Specification for allocation of records of arity 2,
      See below for the generalization to arbitrary arities. *)
charguer's avatar
charguer committed
431 432 433 434 435 436 437 438 439 440 441 442 443 444

Definition val_new_record_2 := 
  Vars X1, X2, P in
  ValFun X1 X2 := 
    Let P := val_alloc 2 in
    val_set_field 0%nat P X1;;
    val_set_field 1%nat P X2;;
    P.

Lemma Rule_new_record_2 : forall `{EA1:Enc A1} `{EA2:Enc A2} (v1:A1) (v2:A2),
  Triple (val_new_record_2 `v1 `v2) 
    PRE \[]
    POST (fun p => p ~> Record`{ 0%nat := v1 ; 1%nat := v2 }).
Proof using. 
charguer's avatar
charguer committed
445
  xcf. xapp Rule_alloc as p. { math. } (* TODO: try Rule_alloc_nat *)
charguer's avatar
charguer committed
446
  intros Np. xchanges~ Alloc2_to_Record ;=> w1 w2.
charguer's avatar
charguer committed
447 448 449 450 451
  xapp. xapp. xval~. hsimpl.
Qed.


(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
452
(* ** Specification for allocation of records of arbitrary arity *)
charguer's avatar
charguer committed
453 454 455

Definition val_new_record (n:nat) :=
  let xs := nat_seq 0%nat n in
charguer's avatar
charguer committed
456
  let P : var := n%nat in
charguer's avatar
charguer committed
457 458 459 460
  val_funs xs (
    Let P := val_alloc n in
    LibList.fold_right (fun x t => val_set_field (x:field) P (x:var);; t) (trm_var P) xs).

charguer's avatar
charguer committed
461
Lemma Subst_new_record_aux : forall xs Vs (i n n':nat) (p:loc),
charguer's avatar
charguer committed
462 463 464 465 466 467 468 469 470 471 472 473 474 475 476
  n' = length Vs ->
  xs = nat_seq i n' ->
  (i + n' = n)%nat ->
    (Subst n (Dyn p) (Substs xs Vs (fold_right (fun x t => trm_seq (val_set_field x (trm_var n) (trm_var x)) t) (trm_var n) xs)))
  =  fold_right (fun xV t => let '(x,V) := xV in trm_seq (val_set_field x p (enc V)) t) p (LibList.combine xs Vs).
Proof using.
  intros xs. induction xs as [|x xs']; introv LVs Exs Ein. 
  { simpl combine. rew_list. unfold Subst. simpl. case_if~. } 
  { forwards Lin: length_nat_seq i n'.
    rewrite <- Exs in Lin. rew_list in Lin. 
    destruct Vs as [|V Vs']. { false. rew_list in LVs. math. }
    rew_list in LVs. asserts EL: (length xs' = length Vs'). { math. }
    destruct n' as [|n'']. { inverts Exs. } simpl in Exs. 
    invert Exs. intros Ei Exs'. subst i. rewrite <- Exs'. 
    asserts N: (x <> n). { math. } 
charguer's avatar
compile  
charguer committed
477
    rewrite Substs_cons. rewrite combine_cons. rew_listx.
charguer's avatar
charguer committed
478 479 480 481 482 483 484
    rewrite Subst_seq.
    asserts_rewrite (Subst x V (val_set_field x (trm_var n) (trm_var x)) 
                     = val_set_field x (trm_var n) (enc V)).
    { unfold Subst. simpl. case_if. case_if~.  }
    rewrite~ Substs_seq.
    asserts_rewrite (Substs xs' Vs' (val_set_field x (trm_var n) `V) 
                    = (val_set_field x (trm_var n) `V)).
charguer's avatar
charguer committed
485 486
    { do 2 rewrite~ Substs_app. do 2 rewrite~ Substs_val. rewrite~ Substs_var_neq.
      { rewrite Exs'. applys var_fresh_nat_seq_ge. math. } }
charguer's avatar
charguer committed
487 488
    rewrite~ Subst_seq.
    asserts_rewrite (Subst n (Dyn p) (val_set_field x (trm_var n) `V) = val_set_field x p `V).
charguer's avatar
charguer committed
489
    { unfold Subst; simpl. case_if~. } (* todo: lemma Subst_var *)
charguer's avatar
charguer committed
490
    fequals.
charguer's avatar
charguer committed
491 492 493 494 495 496 497 498 499 500 501 502
    match goal with |- context [Subst x V ?t'] => set (t:=t') end.
    asserts_rewrite (Subst x V t = t).
    { subst xs'. cuts K: (forall n' i, 
       (x < i)%nat ->
        let t := @fold_right nat trm (fun f t => trm_seq (val_set_field f (trm_var n) (trm_var f)) t) (trm_var n) (nat_seq i n') in
       Subst x V t = t).
     { applys K. math. }
     intros n'. gen N. clears_all. induction n'; introv L; intros; subst t.
     { simpl. unfold Subst. simpl. case_if~. } (*todo: Subst_var_neq.*)
     { simpl. rewrite Subst_seq. fequals.
       { unfold Subst. simpl. case_if. case_if. { false; math. } { auto. } }
       { rewrite~ IHn'. } } } 
charguer's avatar
charguer committed
503 504 505
    applys IHxs' Exs'; math. }
Qed.

charguer's avatar
charguer committed
506 507 508
Lemma Rule_new_record : forall (n:nat) (Vs:dyns),
  (n > 0)%nat ->
  n = length Vs -> 
charguer's avatar
charguer committed
509
  let xs := nat_seq 0%nat n in
charguer's avatar
charguer committed
510 511
  Triple (trm_apps (val_new_record n) (encs Vs))
    PRE \[]
charguer's avatar
charguer committed
512
    POST (fun p => p ~> Record (combine xs Vs)).
charguer's avatar
charguer committed
513
Proof using. 
charguer's avatar
charguer committed
514
  introv HP LVs. intros xs. applys Rule_apps_funs.
charguer's avatar
charguer committed
515 516
  { reflexivity. }
  { subst. applys~ var_funs_nat_seq. }
charguer's avatar
charguer committed
517 518
  { asserts EL: (length Vs = length xs). { unfold xs. rewrite~ length_nat_seq. }
    rewrite Substs_let; [| applys var_fresh_nat_seq_ge; math | auto ].
charguer's avatar
charguer committed
519
    asserts_rewrite (Substs (nat_seq 0 n) Vs (val_alloc n) = val_alloc n).
charguer's avatar
charguer committed
520 521
    { rewrite~ Substs_app. do 2 rewrite~ Substs_val. }
    eapply (@Rule_let _ _ _ _ _ _ _ loc). (* todo: cleanup *)
charguer's avatar
charguer committed
522
    { xapplys Rule_alloc_nat. }
charguer's avatar
charguer committed
523
    { intros p. xpull ;=> Np. xchange~ (@Alloc_to_Record p 0%nat).
charguer's avatar
charguer committed
524
      { math_rewrite ((p+0)%nat = p). hsimpl. } (* todo simplify *)
charguer's avatar
charguer committed
525
        xpull ;=> Ws LWs. fold xs.
charguer's avatar
charguer committed
526
        rewrite (@Subst_new_record_aux xs Vs 0%nat n n); try first [ math | auto ].
charguer's avatar
charguer committed
527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544
        asserts Lxs: (length xs = n). { subst xs. rewrite~ length_nat_seq. }
        clearbody xs. clear HP.
        applys local_weaken_post (fun p' => \[p' = p] \* p ~> Record (combine xs Vs));
        [ xlocal | | hsimpl; intros; subst~]. (* todo: weaken_post with swapped order *)
        gen n Vs Ws. induction xs; intros.
        { simpl. (* todo: rew_list *) applys~ Rule_val p. hsimpl~. }
        { rew_list in Lxs.
          destruct Vs as [|V Vs']; rew_list in LVs.
          { false; math. }
          destruct Ws as [|W Ws']; rew_list in LWs.
          { false; math. }
          destruct n as [|n']. { false; math. }
          { do 2 rewrite combine_cons. rew_list.
            rewrite Record_cons. applys Rule_seq.
            { xapplys @Rule_set_field. }
            { simpl. xapply (>> IHxs n' Vs' Ws'); try math.
              { hsimpl. } { intros p'. rewrite Record_cons. hsimpl~. } } } } } }
Qed.
charguer's avatar
charguer committed
545 546 547 548 549 550 551 552 553 554

Lemma Rule_new_record' : forall (n:nat) (Vs:dyns) (vs:vals) (Q:loc->hprop),
  vs = (encs Vs) ->
  (n = List.length Vs)%nat -> 
  (n > 0)%nat ->
  let xs := nat_seq 0%nat n in
  ((fun p => p ~> Record (List.combine xs Vs)) ===> Q) ->
  Triple (trm_apps (val_new_record n) (vals_to_trms vs)) \[] Q.
Proof using. 
  introv E HL HP HQ. rewrite List_length_eq in HL.
charguer's avatar
ok  
charguer committed
555
  rewrite List_combine_eq in HQ; [| rewrite~ length_nat_seq].
charguer's avatar
charguer committed
556
  subst. xapply~ Rule_new_record. hsimpl. hchanges~ HQ.
charguer's avatar
charguer committed
557 558
Qed.

charguer's avatar
charguer committed
559 560 561 562 563
(** Tactic [xrule_new_record] for proving the specification 
    triple for the allocation of a specific record.
    For an example, check out [ExampleTree.v], 
    Definition [val_new_node] and  Lemma [Rule_new_node]. *)

charguer's avatar
charguer committed
564 565 566
Ltac xrule_new_record_core tt :=
  intros; rew_nary; rew_vals_to_trms; applys Rule_new_record';
  [ xeq_encs | auto | math | hsimpl ].
charguer's avatar
charguer committed
567

charguer's avatar
charguer committed
568 569
Tactic Notation "xrule_new_record" :=
  xrule_new_record_core tt.
charguer's avatar
charguer committed
570 571


charguer's avatar
charguer committed
572 573 574
(* ********************************************************************** *)
(* * Lifted access rules for arrays *)

charguer's avatar
charguer committed
575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596
(* TODO *)





















charguer's avatar
charguer committed
597 598 599 600 601 602 603 604 605 606










charguer's avatar
charguer committed
607 608 609 610 611 612 613 614 615 616