Library CFML.Stdlib.Array_proof

Set Implicit Arguments.
Require Import CFLib.
Require Import LibListZ LibListSub.
Require Sys_ml.
Require Array_ml.



Implicit Types t : loc. Implicit Types i ofs len : int.


Notation "'App'' t `[ i ]" := (App Array_ml.get t i;)
  (at level 69, t at level 0, no associativity,
   format "'App'' t `[ i ]") : charac.

Notation "'App'' t `[ i ] `<- x" := (App Array_ml.set t i x;)
  (at level 69, t at level 0, no associativity,
   format "'App'' t `[ i ] `<- x") : charac.



Parameter Array : forall A, list A -> loc -> hprop.

Parameter affine_Array : forall A t (L: list A), affine (t ~> Array L).
Hint Resolve affine_Array : affine.

Hint Transparent array : affine.



Parameter bounded_length:
  forall A t (xs : list A),
  t ~> Array xs ==>
  t ~> Array xs \* \[ length xs <= Sys_ml.max_array_length ].



Parameter of_list_spec :
  curried 2%nat Array_ml.of_list /\
  forall A (xs:list A),
  app Array_ml.of_list [xs]
    PRE \[]
    POST (fun t => t ~> Array xs).

Hint Extern 1 (RegisterSpec Array_ml.of_list) => Provide of_list_spec.



Parameter length_spec :
  curried 1%nat Array_ml.length /\
  forall A (xs:list A) t,
  app Array_ml.length [t]
    INV (t ~> Array xs)
    POST (fun n => \[n = length xs]).

Hint Extern 1 (RegisterSpec Array_ml.length) => Provide length_spec.



