val push_stack_parameters_maintains_positions_valid_in_state
      (actor: tid_t)
      (writer_pc: pc_t)
      (writer_expression_number: nat)
      (method_id: method_id_t)
      (frame_uniq: root_id_uniquifier_t)
      (var_ids: list var_id_t)
      (parameters: list object_value_t)
      (s: Armada.State.t)
    : Lemma (requires positions_valid_in_state s)
      (ensures
        (match
            push_stack_parameters actor
              writer_pc
              writer_expression_number
              method_id
              frame_uniq
              var_ids
              parameters
              s
          with
          | ComputationImpossible | ComputationUndefined -> True
          | ComputationProduces s' -> positions_valid_in_state s'))
      (decreases parameters)
val push_stack_parameters_maintains_positions_valid_in_state
      (actor: tid_t)
      (writer_pc: pc_t)
      (writer_expression_number: nat)
      (method_id: method_id_t)
      (frame_uniq: root_id_uniquifier_t)
      (var_ids: list var_id_t)
      (parameters: list object_value_t)
      (s: Armada.State.t)
    : Lemma (requires positions_valid_in_state s)
      (ensures
        (match
            push_stack_parameters actor
              writer_pc
              writer_expression_number
              method_id
              frame_uniq
              var_ids
              parameters
              s
          with
          | ComputationImpossible | ComputationUndefined -> True
          | ComputationProduces s' -> positions_valid_in_state s'))
      (decreases parameters)
