module Func_SortingBySortedness_InsertionSort
#lang-pulse

open Let_SeqLemmas_UpdShiftIsPermutation
open Let_SortedSpec_AllAbove
open Let_SortedSpec_Dominated
open Let_SortedSpec_Sorted
open Pulse
open Pulse.Lib.CSharp.Array
open Pulse.Lib.CSharp.Casts

module R = Pulse.Lib.Reference
module A = Pulse.Lib.Array
module S = Pulse.Lib.Slice
module Span = Pulse.Lib.CSharp.Span
module B = Pulse.Lib.Box
module I8 = FStar.Int8
module I16 = FStar.Int16
module I32 = FStar.Int32
module I64 = FStar.Int64
module U8 = FStar.UInt8
module U16 = FStar.UInt16
module U32 = FStar.UInt32
module U64 = FStar.UInt64
module Seq = FStar.Seq
module CS = Pulse.Lib.CSharp.Seq
module CA = Pulse.Lib.CSharp.Arith
module CL = Pulse.Lib.CSharp.List
module List = FStar.List.Tot
module Cast = FStar.Int.Cast
module D = Pulse.Lib.CSharp.Decimal
module Linq = Pulse.Lib.CSharp.Linq
module Opaque = Pulse.Lib.CSharp.Opaque

fn func_SortingBySortedness_InsertionSort (var_a: array I32.t) (#pre_a: erased (Seq.seq I32.t))
  requires A.pts_to var_a pre_a
  ensures  exists* post_a.
           A.pts_to var_a post_a **
           pure (((Seq.length post_a) == (Seq.length (reveal pre_a))) /\
           (spec_SortedSpec_Sorted post_a 0 (Seq.length post_a)) /\
           (CS.is_permutation post_a (reveal pre_a)))
{
  let mut var_i = 1l;
  while (
  let t0 = !var_i;
  let t1 = length_i32 var_a;
    (I32.lt t0 t1)
  )
  invariant exists* va_0 vi_1.
           A.pts_to var_a va_0 **
           R.pts_to var_i vi_1 **
           pure ((1 <= (I32.v vi_1)) /\
           ((Seq.length va_0) == (Seq.length (reveal pre_a))) /\
           (spec_SortedSpec_Sorted va_0 0 (I32.v vi_1)) /\
           (CS.is_permutation va_0 (reveal pre_a)))
  decreases ((pow2 31 - (I32.v !var_i)))
  {
    let t2 = !var_i;
    let t3 = read var_a t2;
    let mut var_key = t3;
    let t4 = !var_i;
    let mut var_j = (I32.sub t4 1l);
    with vi_3 vkey_5. assert (R.pts_to var_i vi_3 ** R.pts_to var_key vkey_5);
    while (
    let t5 = !var_j;
    let t10 = if ((I32.gte t5 0l)) {
    let t6 = !var_j;
    let t7 = read var_a t6;
    let t8 = !var_key;
      (I32.gt t7 t8)
    } else {
    let t9 = false;
      t9
    };
      t10
    )
    invariant exists* va_2 vj_4.
           A.pts_to var_a va_2 **
           R.pts_to var_i vi_3 **
           R.pts_to var_j vj_4 **
           R.pts_to var_key vkey_5 **
           pure ((((0 - 1) <= (I32.v vj_4)) /\ ((I32.v vj_4) < (I32.v vi_3))) /\
           ((I32.v vi_3) < (Seq.length va_2)) /\
           ((Seq.length va_2) == (Seq.length (reveal pre_a))) /\
           (spec_SortedSpec_Sorted va_2 0 ((I32.v vj_4) + 1)) /\
           (spec_SortedSpec_Sorted va_2 ((I32.v vj_4) + 2) ((I32.v vi_3) + 1)) /\
           (spec_SortedSpec_AllAbove va_2 ((I32.v vj_4) + 2) ((I32.v vi_3) + 1) (I32.v vkey_5)) /\
           (spec_SortedSpec_Dominated va_2 0 ((I32.v vj_4) + 1) ((I32.v vj_4) + 2) ((I32.v vi_3) + 1)) /\
           (CS.is_permutation (Seq.upd va_2 ((I32.v vj_4) + 1) vkey_5) (reveal pre_a)))
    decreases (((I32.v !var_j) + 1))
    {
      with va_6 vi_7 vkey_8 vj_9. assert (A.pts_to var_a va_6 ** R.pts_to var_i vi_7 ** R.pts_to var_key vkey_8 ** R.pts_to var_j vj_9);
      Let_SeqLemmas_UpdShiftIsPermutation.lemma_SeqLemmas_UpdShiftIsPermutation va_6 vj_9 vkey_8;
      let t11 = !var_j;
      let t12 = !var_j;
      let t13 = read var_a t12;
      write var_a (I32.add t11 1l) t13;
      with va_10 vi_11 vkey_12 vj_13. assert (A.pts_to var_a va_10 ** R.pts_to var_i vi_11 ** R.pts_to var_key vkey_12 ** R.pts_to var_j vj_13);
      assert (pure ((spec_SortedSpec_Sorted va_10 0 (I32.v vj_13))));
      with va_14 vi_15 vkey_16 vj_17. assert (A.pts_to var_a va_14 ** R.pts_to var_i vi_15 ** R.pts_to var_key vkey_16 ** R.pts_to var_j vj_17);
      assert (pure ((spec_SortedSpec_Sorted va_14 ((I32.v vj_17) + 1) ((I32.v vi_15) + 1))));
      with va_18 vi_19 vkey_20 vj_21. assert (A.pts_to var_a va_18 ** R.pts_to var_i vi_19 ** R.pts_to var_key vkey_20 ** R.pts_to var_j vj_21);
      assert (pure ((spec_SortedSpec_AllAbove va_18 ((I32.v vj_21) + 1) ((I32.v vi_19) + 1) (I32.v vkey_20))));
      with va_22 vi_23 vkey_24 vj_25. assert (A.pts_to var_a va_22 ** R.pts_to var_i vi_23 ** R.pts_to var_key vkey_24 ** R.pts_to var_j vj_25);
      assert (pure ((spec_SortedSpec_Dominated va_22 0 (I32.v vj_25) ((I32.v vj_25) + 1) ((I32.v vi_23) + 1))));
      let t14 = !var_j;
      var_j := (I32.sub t14 1l);
      ()
    };
    let t15 = !var_j;
    let t16 = !var_key;
    write var_a (I32.add t15 1l) t16;
    let t17 = !var_i;
    var_i := (I32.add t17 1l);
    ()
  };
  ()
}