Parameter get_spec :
  curried 2%nat Array_ml.get /\
  forall A `{Inhab A} (xs:list A) t i,
  index xs i ->
  app Array_ml.get [t i]
    INV (t ~> Array xs)
    POST \[= xs[i] ].

Hint Extern 1 (RegisterSpec Array_ml.get) => Provide get_spec.



Parameter set_spec :
  curried 2%nat Array_ml.set /\
  forall A (xs:list A) t i x,
  index xs i ->
  app Array_ml.set [t i x]
    PRE ( t ~> Array xs)
    POST (# t ~> Array (xs[i:=x])).

Hint Extern 1 (RegisterSpec Array_ml.set) => Provide set_spec.




Parameter make_spec :
  curried 2%nat Array_ml.make /\
  forall A n (x:A),
  0 <= n ->
  app Array_ml.make [n x]
    PRE \[]
    POST (fun t => Hexists xs, t ~> Array xs \* \[xs = make n x]).

Hint Extern 1 (RegisterSpec Array_ml.make) => Provide make_spec.




Local Hint Resolve index_of_index_length int_index_prove.
Lemma aaa: forall n, n <= n.
Proof. math. Qed.
Lemma aab: forall n, 0 <= n -> n <> 0 -> 0 < n.
Proof. math. Qed.
Lemma aac: forall i, 1 <= i -> 0 <= i.
Proof. math. Qed.

Local Hint Resolve aaa aab aac.

Lemma singleton_prefix_make:
  forall n A (x : A),
  0 < n ->
  prefix (x :: nil) (make n x).
Proof.
  intros.
  exists (make (n - 1) x).
  rewrite app_cons_one_r.
  rewrite* <- make_eq_cons_make_pred.
Qed.

Lemma prefix_snoc_write:
  forall A i n x (xs zs : list A),
  prefix xs zs ->
  i = length xs ->
  n = length zs ->
  i < n ->
  prefix (xs & x) zs[i := x].
Proof.
  introv [ ys Hp ] Hxs Hzs ?.
  destruct ys as [| y ys ].
  { false. rewrite app_nil_r in Hp. subst xs. math. }
  
  exists ys. subst zs. rewrite* update_middle.
Qed.

Lemma prefix_identity:
  forall A n (xs zs : list A),
  prefix xs zs ->
  n = length xs ->
  n = length zs ->
  xs = zs.
Proof.
  introv [ ys ? ] Hxs Hzs. subst zs. rewrite length_app in Hzs.
  assert (ys = nil). { eapply length_zero_inv. math. }
  subst ys. rewrite app_nil_r. reflexivity.
Qed.

Lemma init_spec :
  forall A (F : list A -> hprop) (n : int) (f : func),
  0 <= n ->
  (forall (i : int) (xs : list A),
      index n i ->
      i = length xs ->
      app f [i]
        PRE (F xs)
        POST (fun x => F (xs & x))) ->
  app Array_ml.init [n f]
    PRE (F nil)
    POST (fun t =>
           Hexists xs, t ~> Array xs \* \[n = length xs] \* F xs).
Proof.
  introv ? hf.
  xcf.
  xassert. { xret. xsimpl*. }
  
  xret. xintros. xif.
  { xstraight. }
  
  { xapp* hf as x.
    xstraight.
    xfor_inv (fun i =>
      Hexists xs zs,
      F xs \*
      res ~> Array zs \*
      \[ prefix xs zs ] \*
      \[ i = length xs ] \*
      \[ n = length zs ]
    ).
    math.
    { xsimpl (nil & x).
      { rewrite* length_make. }
      { rewrite app_nil_l, length_one. eauto. }
      { rewrite app_nil_l. apply* singleton_prefix_make. }
    }
    
    { clear x. intros i [ ? ? ]. xpull; intros xs zs. intros.
      xapp* hf as x.
      xapp*.
      xsimpl* (xs & x).
      { rewrite* length_update. }
      { rew_list. math. }
      { eauto using prefix_snoc_write. }
    }
    
    { clear x. intros xs zs. intros. xret.
      forwards*: prefix_identity. math. subst xs.
      xsimpl*. }
  }
Qed.

Hint Extern 1 (RegisterSpec Array_ml.init) => Provide init_spec.



Parameter copy_spec:
  curried 1%nat Array_ml.copy /\
  forall A (xs:list A) t,
  app Array_ml.copy [t]
    INV (t ~> Array xs)
    POST (fun t' => t' ~> Array xs).

Hint Extern 1 (RegisterSpec Array_ml.copy) => Provide copy_spec.



Parameter fill_spec :
  curried 4%nat Array_ml.fill /\
  forall A `{Inhab A} (xs:list A) t ofs len x,
  0 <= ofs ->
  ofs <= length xs ->
  0 <= len ->
  ofs + len <= length xs ->
  app Array_ml.fill [t ofs len x]
    PRE (t ~> Array xs)
    POST (# Hexists xs', t ~> Array xs' \*
      \[ length xs' = length xs ] \*
      \[ forall i, ofs <= i < ofs + len -> xs'[i] = x ] \*
      \[ forall i, (i < ofs \/ ofs + len <= i) -> xs'[i] = xs[i] ]
    ).

Hint Extern 1 (RegisterSpec Array_ml.fill) => Provide fill_spec.




Parameter iter_spec :
  curried 2%nat Array_ml.iter /\
  forall A (I : list A -> hprop),
  forall xs f t,
  (
    forall ys x,
    prefix (ys & x) xs ->
    app f [x]
      PRE (I ys)
      POST (# I (ys & x))
  ) ->
  app Array_ml.iter [f t]
    PRE ( t ~> Array xs \* I nil)
    POST (# t ~> Array xs \* I xs ).

Hint Extern 1 (RegisterSpec Array_ml.iter) => Provide iter_spec.




Parameter sub_spec :
  curried 3%nat Array_ml.sub /\
  forall A `{Inhab A} (xs:list A) t ofs len,
  0 <= ofs ->
  0 <= len ->
  ofs + len <= length xs ->
  app Array_ml.sub [t ofs len]
    INV (t ~> Array xs)
    POST (fun t' => Hexists xs',
             t' ~> Array xs'
          \* \[length xs' = len]
          \* \[forall i, ofs <= i < len -> xs'[i] = xs[i]]).

Hint Extern 1 (RegisterSpec Array_ml.sub) => Provide sub_spec.