let rec push_stack_parameters_maintains_positions_valid_in_state
  (actor: tid_t)
  (writer_pc: pc_t)
  (writer_expression_number: nat)
  (method_id: method_id_t)
  (frame_uniq: root_id_uniquifier_t)
  (var_ids: list var_id_t)
  (parameters: list object_value_t)
  (s: Armada.State.t)
  : Lemma (requires positions_valid_in_state s)
          (ensures  (match push_stack_parameters actor writer_pc writer_expression_number method_id frame_uniq
                             var_ids parameters s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> positions_valid_in_state s'))
          (decreases parameters) =
  match parameters, var_ids with
  | [], [] -> ()
  | first_parameter :: remaining_parameters, first_var_id :: remaining_var_ids ->
      let first_initializer =
        { var_id = first_var_id; iv = InitializerSpecific first_parameter; weakly_consistent = false } in
      (match push_stack_variable actor writer_pc writer_expression_number method_id frame_uniq first_initializer s with
       | ComputationImpossible | ComputationUndefined -> ()
       | ComputationProduces s' ->
           push_stack_parameters_maintains_positions_valid_in_state actor writer_pc (writer_expression_number + 1)
             method_id frame_uniq remaining_var_ids remaining_parameters s')
  | _ -> ()
module Strategies.ArmadaInvariant.PositionsValid

open Armada.Action
open Armada.Base
open Armada.Computation
open Armada.Expression
open Armada.Init
open Armada.Memory
open Armada.Pointer
open Armada.Program
open Armada.State
open Armada.Statement
open Armada.Thread
open Armada.Threads
open Armada.Transition
open Armada.Type
open FStar.Sequence.Ambient
open FStar.Sequence.Base
open FStar.Tactics.V2
open Spec.List
open Spec.Ubool
open Strategies.ArmadaStatement
open Util.Tactics

let init_implies_positions_valid_in_state (program: Armada.Program.t) (s: Armada.State.t)
  : Lemma (requires init_program program s)
          (ensures  positions_valid_in_state s) =
  ()

let rec push_stack_variables_maintains_positions_valid_in_state
  (actor: tid_t)
  (writer_pc: pc_t)
  (writer_expression_number: nat)
  (method_id: method_id_t)
  (frame_uniq: root_id_uniquifier_t)
  (initializers: list initializer_t)
  (s: Armada.State.t)
  : Lemma (requires positions_valid_in_state s)
          (ensures  (match push_stack_variables actor writer_pc writer_expression_number method_id
                             frame_uniq initializers s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> positions_valid_in_state s'))
          (decreases initializers) =
  match initializers with
  | [] -> ()
  | first_initializer :: remaining_initializers ->
      (match push_stack_variable actor writer_pc writer_expression_number method_id frame_uniq first_initializer s with
       | ComputationImpossible | ComputationUndefined -> ()
       | ComputationProduces s' ->
           push_stack_variables_maintains_positions_valid_in_state actor writer_pc (writer_expression_number + 1)
             method_id frame_uniq remaining_initializers s')
/
Util.Tactics.fst.checked Strategies.ArmadaStatement.fst.checked Spec.Ubool.fst.checked Spec.List.fst.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Sequence.Base.fsti.checked FStar.Sequence.Ambient.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked Armada.Type.fst.checked Armada.Transition.fst.checked Armada.Threads.fst.checked Armada.Thread.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Pointer.fst.checked Armada.Memory.fst.checked Armada.Init.fst.checked Armada.Expression.fst.checked Armada.Computation.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
Strategies.ArmadaInvariant.PositionsValid.fst

    actor: Armada.Base.tid_t ->
    writer_pc: Armada.Base.pc_t ->
    writer_expression_number: Prims.nat ->
    method_id: Armada.Base.method_id_t ->
    frame_uniq: Armada.Base.root_id_uniquifier_t ->
    var_ids: Prims.list Armada.Base.var_id_t ->
    parameters: Prims.list Armada.Type.object_value_t ->
    s: Armada.State.t
  -> FStar.Pervasives.Lemma
      (requires Strategies.ArmadaInvariant.PositionsValid.positions_valid_in_state s)
      (ensures
        ((match
              Armada.Init.push_stack_parameters actor
                writer_pc
                writer_expression_number
                method_id
                frame_uniq
                var_ids
                parameters
                s
            with
            | Armada.Computation.ComputationImpossible #_ -> Prims.l_True
            | Armada.Computation.ComputationUndefined #_ -> Prims.l_True
            | Armada.Computation.ComputationProduces #_ s' ->
              Strategies.ArmadaInvariant.PositionsValid.positions_valid_in_state s')
          <:
          Type0))
      (decreases parameters)
Armada.Base.tid_t Armada.Base.pc_t Prims.nat Armada.Base.method_id_t Armada.Base.root_id_uniquifier_t Prims.list Armada.Base.var_id_t Armada.Type.object_value_t Armada.State.t FStar.Pervasives.Native.Mktuple2 Armada.Init.push_stack_variable Strategies.ArmadaInvariant.PositionsValid.push_stack_parameters_maintains_positions_valid_in_state Prims.op_Addition Prims.unit Armada.Init.initializer_t Armada.Init.Mkinitializer_t Armada.Init.InitializerSpecific FStar.Pervasives.Native.tuple2 Strategies.ArmadaInvariant.PositionsValid.positions_valid_in_state Prims.squash Armada.Init.push_stack_parameters Prims.l_True Prims.Nil FStar.Pervasives.pattern
let rec push_stack_parameters_maintains_positions_valid_in_state
      (actor: tid_t)
      (writer_pc: pc_t)
      (writer_expression_number: nat)
      (method_id: method_id_t)
      (frame_uniq: root_id_uniquifier_t)
      (var_ids: list var_id_t)
      (parameters: list object_value_t)
      (s: Armada.State.t)
    : Lemma (requires positions_valid_in_state s)
      (ensures
        (match
            push_stack_parameters actor
              writer_pc
              writer_expression_number
              method_id
              frame_uniq
              var_ids
              parameters
              s
          with
          | ComputationImpossible | ComputationUndefined -> True
          | ComputationProduces s' -> positions_valid_in_state s'))
      (decreases parameters) =
  
match parameters, var_ids with
| [], [] -> ()
| first_parameter :: remaining_parameters, first_var_id :: remaining_var_ids ->
  let first_initializer =
    { var_id = first_var_id; iv = InitializerSpecific first_parameter; weakly_consistent = false }
  in
  (match
      push_stack_variable actor
        writer_pc
        writer_expression_number
        method_id
        frame_uniq
        first_initializer
        s
    with
    | ComputationImpossible | ComputationUndefined -> ()
    | ComputationProduces s' ->
      push_stack_parameters_maintains_positions_valid_in_state actor
        writer_pc
        (writer_expression_number + 1)
        method_id
        frame_uniq
        remaining_var_ids
        remaining_parameters
        s')
| _ -> ()