val array_literal
  (#a:Type0)
  (n:US.t)
  (f:(i:US.t{US.v i < US.v n} -> a))
  : ST (A.array a)
       emp
       (fun arr ->
        A.pts_to arr full_perm (Seq.init (US.v n) (fun i -> f (US.uint_to_t i))))
       (requires US.v n > 0)
       (ensures fun arr -> A.length arr == US.v n)
let array_literal #a n f =
  let arr = A.alloc (f 0sz) n in

  intro_pure
    (array_literal_inv_pure n f 1 (Seq.create (US.v n) (f 0sz)));
  intro_exists
    (Seq.create (US.v n) (f 0sz))
    (array_literal_inv n arr f 1);

  Loops.for_loop
    1sz
    n
    (fun i -> exists_ (array_literal_inv n arr f i))
    (array_literal_loop_body n arr f);

  let s = elim_exists () in
  A.pts_to_length arr s;
  elim_pure (array_literal_inv_pure n f (US.v n) s);
  assert (Seq.equal s (Seq.init (US.v n) (fun i -> f (US.uint_to_t i))));
  rewrite (A.pts_to arr full_perm s) _;
  return arr
val array_literal
  (#a:Type0)
  (n:US.t)
  (f:(i:US.t{US.v i < US.v n} -> a))
  : ST (A.array a)
       emp
       (fun arr ->
        A.pts_to arr full_perm (Seq.init (US.v n) (fun i -> f (US.uint_to_t i))))
       (requires US.v n > 0)
       (ensures fun arr -> A.length arr == US.v n)
let array_literal #a n f =
let arr = A.alloc (f 0sz) n in
intro_pure (array_literal_inv_pure n f 1 (Seq.create (US.v n) (f 0sz)));
intro_exists (Seq.create (US.v n) (f 0sz)) (array_literal_inv n arr f 1);
Loops.for_loop 1sz
  n
  (fun i -> exists_ (array_literal_inv n arr f i))
  (array_literal_loop_body n arr f);
let s = elim_exists () in
A.pts_to_length arr s;
elim_pure (array_literal_inv_pure n f (US.v n) s);
assert (Seq.equal s (Seq.init (US.v n) (fun i -> f (US.uint_to_t i))));
rewrite (A.pts_to arr full_perm s) _;
return arr
Steel.ST.Array.Util.fst.checked
Steel.ST.Util.fsti.checked Steel.ST.Reference.fsti.checked Steel.ST.Loops.fsti.checked Steel.ST.Effect.fsti.checked Steel.ST.Array.fsti.checked Steel.FractionalPermission.fst.checked prims.fst.checked FStar.SizeT.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked
Steel.ST.Array.Util.fst
FStar.SizeT.t Prims.b2t Prims.op_LessThan FStar.SizeT.v Steel.ST.Util.return Steel.ST.Array.array FStar.Ghost.hide FStar.Set.set Steel.Memory.iname FStar.Set.empty Steel.ST.Array.pts_to Steel.FractionalPermission.full_perm FStar.Seq.Base.init Prims.nat FStar.SizeT.uint_to_t Steel.Effect.Common.vprop Prims.unit Steel.ST.Util.rewrite FStar.Ghost.reveal FStar.Seq.Base.seq Prims._assert FStar.Seq.Base.equal Steel.ST.Util.elim_pure Steel.ST.Array.Util.array_literal_inv_pure Steel.ST.Array.pts_to_length FStar.Ghost.erased Steel.ST.Util.elim_exists Steel.Effect.Common.VStar Steel.ST.Util.pure Steel.ST.Loops.for_loop FStar.SizeT.__uint_to_t Steel.ST.Loops.nat_at_most Steel.ST.Util.exists_ Steel.ST.Array.Util.array_literal_inv Steel.ST.Array.Util.array_literal_loop_body Steel.ST.Util.intro_exists FStar.Seq.Base.create Steel.ST.Util.intro_pure Steel.ST.Array.alloc
(*
   Copyright 2021 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)

module Steel.ST.Array.Util

module G = FStar.Ghost
module US = FStar.SizeT

module R = Steel.ST.Reference
module A = Steel.ST.Array
module Loops = Steel.ST.Loops

open Steel.FractionalPermission
open Steel.ST.Effect
open Steel.ST.Util

/// Implementation of array_literal using a for loop


let array_literal_inv_pure
  (#a:Type0)
  (n:US.t)
  (f:(i:US.t{US.v i < US.v n} -> a))
  (i:Loops.nat_at_most n)
  (s:Seq.seq a)
  : prop
  = forall (j:nat).
      (j < i /\ j < Seq.length s) ==> Seq.index s j == f (US.uint_to_t j)

[@@ __reduce__]
let array_literal_inv
  (#a:Type0)
  (n:US.t)
  (arr:A.array a)
  (f:(i:US.t{US.v i < US.v n} -> a))
  (i:Loops.nat_at_most n)
  : Seq.seq a -> vprop
  = fun s ->
    A.pts_to arr full_perm s
      `star`
    pure (array_literal_inv_pure n f i s)

inline_for_extraction
let array_literal_loop_body
  (#a:Type0)
  (n:US.t)
  (arr:A.array a{A.length arr == US.v n})
  (f:(i:US.t{US.v i < US.v n} -> a))
  : i:Loops.u32_between 0sz n ->
    STT unit
        (exists_ (array_literal_inv n arr f (US.v i)))
        (fun _ -> exists_ (array_literal_inv n arr f (US.v i + 1)))
  = fun i ->
    let s = elim_exists () in
    ();
    A.pts_to_length arr s;
    elim_pure (array_literal_inv_pure n f (US.v i) s);

    A.write arr i (f i);

    intro_pure
      (array_literal_inv_pure n f (US.v i + 1) (Seq.upd s (US.v i) (f i)));
    intro_exists
      (Seq.upd s (US.v i) (f i))
      (array_literal_inv n arr f (US.v i + 1))
val array_literal
  (#a:Type0)
  (n:US.t)
  (f:(i:US.t{US.v i < US.v n} -> a))
  : ST (A.array a)
       emp
       (fun arr ->
        A.pts_to arr full_perm (Seq.init (US.v n) (fun i -> f (US.uint_to_t i))))
       (requires US.v n > 0)
       (ensures fun arr -> A.length arr == US.v n)
n: FStar.SizeT.t -> f: (i: FStar.SizeT.t{FStar.SizeT.v i < FStar.SizeT.v n} -> a)
  -> Steel.ST.Effect.ST (Steel.ST.Array.array a)