val push_stack_variables_maintains_status
  (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 (ensures  (match push_stack_variables actor writer_pc writer_expression_number method_id
                             frame_uniq initializers s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> status_unchanged actor s s'))
val push_stack_variables_maintains_status
  (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 (ensures  (match push_stack_variables actor writer_pc writer_expression_number method_id
                             frame_uniq initializers s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> status_unchanged actor s s'))
let rec push_stack_variables_maintains_status
  (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 (ensures  (match push_stack_variables actor writer_pc writer_expression_number method_id
                             frame_uniq initializers s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> status_unchanged actor s s'))
          (decreases initializers) =
  match initializers with
  | [] -> ()
  | first_initializer :: remaining_initializers ->
      push_stack_variable_maintains_status actor writer_pc
        writer_expression_number method_id frame_uniq first_initializer s;
      (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_status actor writer_pc
             (writer_expression_number + 1) method_id frame_uniq remaining_initializers s')
module Strategies.ArmadaStatement.Status

open Armada.Action
open Armada.Base
open Armada.Computation
open Armada.Expression
open Armada.Init
open Armada.Memory
open Armada.Pointer
open Armada.State
open Armada.Statement
open Armada.Thread
open Armada.Transition
open Armada.Type
open FStar.Sequence.Base
open Spec.List
open Spec.Logic
open Spec.Ubool
open Strategies.ArmadaStatement
open Strategies.PCRelation
open Strategies.Semantics.Armada

let push_stack_variable_maintains_status
  (actor: tid_t)
  (writer_pc: pc_t)
  (writer_expression_number: nat)
  (method_id: method_id_t)
  (frame_uniq: root_id_uniquifier_t)
  (initializer: initializer_t)
  (s: Armada.State.t)
  : Lemma (ensures  (match push_stack_variable actor writer_pc writer_expression_number method_id
                             frame_uniq initializer s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> status_unchanged actor s s')) =
  ()
/
Strategies.Semantics.Armada.fsti.checked Strategies.PCRelation.fst.checked Strategies.ArmadaStatement.fst.checked Spec.Ubool.fst.checked Spec.Logic.fst.checked Spec.List.fst.checked prims.fst.checked FStar.Sequence.Base.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked Armada.Type.fst.checked Armada.Transition.fst.checked Armada.Thread.fst.checked Armada.Step.fst.checked Armada.Statement.fst.checked Armada.State.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.ArmadaStatement.Status.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 ->
    initializers: Prims.list Armada.Init.initializer_t ->
    s: Armada.State.t
  -> FStar.Pervasives.Lemma
      (ensures
        ((match
              Armada.Init.push_stack_variables actor
                writer_pc
                writer_expression_number
                method_id
                frame_uniq
                initializers
                s
            with
            | Armada.Computation.ComputationImpossible #_ -> Prims.l_True
            | Armada.Computation.ComputationUndefined #_ -> Prims.l_True
            | Armada.Computation.ComputationProduces #_ s' ->
              Strategies.ArmadaStatement.Status.status_unchanged actor s s')
          <:
          Type0)) (decreases initializers)
Armada.Base.tid_t Armada.Base.pc_t Prims.nat Armada.Base.method_id_t Armada.Base.root_id_uniquifier_t Prims.list Armada.Init.initializer_t Armada.State.t Armada.Init.push_stack_variable Strategies.ArmadaStatement.Status.push_stack_variables_maintains_status Prims.op_Addition Prims.unit Strategies.ArmadaStatement.Status.push_stack_variable_maintains_status Prims.l_True Prims.squash Armada.Init.push_stack_variables Strategies.ArmadaStatement.Status.status_unchanged Prims.Nil FStar.Pervasives.pattern
let rec push_stack_variables_maintains_status
      (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
      (ensures
        (match
            push_stack_variables actor
              writer_pc
              writer_expression_number
              method_id
              frame_uniq
              initializers
              s
          with
          | ComputationImpossible | ComputationUndefined -> True
          | ComputationProduces s' -> status_unchanged actor s s')) (decreases initializers) =
  
match initializers with
| [] -> ()
| first_initializer :: remaining_initializers ->
  push_stack_variable_maintains_status actor
    writer_pc
    writer_expression_number
    method_id
    frame_uniq
    first_initializer
    s;
  (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_status actor
        writer_pc
        (writer_expression_number + 1)
        method_id
        frame_uniq
        remaining_initializers
        s')