heapsort_generic.coma

module M_heap_frag_max
  use seq.Seq
  use int.ComputerDivision
  use int.Int
  
  type t_T
  
  function parent (i: int) : int = ComputerDivision.div (i + 1) 2 - 1
  
  type t_Ordering = Less | Equal | Greater
  
  function cmp_log_T (self: t_T) (other: t_T) : t_Ordering
  
  function eq_cmp_T (x: t_T) (y: t_T) : ()
  
  axiom eq_cmp_T_spec: forall x: t_T, y: t_T. (x = y) = (cmp_log_T x y = Equal)
  
  function antisym2_T (x: t_T) (y: t_T) : ()
  
  axiom antisym2_T_spec: forall x: t_T, y: t_T. cmp_log_T x y = Greater -> cmp_log_T y x = Less
  
  function antisym1_T (x: t_T) (y: t_T) : ()
  
  axiom antisym1_T_spec: forall x: t_T, y: t_T. cmp_log_T x y = Less -> cmp_log_T y x = Greater
  
  function trans_T (x: t_T) (y: t_T) (z: t_T) (o: t_Ordering) : ()
  
  axiom trans_T_spec: forall x: t_T, y: t_T, z: t_T, o: t_Ordering. cmp_log_T x y = o
      -> cmp_log_T y z = o -> cmp_log_T x z = o
  
  function refl_T (x: t_T) : ()
  
  axiom refl_T_spec: forall x: t_T. cmp_log_T x x = Equal
  
  predicate gt_log_T (self: t_T) (o: t_T)
  
  function cmp_gt_log_T (x: t_T) (y: t_T) : ()
  
  axiom cmp_gt_log_T_spec: forall x: t_T, y: t_T. gt_log_T x y = (cmp_log_T x y = Greater)
  
  predicate ge_log_T (self: t_T) (o: t_T)
  
  function cmp_ge_log_T (x: t_T) (y: t_T) : ()
  
  axiom cmp_ge_log_T_spec: forall x: t_T, y: t_T. ge_log_T x y = (cmp_log_T x y <> Less)
  
  predicate lt_log_T (self: t_T) (o: t_T)
  
  function cmp_lt_log_T (x: t_T) (y: t_T) : ()
  
  axiom cmp_lt_log_T_spec: forall x: t_T, y: t_T. lt_log_T x y = (cmp_log_T x y = Less)
  
  predicate le_log_T (self: t_T) (o: t_T)
  
  function cmp_le_log_T (x: t_T) (y: t_T) : ()
  
  axiom cmp_le_log_T_spec: forall x: t_T, y: t_T. le_log_T x y = (cmp_log_T x y <> Greater)
  
  predicate heap_frag_T (s: Seq.seq t_T) (start: int) (end': int) =
    forall i: int. start <= parent i /\ i < end' -> le_log_T (Seq.get s i) (Seq.get s (parent i))
  
  predicate well_founded_relation_Int [@inline:trivial] (self: int) (other: int) = self >= 0 /\ self > other
  
  meta "rewrite_def" predicate well_founded_relation_Int
  
  meta "compute_max_steps" 1000000
  
  meta "select_lsinst" "all"
  
  constant s : Seq.seq t_T
  
  constant i : int
  
  constant end' : int
  
  function heap_frag_max_T (s: Seq.seq t_T) (i: int) (end': int) : ()
  
  goal vc_heap_frag_max_T: heap_frag_T s 0 end'
    -> 0 <= i /\ i < end'
    -> (if i > 0 then
      (([@stop_split] [@expl:heap_frag_max requires] ([@stop_split] [@expl:heap_frag_max requires #0] heap_frag_T s 0 end')
          /\ ([@stop_split] [@expl:heap_frag_max requires #1] 0 <= parent i /\ parent i < end'))
        /\ ([@expl:variant decreases] well_founded_relation_Int i (parent i)))
      /\ (([@stop_split] [@expl:heap_frag_max ensures] le_log_T (Seq.get s (parent i)) (Seq.get s 0))
      -> ([@stop_split] [@expl:heap_frag_max ensures] le_log_T (Seq.get s i) (Seq.get s 0)))
    else
      [@stop_split] [@expl:heap_frag_max ensures] le_log_T (Seq.get s i) (Seq.get s 0)
    )
end
module M_sift_down
  use creusot.prelude.MutBorrow
  use creusot.int.UInt64
  use int.ComputerDivision
  use seq.Seq
  use seq.Permut
  use creusot.slice.Slice64
  use creusot.prelude.Any
  use int.Int
  
  function parent (i: int) : int = ComputerDivision.div (i + 1) 2 - 1
  
  type t_DeepModelTy
  
  type t_Ordering = Less | Equal | Greater
  
  function cmp_log_DeepModelTy (self: t_DeepModelTy) (other: t_DeepModelTy) : t_Ordering
  
  function eq_cmp_DeepModelTy (x: t_DeepModelTy) (y: t_DeepModelTy) : ()
  
  axiom eq_cmp_DeepModelTy_spec: forall x: t_DeepModelTy, y: t_DeepModelTy. (x = y) = (cmp_log_DeepModelTy x y = Equal)
  
  function antisym2_DeepModelTy (x: t_DeepModelTy) (y: t_DeepModelTy) : ()
  
  axiom antisym2_DeepModelTy_spec: forall x: t_DeepModelTy, y: t_DeepModelTy. cmp_log_DeepModelTy x y = Greater
      -> cmp_log_DeepModelTy y x = Less
  
  function antisym1_DeepModelTy (x: t_DeepModelTy) (y: t_DeepModelTy) : ()
  
  axiom antisym1_DeepModelTy_spec: forall x: t_DeepModelTy, y: t_DeepModelTy. cmp_log_DeepModelTy x y = Less
      -> cmp_log_DeepModelTy y x = Greater
  
  function trans_DeepModelTy (x: t_DeepModelTy) (y: t_DeepModelTy) (z: t_DeepModelTy) (o: t_Ordering) : ()
  
  axiom trans_DeepModelTy_spec:
    forall x: t_DeepModelTy, y: t_DeepModelTy, z: t_DeepModelTy, o: t_Ordering. cmp_log_DeepModelTy x y = o
      -> cmp_log_DeepModelTy y z = o -> cmp_log_DeepModelTy x z = o
  
  function refl_DeepModelTy (x: t_DeepModelTy) : ()
  
  axiom refl_DeepModelTy_spec: forall x: t_DeepModelTy. cmp_log_DeepModelTy x x = Equal
  
  predicate gt_log_DeepModelTy (self: t_DeepModelTy) (o: t_DeepModelTy)
  
  function cmp_gt_log_DeepModelTy (x: t_DeepModelTy) (y: t_DeepModelTy) : ()
  
  axiom cmp_gt_log_DeepModelTy_spec: forall x: t_DeepModelTy, y: t_DeepModelTy. gt_log_DeepModelTy x y
      = (cmp_log_DeepModelTy x y = Greater)
  
  predicate ge_log_DeepModelTy (self: t_DeepModelTy) (o: t_DeepModelTy)
  
  function cmp_ge_log_DeepModelTy (x: t_DeepModelTy) (y: t_DeepModelTy) : ()
  
  axiom cmp_ge_log_DeepModelTy_spec: forall x: t_DeepModelTy, y: t_DeepModelTy. ge_log_DeepModelTy x y
      = (cmp_log_DeepModelTy x y <> Less)
  
  predicate lt_log_DeepModelTy (self: t_DeepModelTy) (o: t_DeepModelTy)
  
  function cmp_lt_log_DeepModelTy (x: t_DeepModelTy) (y: t_DeepModelTy) : ()
  
  axiom cmp_lt_log_DeepModelTy_spec: forall x: t_DeepModelTy, y: t_DeepModelTy. lt_log_DeepModelTy x y
      = (cmp_log_DeepModelTy x y = Less)
  
  predicate le_log_DeepModelTy (self: t_DeepModelTy) (o: t_DeepModelTy)
  
  function cmp_le_log_DeepModelTy (x: t_DeepModelTy) (y: t_DeepModelTy) : ()
  
  axiom cmp_le_log_DeepModelTy_spec: forall x: t_DeepModelTy, y: t_DeepModelTy. le_log_DeepModelTy x y
      = (cmp_log_DeepModelTy x y <> Greater)
  
  type t_Vec_T_Global
  
  type t_T
  
  constant const_MAX: UInt64.t = (18446744073709551615: UInt64.t)
  
  function view_Vec_T_Global (self: t_Vec_T_Global) : Seq.seq t_T
  
  axiom view_Vec_T_Global_spec: forall self: t_Vec_T_Global. Seq.length (view_Vec_T_Global self)
      <= UInt64.t'int const_MAX
  
  function deep_model_T (self: t_T) : t_DeepModelTy
  
  function index_Vec_T_Global [@inline:trivial] (self: t_Vec_T_Global) (ix: int) : t_T =
    Seq.get (view_Vec_T_Global self) ix
  
  meta "rewrite_def" function index_Vec_T_Global
  
  function deep_model_Vec_T_Global (self: t_Vec_T_Global) : Seq.seq t_DeepModelTy
  
  axiom deep_model_Vec_T_Global_spec: forall self: t_Vec_T_Global. Seq.length (view_Vec_T_Global self)
      = Seq.length (deep_model_Vec_T_Global self)
  
  axiom deep_model_Vec_T_Global_spec'0: forall self: t_Vec_T_Global. forall i: int. 0 <= i
          /\ i < Seq.length (view_Vec_T_Global self)
        -> Seq.get (deep_model_Vec_T_Global self) i = deep_model_T (index_Vec_T_Global self i)
  
  function deep_model_refmut_Vec_T_Global [@inline:trivial] (self: MutBorrow.t t_Vec_T_Global) : Seq.seq t_DeepModelTy =
    deep_model_Vec_T_Global self.current
  
  meta "rewrite_def" function deep_model_refmut_Vec_T_Global
  
  predicate permutation_of_T (self: Seq.seq t_T) (other: Seq.seq t_T) = Permut.permut self other 0 (Seq.length self)
  
  predicate inv_T (_1: t_T)
  
  predicate invariant_ref_T [@inline:trivial] (self: t_T) = inv_T self
  
  meta "rewrite_def" predicate invariant_ref_T
  
  predicate inv_ref_T [@inline:trivial] (_1: t_T) = invariant_ref_T _1
  
  meta "rewrite_def" predicate inv_ref_T
  
  predicate invariant_Seq_T [@inline:trivial] (self: Seq.seq t_T) =
    forall i: int. 0 <= i /\ i < Seq.length self -> inv_ref_T (Seq.get self i)
  
  meta "rewrite_def" predicate invariant_Seq_T
  
  predicate inv_Seq_T [@inline:trivial] (_1: Seq.seq t_T) = invariant_Seq_T _1
  
  meta "rewrite_def" predicate inv_Seq_T
  
  predicate invariant_Vec_T_Global (self: t_Vec_T_Global) = inv_Seq_T (view_Vec_T_Global self)
  
  predicate inv_Vec_T_Global (_1: t_Vec_T_Global)
  
  axiom inv_axiom: forall x: t_Vec_T_Global [inv_Vec_T_Global x]. inv_Vec_T_Global x -> invariant_Vec_T_Global x
  
  predicate invariant_refmut_Vec_T_Global [@inline:trivial] (self: MutBorrow.t t_Vec_T_Global) =
    inv_Vec_T_Global self.current /\ inv_Vec_T_Global self.final
  
  meta "rewrite_def" predicate invariant_refmut_Vec_T_Global
  
  predicate inv_refmut_Vec_T_Global [@inline:trivial] (_1: MutBorrow.t t_Vec_T_Global) =
    invariant_refmut_Vec_T_Global _1
  
  meta "rewrite_def" predicate inv_refmut_Vec_T_Global
  
  predicate invariant_ref_Vec_T_Global [@inline:trivial] (self: t_Vec_T_Global) = inv_Vec_T_Global self
  
  meta "rewrite_def" predicate invariant_ref_Vec_T_Global
  
  predicate inv_ref_Vec_T_Global [@inline:trivial] (_1: t_Vec_T_Global) = invariant_ref_Vec_T_Global _1
  
  meta "rewrite_def" predicate inv_ref_Vec_T_Global
  
  predicate in_bounds_usize [@inline:trivial] (self: UInt64.t) (seq: Seq.seq t_T) = UInt64.t'int self < Seq.length seq
  
  meta "rewrite_def" predicate in_bounds_usize
  
  predicate has_value_usize [@inline:trivial] (self: UInt64.t) (seq: Seq.seq t_T) (out: t_T) =
    Seq.get seq (UInt64.t'int self) = out
  
  meta "rewrite_def" predicate has_value_usize
  
  let rec index_Vec_T_Global'0 (self_: t_Vec_T_Global) (ix: UInt64.t) (return (x: t_T)) =
    {[@stop_split] [@expl:index_Vec_T_Global requires] ([@stop_split] [@expl:index 'self_' type invariant] inv_ref_Vec_T_Global self_)
    /\ ([@stop_split] [@expl:index requires] in_bounds_usize ix (view_Vec_T_Global self_))}
    any
    [ return (result: t_T) ->
    {[@stop_split] [@expl:index_Vec_T_Global ensures] ([@stop_split] [@expl:index result type invariant] inv_ref_T result)
      /\ ([@stop_split] [@expl:index ensures] has_value_usize ix (view_Vec_T_Global self_) result)}
      (! return {result}) ]
  
  type tup2_ref_T_ref_T = { f0: t_T; f1: t_T }
  
  predicate precondition_lt (self: ()) (args: tup2_ref_T_ref_T)
  
  axiom precondition_fndef:
    forall args: tup2_ref_T_ref_T [precondition_lt () args]. (let {f0 = self_; f1 = other} = args in inv_ref_T self_
        /\ inv_ref_T other) -> precondition_lt () args
  
  function deep_model_ref_T [@inline:trivial] (self: t_T) : t_DeepModelTy = deep_model_T self
  
  meta "rewrite_def" function deep_model_ref_T
  
  predicate postcondition_once_lt (self: ()) (args: tup2_ref_T_ref_T) (result: bool)
  
  axiom postcondition_fndef:
    forall args: tup2_ref_T_ref_T, res: bool [postcondition_once_lt () args res]. postcondition_once_lt () args res
      -> (let {f0 = self_; f1 = other} = args in res
      = lt_log_DeepModelTy (deep_model_ref_T self_) (deep_model_ref_T other))
  
  let rec lt_T (self_: t_T) (other: t_T) (return (x: bool)) =
    {[@stop_split] [@expl:lt requires] precondition_lt () { f0 = self_; f1 = other }}
    any
    [ return (result: bool) -> {[@stop_split] [@expl:lt ensures] postcondition_once_lt () { f0 = self_;
                                                                                            f1 = other } result}
      (! return {result}) ]
  
  predicate precondition_le (self: ()) (args: tup2_ref_T_ref_T)
  
  axiom precondition_fndef'0:
    forall args: tup2_ref_T_ref_T [precondition_le () args]. (let {f0 = self_; f1 = other} = args in inv_ref_T self_
        /\ inv_ref_T other) -> precondition_le () args
  
  predicate postcondition_once_le (self: ()) (args: tup2_ref_T_ref_T) (result: bool)
  
  axiom postcondition_fndef'0:
    forall args: tup2_ref_T_ref_T, res: bool [postcondition_once_le () args res]. postcondition_once_le () args res
      -> (let {f0 = self_; f1 = other} = args in res
      = le_log_DeepModelTy (deep_model_ref_T self_) (deep_model_ref_T other))
  
  let rec le_T (self_: t_T) (other: t_T) (return (x: bool)) =
    {[@stop_split] [@expl:le requires] precondition_le () { f0 = self_; f1 = other }}
    any
    [ return (result: bool) -> {[@stop_split] [@expl:le ensures] postcondition_once_le () { f0 = self_;
                                                                                            f1 = other } result}
      (! return {result}) ]
  
  predicate invariant_slice_T (self: Slice64.slice t_T) = inv_Seq_T (Slice64.view self)
  
  predicate inv_slice_T [@inline:trivial] (_1: Slice64.slice t_T) = invariant_slice_T _1
  
  meta "rewrite_def" predicate inv_slice_T
  
  predicate invariant_refmut_slice_T [@inline:trivial] (self: MutBorrow.t (Slice64.slice t_T)) =
    inv_slice_T self.current /\ inv_slice_T self.final
  
  meta "rewrite_def" predicate invariant_refmut_slice_T
  
  predicate inv_refmut_slice_T [@inline:trivial] (_1: MutBorrow.t (Slice64.slice t_T)) = invariant_refmut_slice_T _1
  
  meta "rewrite_def" predicate inv_refmut_slice_T
  
  let rec deref_mut_Vec_T_Global (self_: MutBorrow.t t_Vec_T_Global) (return (x: MutBorrow.t (Slice64.slice t_T))) =
    {[@stop_split] [@expl:deref_mut 'self_' type invariant] inv_refmut_Vec_T_Global self_}
    any
    [ return (result: MutBorrow.t (Slice64.slice t_T)) ->
    {[@stop_split] [@expl:deref_mut_Vec_T_Global ensures] ([@stop_split] [@expl:deref_mut result type invariant] inv_refmut_slice_T result)
      /\ ([@stop_split] [@expl:deref_mut ensures #0] Slice64.view result.current = view_Vec_T_Global self_.current)
      /\ ([@stop_split] [@expl:deref_mut ensures #1] Seq.length (view_Vec_T_Global self_.final)
        = Seq.length (view_Vec_T_Global self_.current))
      /\ ([@stop_split] [@expl:deref_mut ensures #2] Slice64.view result.final = view_Vec_T_Global self_.final)}
      (! return {result}) ]
  
  let rec swap_T (self_: MutBorrow.t (Slice64.slice t_T)) (i: UInt64.t) (j: UInt64.t) (return (x: ())) =
    {[@stop_split] [@expl:swap_T requires] ([@stop_split] [@expl:swap 'self_' type invariant] inv_refmut_slice_T self_)
    /\ ([@stop_split] [@expl:swap requires #0] UInt64.t'int i < Seq.length (Slice64.view self_.current))
    /\ ([@stop_split] [@expl:swap requires #1] UInt64.t'int j < Seq.length (Slice64.view self_.current))}
    any
    [ return (result: ()) ->
    {[@stop_split] [@expl:swap ensures] Permut.exchange (Slice64.view self_.final) (Slice64.view self_.current) (UInt64.t'int i) (UInt64.t'int j)}
      (! return {result}) ]
  
  predicate resolve_refmut_slice_T [@inline:trivial] (_1: MutBorrow.t (Slice64.slice t_T)) = _1.final = _1.current
  
  meta "rewrite_def" predicate resolve_refmut_slice_T
  
  predicate resolve_refmut_Vec_T_Global [@inline:trivial] (_1: MutBorrow.t t_Vec_T_Global) = _1.final = _1.current
  
  meta "rewrite_def" predicate resolve_refmut_Vec_T_Global
  
  predicate heap_frag_DeepModelTy (s: Seq.seq t_DeepModelTy) (start: int) (end': int) =
    forall i: int. start <= parent i /\ i < end' -> le_log_DeepModelTy (Seq.get s i) (Seq.get s (parent i))
  
  meta "compute_max_steps" 1000000
  
  meta "select_lsinst" "all"
  
  let rec sift_down_T (v: MutBorrow.t t_Vec_T_Global) (start: UInt64.t) (end': UInt64.t) (return (x: ())) =
    {[@stop_split] [@expl:sift_down_T requires] ([@stop_split] [@expl:sift_down 'v' type invariant] inv_refmut_Vec_T_Global v)
    /\ ([@stop_split] [@expl:sift_down requires #0] heap_frag_DeepModelTy (deep_model_refmut_Vec_T_Global v) (UInt64.t'int start
      + 1) (UInt64.t'int end'))
    /\ ([@stop_split] [@expl:sift_down requires #1] UInt64.t'int start < UInt64.t'int end')
    /\ ([@stop_split] [@expl:sift_down requires #2] UInt64.t'int end' <= Seq.length (view_Vec_T_Global v.current))}
    (! bb0
    [ bb0 = s0 [ s0 = [ &old_v <- v ] s1 | s1 = [ &i <- start ] s2 | s2 = [ &_old <- v.final ] s3 | s3 = bb2 ]
    | bb2 = bb2
      [ bb2 = {[@expl:inferred invariant: type invariant] inv_refmut_Vec_T_Global v}
        {[@expl:inferred invariant: unchanged value] _old = v.final}
        {[@expl:loop invariant #0] permutation_of_T (view_Vec_T_Global v.current) (view_Vec_T_Global old_v.current)}
        {[@expl:loop invariant #1] UInt64.t'int start <= UInt64.t'int i /\ UInt64.t'int i < UInt64.t'int end'}
        {[@expl:loop invariant #2] forall j: int. 0 <= j /\ j < UInt64.t'int start
            \/ UInt64.t'int end' <= j /\ j < Seq.length (view_Vec_T_Global v.current)
          -> index_Vec_T_Global old_v.current j = index_Vec_T_Global v.current j}
        {[@expl:loop invariant #3] forall m: t_DeepModelTy. (forall j: int. UInt64.t'int start <= j
                /\ j < UInt64.t'int end' -> le_log_DeepModelTy (Seq.get (deep_model_refmut_Vec_T_Global old_v) j) m)
          -> (forall j: int. UInt64.t'int start <= j /\ j < UInt64.t'int end'
            -> le_log_DeepModelTy (Seq.get (deep_model_refmut_Vec_T_Global v) j) m)}
        {[@expl:loop invariant #4] forall j: int. UInt64.t'int start <= parent j
            /\ j < UInt64.t'int end' /\ UInt64.t'int i <> parent j
          -> le_log_DeepModelTy (Seq.get (deep_model_refmut_Vec_T_Global v) j) (Seq.get (deep_model_refmut_Vec_T_Global v) (parent j))}
        {[@expl:loop invariant #5] let c = 2 * UInt64.t'int i + 1 in c < UInt64.t'int end'
          /\ UInt64.t'int start <= parent (UInt64.t'int i)
        -> le_log_DeepModelTy (Seq.get (deep_model_refmut_Vec_T_Global v) c) (Seq.get (deep_model_refmut_Vec_T_Global v) (parent (parent c)))}
        {[@expl:loop invariant #6] let c = 2 * UInt64.t'int i + 2 in c < UInt64.t'int end'
          /\ UInt64.t'int start <= parent (UInt64.t'int i)
        -> le_log_DeepModelTy (Seq.get (deep_model_refmut_Vec_T_Global v) c) (Seq.get (deep_model_refmut_Vec_T_Global v) (parent (parent c)))}
        (! s0)
        [ s0 = [ &_72 <- (2: UInt64.t) = (0: UInt64.t) ] s1
        | s1 = {[@expl:division by zero] not _72} s2
        | s2 = UInt64.div {end'} {(2: UInt64.t)} (fun (_x: UInt64.t) -> [ &_70 <- _x ] s3)
        | s3 = [ &_68 <- UInt64.ge i _70 ] s4
        | s4 = any [ br0 -> {_68 = false} (! bb6) | br1 -> {_68} (! bb5) ] ]
        [ bb6 = s0
          [ s0 = UInt64.mul {(2: UInt64.t)} {i} (fun (_x: UInt64.t) -> [ &_75 <- _x ] s1)
          | s1 = UInt64.add {_75} {(1: UInt64.t)} (fun (_x: UInt64.t) -> [ &child <- _x ] s2)
          | s2 = UInt64.add {child} {(1: UInt64.t)} (fun (_x: UInt64.t) -> [ &_79 <- _x ] s3)
          | s3 = [ &_78 <- UInt64.lt _79 end' ] s4
          | s4 = any [ br0 -> {_78 = false} (! bb15) | br1 -> {_78} (! bb7) ] ]
        | bb7 = s0
          [ s0 = index_Vec_T_Global'0 {v.current} {child} (fun (_x: t_T) -> [ &_84 <- _x ] s1)
          | s1 = UInt64.add {child} {(1: UInt64.t)} (fun (_x: UInt64.t) -> [ &_90 <- _x ] s2)
          | s2 = index_Vec_T_Global'0 {v.current} {_90} (fun (_x: t_T) -> [ &_88 <- _x ] s3)
          | s3 = lt_T {_84} {_88} (fun (_x: bool) -> [ &_82 <- _x ] s4)
          | s4 = any [ br0 -> {_82 = false} (! bb15) | br1 -> {_82} (! bb12) ] ]
        | bb12 = s0 [ s0 = UInt64.add {child} {(1: UInt64.t)} (fun (_x: UInt64.t) -> [ &child <- _x ] s1) | s1 = bb15 ]
        | bb15 = s0
          [ s0 = index_Vec_T_Global'0 {v.current} {child} (fun (_x: t_T) -> [ &_95 <- _x ] s1)
          | s1 = index_Vec_T_Global'0 {v.current} {i} (fun (_x: t_T) -> [ &_99 <- _x ] s2)
          | s2 = le_T {_95} {_99} (fun (_x: bool) -> [ &_93 <- _x ] s3)
          | s3 = any [ br0 -> {_93 = false} (! bb20) | br1 -> {_93} (! bb19) ] ]
        | bb20 = s0
          [ s0 = MutBorrow.borrow_mut <t_Vec_T_Global> {v.current}
              (fun (_bor: MutBorrow.t t_Vec_T_Global) ->
                [ &_106 <- _bor ] -{inv_Vec_T_Global _bor.final}-
                [ &v <- { v with current = _bor.final } ] s1)
            [ _ck -> (! {[@expl:type invariant] inv_Vec_T_Global v.current} any) ]
          | s1 = deref_mut_Vec_T_Global {_106} (fun (_x: MutBorrow.t (Slice64.slice t_T)) -> [ &_105 <- _x ] s2)
          | s2 = MutBorrow.borrow_final <Slice64.slice t_T> {_105.current} {MutBorrow.get_id _105}
              (fun (_bor: MutBorrow.t (Slice64.slice t_T)) ->
                [ &_104 <- _bor ] -{inv_slice_T _bor.final}-
                [ &_105 <- { _105 with current = _bor.final } ] s3)
            [ _ck -> (! {[@expl:type invariant] inv_slice_T _105.current} any) ]
          | s3 = swap_T {_104} {i} {child} (fun (_x: ()) -> [ &_103 <- _x ] s4)
          | s4 = s5 [ _ck -> (! {[@expl:type invariant] inv_refmut_slice_T _105} any) ]
          | s5 = -{resolve_refmut_slice_T _105}- s6
          | s6 = [ &i <- child ] s7
          | s7 = bb2 ] ] ]
    | bb5 = s0
      [ s0 = s1 [ _ck -> (! {[@expl:type invariant] inv_refmut_Vec_T_Global v} any) ]
      | s1 = -{resolve_refmut_Vec_T_Global v}- s2
      | s2 = return {_ret} ]
    | bb19 = s0
      [ s0 = s1 [ _ck -> (! {[@expl:type invariant] inv_refmut_Vec_T_Global v} any) ]
      | s1 = -{resolve_refmut_Vec_T_Global v}- s2
      | s2 = return {_ret} ] ]
    [ & _ret: () = Any.any_l ()
    | & v: MutBorrow.t t_Vec_T_Global = v
    | & start: UInt64.t = start
    | & end': UInt64.t = end'
    | & old_v: MutBorrow.t t_Vec_T_Global = Any.any_l ()
    | & i: UInt64.t = Any.any_l ()
    | & _68: bool = Any.any_l ()
    | & _70: UInt64.t = Any.any_l ()
    | & _72: bool = Any.any_l ()
    | & child: UInt64.t = Any.any_l ()
    | & _75: UInt64.t = Any.any_l ()
    | & _78: bool = Any.any_l ()
    | & _79: UInt64.t = Any.any_l ()
    | & _82: bool = Any.any_l ()
    | & _84: t_T = Any.any_l ()
    | & _88: t_T = Any.any_l ()
    | & _90: UInt64.t = Any.any_l ()
    | & _93: bool = Any.any_l ()
    | & _95: t_T = Any.any_l ()
    | & _99: t_T = Any.any_l ()
    | & _103: () = Any.any_l ()
    | & _104: MutBorrow.t (Slice64.slice t_T) = Any.any_l ()
    | & _105: MutBorrow.t (Slice64.slice t_T) = Any.any_l ()
    | & _106: MutBorrow.t t_Vec_T_Global = Any.any_l ()
    | & _old: t_Vec_T_Global = Any.any_l () ])
    [ return (result: ()) ->
    {[@stop_split] [@expl:sift_down_T ensures] ([@stop_split] [@expl:sift_down ensures #0] heap_frag_DeepModelTy (deep_model_Vec_T_Global v.final) (UInt64.t'int start) (UInt64.t'int end'))
      /\ ([@stop_split] [@expl:sift_down ensures #1] permutation_of_T (view_Vec_T_Global v.final) (view_Vec_T_Global v.current))
      /\ ([@stop_split] [@expl:sift_down ensures #2] forall i: int. 0 <= i /\ i < UInt64.t'int start
            \/ UInt64.t'int end' <= i /\ i < Seq.length (view_Vec_T_Global v.current)
          -> index_Vec_T_Global v.current i = index_Vec_T_Global v.final i)
      /\ ([@stop_split] [@expl:sift_down ensures #3] forall m: t_DeepModelTy. (forall j: int. UInt64.t'int start <= j
              /\ j < UInt64.t'int end' -> le_log_DeepModelTy (Seq.get (deep_model_refmut_Vec_T_Global v) j) m)
        -> (forall j: int. UInt64.t'int start <= j /\ j < UInt64.t'int end'
          -> le_log_DeepModelTy (Seq.get (deep_model_Vec_T_Global v.final) j) m))}
      (! return {result}) ]
end
module M_heap_sort
  use creusot.int.UInt64
  use seq.Seq
  use creusot.prelude.MutBorrow
  use int.ComputerDivision
  use seq.Permut
  use creusot.slice.Slice64
  use creusot.prelude.Any
  use int.Int
  
  type t_Vec_T_Global
  
  type t_T
  
  predicate inv_T (_1: t_T)
  
  predicate invariant_ref_T [@inline:trivial] (self: t_T) = inv_T self
  
  meta "rewrite_def" predicate invariant_ref_T
  
  predicate inv_ref_T [@inline:trivial] (_1: t_T) = invariant_ref_T _1
  
  meta "rewrite_def" predicate inv_ref_T
  
  predicate invariant_Seq_T [@inline:trivial] (self: Seq.seq t_T) =
    forall i: int. 0 <= i /\ i < Seq.length self -> inv_ref_T (Seq.get self i)
  
  meta "rewrite_def" predicate invariant_Seq_T
  
  predicate inv_Seq_T [@inline:trivial] (_1: Seq.seq t_T) = invariant_Seq_T _1
  
  meta "rewrite_def" predicate inv_Seq_T
  
  constant const_MAX: UInt64.t = (18446744073709551615: UInt64.t)
  
  function view_Vec_T_Global (self: t_Vec_T_Global) : Seq.seq t_T
  
  axiom view_Vec_T_Global_spec: forall self: t_Vec_T_Global. Seq.length (view_Vec_T_Global self)
      <= UInt64.t'int const_MAX
  
  predicate invariant_Vec_T_Global (self: t_Vec_T_Global) = inv_Seq_T (view_Vec_T_Global self)
  
  predicate inv_Vec_T_Global (_1: t_Vec_T_Global)
  
  axiom inv_axiom: forall x: t_Vec_T_Global [inv_Vec_T_Global x]. inv_Vec_T_Global x -> invariant_Vec_T_Global x
  
  predicate invariant_ref_Vec_T_Global [@inline:trivial] (self: t_Vec_T_Global) = inv_Vec_T_Global self
  
  meta "rewrite_def" predicate invariant_ref_Vec_T_Global
  
  predicate inv_ref_Vec_T_Global [@inline:trivial] (_1: t_Vec_T_Global) = invariant_ref_Vec_T_Global _1
  
  meta "rewrite_def" predicate inv_ref_Vec_T_Global
  
  let rec len_T (self_: t_Vec_T_Global) (return (x: UInt64.t)) =
    {[@stop_split] [@expl:len 'self_' type invariant] inv_ref_Vec_T_Global self_}
    any
    [ return (result: UInt64.t) -> {[@stop_split] [@expl:len ensures] UInt64.t'int result
      = Seq.length (view_Vec_T_Global self_)}
      (! return {result}) ]
  
  type t_DeepModelTy
  
  function parent (i: int) : int = ComputerDivision.div (i + 1) 2 - 1
  
  type t_Ordering = Less | Equal | Greater
  
  function cmp_log_DeepModelTy (self: t_DeepModelTy) (other: t_DeepModelTy) : t_Ordering
  
  function eq_cmp_DeepModelTy (x: t_DeepModelTy) (y: t_DeepModelTy) : ()
  
  axiom eq_cmp_DeepModelTy_spec: forall x: t_DeepModelTy, y: t_DeepModelTy. (x = y) = (cmp_log_DeepModelTy x y = Equal)
  
  function antisym2_DeepModelTy (x: t_DeepModelTy) (y: t_DeepModelTy) : ()
  
  axiom antisym2_DeepModelTy_spec: forall x: t_DeepModelTy, y: t_DeepModelTy. cmp_log_DeepModelTy x y = Greater
      -> cmp_log_DeepModelTy y x = Less
  
  function antisym1_DeepModelTy (x: t_DeepModelTy) (y: t_DeepModelTy) : ()
  
  axiom antisym1_DeepModelTy_spec: forall x: t_DeepModelTy, y: t_DeepModelTy. cmp_log_DeepModelTy x y = Less
      -> cmp_log_DeepModelTy y x = Greater
  
  function trans_DeepModelTy (x: t_DeepModelTy) (y: t_DeepModelTy) (z: t_DeepModelTy) (o: t_Ordering) : ()
  
  axiom trans_DeepModelTy_spec:
    forall x: t_DeepModelTy, y: t_DeepModelTy, z: t_DeepModelTy, o: t_Ordering. cmp_log_DeepModelTy x y = o
      -> cmp_log_DeepModelTy y z = o -> cmp_log_DeepModelTy x z = o
  
  function refl_DeepModelTy (x: t_DeepModelTy) : ()
  
  axiom refl_DeepModelTy_spec: forall x: t_DeepModelTy. cmp_log_DeepModelTy x x = Equal
  
  predicate gt_log_DeepModelTy (self: t_DeepModelTy) (o: t_DeepModelTy)
  
  function cmp_gt_log_DeepModelTy (x: t_DeepModelTy) (y: t_DeepModelTy) : ()
  
  axiom cmp_gt_log_DeepModelTy_spec: forall x: t_DeepModelTy, y: t_DeepModelTy. gt_log_DeepModelTy x y
      = (cmp_log_DeepModelTy x y = Greater)
  
  predicate ge_log_DeepModelTy (self: t_DeepModelTy) (o: t_DeepModelTy)
  
  function cmp_ge_log_DeepModelTy (x: t_DeepModelTy) (y: t_DeepModelTy) : ()
  
  axiom cmp_ge_log_DeepModelTy_spec: forall x: t_DeepModelTy, y: t_DeepModelTy. ge_log_DeepModelTy x y
      = (cmp_log_DeepModelTy x y <> Less)
  
  predicate lt_log_DeepModelTy (self: t_DeepModelTy) (o: t_DeepModelTy)
  
  function cmp_lt_log_DeepModelTy (x: t_DeepModelTy) (y: t_DeepModelTy) : ()
  
  axiom cmp_lt_log_DeepModelTy_spec: forall x: t_DeepModelTy, y: t_DeepModelTy. lt_log_DeepModelTy x y
      = (cmp_log_DeepModelTy x y = Less)
  
  predicate le_log_DeepModelTy (self: t_DeepModelTy) (o: t_DeepModelTy)
  
  function cmp_le_log_DeepModelTy (x: t_DeepModelTy) (y: t_DeepModelTy) : ()
  
  axiom cmp_le_log_DeepModelTy_spec: forall x: t_DeepModelTy, y: t_DeepModelTy. le_log_DeepModelTy x y
      = (cmp_log_DeepModelTy x y <> Greater)
  
  predicate heap_frag_DeepModelTy (s: Seq.seq t_DeepModelTy) (start: int) (end': int) =
    forall i: int. start <= parent i /\ i < end' -> le_log_DeepModelTy (Seq.get s i) (Seq.get s (parent i))
  
  function deep_model_T (self: t_T) : t_DeepModelTy
  
  function index_Vec_T_Global [@inline:trivial] (self: t_Vec_T_Global) (ix: int) : t_T =
    Seq.get (view_Vec_T_Global self) ix
  
  meta "rewrite_def" function index_Vec_T_Global
  
  function deep_model_Vec_T_Global (self: t_Vec_T_Global) : Seq.seq t_DeepModelTy
  
  axiom deep_model_Vec_T_Global_spec: forall self: t_Vec_T_Global. Seq.length (view_Vec_T_Global self)
      = Seq.length (deep_model_Vec_T_Global self)
  
  axiom deep_model_Vec_T_Global_spec'0: forall self: t_Vec_T_Global. forall i: int. 0 <= i
          /\ i < Seq.length (view_Vec_T_Global self)
        -> Seq.get (deep_model_Vec_T_Global self) i = deep_model_T (index_Vec_T_Global self i)
  
  function deep_model_refmut_Vec_T_Global [@inline:trivial] (self: MutBorrow.t t_Vec_T_Global) : Seq.seq t_DeepModelTy =
    deep_model_Vec_T_Global self.current
  
  meta "rewrite_def" function deep_model_refmut_Vec_T_Global
  
  predicate permutation_of_T (self: Seq.seq t_T) (other: Seq.seq t_T) = Permut.permut self other 0 (Seq.length self)
  
  predicate invariant_refmut_Vec_T_Global [@inline:trivial] (self: MutBorrow.t t_Vec_T_Global) =
    inv_Vec_T_Global self.current /\ inv_Vec_T_Global self.final
  
  meta "rewrite_def" predicate invariant_refmut_Vec_T_Global
  
  predicate inv_refmut_Vec_T_Global [@inline:trivial] (_1: MutBorrow.t t_Vec_T_Global) =
    invariant_refmut_Vec_T_Global _1
  
  meta "rewrite_def" predicate inv_refmut_Vec_T_Global
  
  let rec sift_down_T (v: MutBorrow.t t_Vec_T_Global) (start: UInt64.t) (end': UInt64.t) (return (x: ())) =
    {[@stop_split] [@expl:sift_down_T requires] ([@stop_split] [@expl:sift_down 'v' type invariant] inv_refmut_Vec_T_Global v)
    /\ ([@stop_split] [@expl:sift_down requires #0] heap_frag_DeepModelTy (deep_model_refmut_Vec_T_Global v) (UInt64.t'int start
      + 1) (UInt64.t'int end'))
    /\ ([@stop_split] [@expl:sift_down requires #1] UInt64.t'int start < UInt64.t'int end')
    /\ ([@stop_split] [@expl:sift_down requires #2] UInt64.t'int end' <= Seq.length (view_Vec_T_Global v.current))}
    any
    [ return (result: ()) ->
    {[@stop_split] [@expl:sift_down_T ensures] ([@stop_split] [@expl:sift_down ensures #0] heap_frag_DeepModelTy (deep_model_Vec_T_Global v.final) (UInt64.t'int start) (UInt64.t'int end'))
      /\ ([@stop_split] [@expl:sift_down ensures #1] permutation_of_T (view_Vec_T_Global v.final) (view_Vec_T_Global v.current))
      /\ ([@stop_split] [@expl:sift_down ensures #2] forall i: int. 0 <= i /\ i < UInt64.t'int start
            \/ UInt64.t'int end' <= i /\ i < Seq.length (view_Vec_T_Global v.current)
          -> index_Vec_T_Global v.current i = index_Vec_T_Global v.final i)
      /\ ([@stop_split] [@expl:sift_down ensures #3] forall m: t_DeepModelTy. (forall j: int. UInt64.t'int start <= j
              /\ j < UInt64.t'int end' -> le_log_DeepModelTy (Seq.get (deep_model_refmut_Vec_T_Global v) j) m)
        -> (forall j: int. UInt64.t'int start <= j /\ j < UInt64.t'int end'
          -> le_log_DeepModelTy (Seq.get (deep_model_Vec_T_Global v.final) j) m))}
      (! return {result}) ]
  
  predicate sorted_range_DeepModelTy (s: Seq.seq t_DeepModelTy) (l: int) (u: int) =
    forall i: int, j: int. l <= i /\ i < j /\ j < u -> le_log_DeepModelTy (Seq.get s i) (Seq.get s j)
  
  predicate invariant_slice_T (self: Slice64.slice t_T) = inv_Seq_T (Slice64.view self)
  
  predicate inv_slice_T [@inline:trivial] (_1: Slice64.slice t_T) = invariant_slice_T _1
  
  meta "rewrite_def" predicate inv_slice_T
  
  predicate invariant_refmut_slice_T [@inline:trivial] (self: MutBorrow.t (Slice64.slice t_T)) =
    inv_slice_T self.current /\ inv_slice_T self.final
  
  meta "rewrite_def" predicate invariant_refmut_slice_T
  
  predicate inv_refmut_slice_T [@inline:trivial] (_1: MutBorrow.t (Slice64.slice t_T)) = invariant_refmut_slice_T _1
  
  meta "rewrite_def" predicate inv_refmut_slice_T
  
  let rec deref_mut_Vec_T_Global (self_: MutBorrow.t t_Vec_T_Global) (return (x: MutBorrow.t (Slice64.slice t_T))) =
    {[@stop_split] [@expl:deref_mut 'self_' type invariant] inv_refmut_Vec_T_Global self_}
    any
    [ return (result: MutBorrow.t (Slice64.slice t_T)) ->
    {[@stop_split] [@expl:deref_mut_Vec_T_Global ensures] ([@stop_split] [@expl:deref_mut result type invariant] inv_refmut_slice_T result)
      /\ ([@stop_split] [@expl:deref_mut ensures #0] Slice64.view result.current = view_Vec_T_Global self_.current)
      /\ ([@stop_split] [@expl:deref_mut ensures #1] Seq.length (view_Vec_T_Global self_.final)
        = Seq.length (view_Vec_T_Global self_.current))
      /\ ([@stop_split] [@expl:deref_mut ensures #2] Slice64.view result.final = view_Vec_T_Global self_.final)}
      (! return {result}) ]
  
  let rec swap_T (self_: MutBorrow.t (Slice64.slice t_T)) (i: UInt64.t) (j: UInt64.t) (return (x: ())) =
    {[@stop_split] [@expl:swap_T requires] ([@stop_split] [@expl:swap 'self_' type invariant] inv_refmut_slice_T self_)
    /\ ([@stop_split] [@expl:swap requires #0] UInt64.t'int i < Seq.length (Slice64.view self_.current))
    /\ ([@stop_split] [@expl:swap requires #1] UInt64.t'int j < Seq.length (Slice64.view self_.current))}
    any
    [ return (result: ()) ->
    {[@stop_split] [@expl:swap ensures] Permut.exchange (Slice64.view self_.final) (Slice64.view self_.current) (UInt64.t'int i) (UInt64.t'int j)}
      (! return {result}) ]
  
  predicate resolve_refmut_slice_T [@inline:trivial] (_1: MutBorrow.t (Slice64.slice t_T)) = _1.final = _1.current
  
  meta "rewrite_def" predicate resolve_refmut_slice_T
  
  function heap_frag_max_DeepModelTy (s: Seq.seq t_DeepModelTy) (i: int) (end': int) : ()
  
  axiom heap_frag_max_DeepModelTy_def:
    forall s: Seq.seq t_DeepModelTy, i: int, end': int. heap_frag_DeepModelTy s 0 end'
      -> 0 <= i /\ i < end'
      -> heap_frag_max_DeepModelTy s i end' = (if i > 0 then heap_frag_max_DeepModelTy s (parent i) end' else ())
  
  axiom heap_frag_max_DeepModelTy_spec:
    forall s: Seq.seq t_DeepModelTy, i: int, end': int. heap_frag_DeepModelTy s 0 end'
      -> 0 <= i /\ i < end' -> le_log_DeepModelTy (Seq.get s i) (Seq.get s 0)
  
  predicate resolve_refmut_Vec_T_Global [@inline:trivial] (_1: MutBorrow.t t_Vec_T_Global) = _1.final = _1.current
  
  meta "rewrite_def" predicate resolve_refmut_Vec_T_Global
  
  predicate sorted_DeepModelTy (s: Seq.seq t_DeepModelTy) = sorted_range_DeepModelTy s 0 (Seq.length s)
  
  meta "compute_max_steps" 1000000
  
  meta "select_lsinst" "all"
  
  let rec heap_sort_T (v: MutBorrow.t t_Vec_T_Global) (return (x: ())) =
    {[@stop_split] [@expl:heap_sort 'v' type invariant] inv_refmut_Vec_T_Global v}
    (! bb0
    [ bb0 = s0
      [ s0 = [ &old_v <- v ] s1
      | s1 = len_T {v.current} (fun (_x: UInt64.t) -> [ &_10 <- _x ] s2)
      | s2 = [ &_12 <- (2: UInt64.t) = (0: UInt64.t) ] s3
      | s3 = {[@expl:division by zero] not _12} s4
      | s4 = UInt64.div {_10} {(2: UInt64.t)} (fun (_x: UInt64.t) -> [ &start <- _x ] s5)
      | s5 = [ &_old <- v.final ] s6
      | s6 = bb4 ]
    | bb4 = bb4
      [ bb4 = {[@expl:inferred invariant: type invariant] inv_refmut_Vec_T_Global v}
        {[@expl:inferred invariant: unchanged value] _old = v.final}
        {[@expl:loop invariant #0] permutation_of_T (view_Vec_T_Global v.current) (view_Vec_T_Global old_v.current)}
        {[@expl:loop invariant #1] heap_frag_DeepModelTy (deep_model_refmut_Vec_T_Global v) (UInt64.t'int start) (Seq.length (view_Vec_T_Global v.current))}
        {[@expl:loop invariant #2] UInt64.t'int start
        <= ComputerDivision.div (Seq.length (view_Vec_T_Global v.current)) 2}
        (! s0)
        [ s0 = [ &_25 <- UInt64.gt start (0: UInt64.t) ] s1
        | s1 = any [ br0 -> {_25 = false} (! bb9) | br1 -> {_25} (! bb6) ] ]
        [ bb6 = s0
          [ s0 = UInt64.sub {start} {(1: UInt64.t)} (fun (_x: UInt64.t) -> [ &start <- _x ] s1)
          | s1 = len_T {v.current} (fun (_x: UInt64.t) -> [ &_30 <- _x ] s2)
          | s2 = MutBorrow.borrow_mut <t_Vec_T_Global> {v.current}
              (fun (_bor: MutBorrow.t t_Vec_T_Global) ->
                [ &_28 <- _bor ] -{inv_Vec_T_Global _bor.final}-
                [ &v <- { v with current = _bor.final } ] s3)
            [ _ck -> (! {[@expl:type invariant] inv_Vec_T_Global v.current} any) ]
          | s3 = sift_down_T {_28} {start} {_30} (fun (_x: ()) -> [ &_27 <- _x ] s4)
          | s4 = bb4 ] ] ]
    | bb9 = s0
      [ s0 = len_T {v.current} (fun (_x: UInt64.t) -> [ &end' <- _x ] s1) | s1 = [ &_old'0 <- v.final ] s2 | s2 = bb11 ]
    | bb11 = bb11
      [ bb11 = {[@expl:inferred invariant: type invariant] inv_refmut_Vec_T_Global v}
        {[@expl:inferred invariant: unchanged value] _old'0 = v.final}
        {[@expl:loop invariant #0] UInt64.t'int end' <= Seq.length (view_Vec_T_Global v.current)}
        {[@expl:loop invariant #1] permutation_of_T (view_Vec_T_Global v.current) (view_Vec_T_Global old_v.current)}
        {[@expl:loop invariant #2] heap_frag_DeepModelTy (deep_model_refmut_Vec_T_Global v) 0 (UInt64.t'int end')}
        {[@expl:loop invariant #3] sorted_range_DeepModelTy (deep_model_refmut_Vec_T_Global v) (UInt64.t'int end') (Seq.length (view_Vec_T_Global v.current))}
        {[@expl:loop invariant #4] forall i: int, j: int. 0 <= i
            /\ i < UInt64.t'int end' /\ UInt64.t'int end' <= j /\ j < Seq.length (view_Vec_T_Global v.current)
          -> le_log_DeepModelTy (Seq.get (deep_model_refmut_Vec_T_Global v) i) (Seq.get (deep_model_refmut_Vec_T_Global v) j)}
        (! s0)
        [ s0 = [ &_51 <- UInt64.gt end' (1: UInt64.t) ] s1
        | s1 = any [ br0 -> {_51 = false} (! bb17) | br1 -> {_51} (! bb13) ] ]
        [ bb13 = s0
          [ s0 = UInt64.sub {end'} {(1: UInt64.t)} (fun (_x: UInt64.t) -> [ &end' <- _x ] s1)
          | s1 = MutBorrow.borrow_mut <t_Vec_T_Global> {v.current}
              (fun (_bor: MutBorrow.t t_Vec_T_Global) ->
                [ &_56 <- _bor ] -{inv_Vec_T_Global _bor.final}-
                [ &v <- { v with current = _bor.final } ] s2)
            [ _ck -> (! {[@expl:type invariant] inv_Vec_T_Global v.current} any) ]
          | s2 = deref_mut_Vec_T_Global {_56} (fun (_x: MutBorrow.t (Slice64.slice t_T)) -> [ &_55 <- _x ] s3)
          | s3 = MutBorrow.borrow_final <Slice64.slice t_T> {_55.current} {MutBorrow.get_id _55}
              (fun (_bor: MutBorrow.t (Slice64.slice t_T)) ->
                [ &_54 <- _bor ] -{inv_slice_T _bor.final}-
                [ &_55 <- { _55 with current = _bor.final } ] s4)
            [ _ck -> (! {[@expl:type invariant] inv_slice_T _55.current} any) ]
          | s4 = swap_T {_54} {(0: UInt64.t)} {end'} (fun (_x: ()) -> [ &_53 <- _x ] s5)
          | s5 = s6 [ _ck -> (! {[@expl:type invariant] inv_refmut_slice_T _55} any) ]
          | s6 = -{resolve_refmut_slice_T _55}- s7
          | s7 =
            {[@expl:assertion] let _ = heap_frag_max_DeepModelTy (deep_model_refmut_Vec_T_Global v) 0 (UInt64.t'int end') in forall i: int, j: int. 0
                  <= i
                /\ i < UInt64.t'int end' /\ UInt64.t'int end' <= j /\ j < Seq.length (view_Vec_T_Global v.current)
              -> le_log_DeepModelTy (Seq.get (deep_model_refmut_Vec_T_Global v) i) (Seq.get (deep_model_refmut_Vec_T_Global v) j)}
            s8
          | s8 = MutBorrow.borrow_mut <t_Vec_T_Global> {v.current}
              (fun (_bor: MutBorrow.t t_Vec_T_Global) ->
                [ &_63 <- _bor ] -{inv_Vec_T_Global _bor.final}-
                [ &v <- { v with current = _bor.final } ] s9)
            [ _ck -> (! {[@expl:type invariant] inv_Vec_T_Global v.current} any) ]
          | s9 = sift_down_T {_63} {(0: UInt64.t)} {end'} (fun (_x: ()) -> [ &_62 <- _x ] s10)
          | s10 = bb11 ] ] ]
    | bb17 = s0
      [ s0 = s1 [ _ck -> (! {[@expl:type invariant] inv_refmut_Vec_T_Global v} any) ]
      | s1 = -{resolve_refmut_Vec_T_Global v}- s2
      | s2 = return {_ret} ] ]
    [ & _ret: () = Any.any_l ()
    | & v: MutBorrow.t t_Vec_T_Global = v
    | & old_v: MutBorrow.t t_Vec_T_Global = Any.any_l ()
    | & start: UInt64.t = Any.any_l ()
    | & _10: UInt64.t = Any.any_l ()
    | & _12: bool = Any.any_l ()
    | & _25: bool = Any.any_l ()
    | & _27: () = Any.any_l ()
    | & _28: MutBorrow.t t_Vec_T_Global = Any.any_l ()
    | & _30: UInt64.t = Any.any_l ()
    | & end': UInt64.t = Any.any_l ()
    | & _51: bool = Any.any_l ()
    | & _53: () = Any.any_l ()
    | & _54: MutBorrow.t (Slice64.slice t_T) = Any.any_l ()
    | & _55: MutBorrow.t (Slice64.slice t_T) = Any.any_l ()
    | & _56: MutBorrow.t t_Vec_T_Global = Any.any_l ()
    | & _62: () = Any.any_l ()
    | & _63: MutBorrow.t t_Vec_T_Global = Any.any_l ()
    | & _old: t_Vec_T_Global = Any.any_l ()
    | & _old'0: t_Vec_T_Global = Any.any_l () ])
    [ return (result: ()) ->
    {[@stop_split] [@expl:heap_sort_T ensures] ([@stop_split] [@expl:heap_sort ensures #0] sorted_DeepModelTy (deep_model_Vec_T_Global v.final))
      /\ ([@stop_split] [@expl:heap_sort ensures #1] permutation_of_T (view_Vec_T_Global v.final) (view_Vec_T_Global v.current))}
      (! return {result}) ]
end