val update_expression_maintains_status
      (exp: expression_t)
      (actor: tid_t)
      (writer_pc: pc_t)
      (writer_expression_number: nat)
      (bypassing_write_buffer: bool)
      (new_value: object_value_t)
      (s: Armada.State.t)
    : Lemma
    (ensures
      (match
          update_expression exp
            actor
            writer_pc
            writer_expression_number
            bypassing_write_buffer
            new_value
            s
        with
        | ComputationImpossible | ComputationUndefined -> True
        | ComputationProduces s' -> status_unchanged actor s s'))
val update_expression_maintains_status
      (exp: expression_t)
      (actor: tid_t)
      (writer_pc: pc_t)
      (writer_expression_number: nat)
      (bypassing_write_buffer: bool)
      (new_value: object_value_t)
      (s: Armada.State.t)
    : Lemma
    (ensures
      (match
          update_expression exp
            actor
            writer_pc
            writer_expression_number
            bypassing_write_buffer
            new_value
            s
        with
        | ComputationImpossible | ComputationUndefined -> True
        | ComputationProduces s' -> status_unchanged actor s s'))
let update_expression_maintains_status
  (exp: expression_t)
  (actor: tid_t)
  (writer_pc: pc_t)
  (writer_expression_number: nat)
  (bypassing_write_buffer: bool)
  (new_value: object_value_t)
  (s: Armada.State.t)
  : Lemma (ensures  (match update_expression exp actor writer_pc writer_expression_number bypassing_write_buffer
                             new_value s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> status_unchanged actor s s')) =
  let cs' = update_expression exp actor writer_pc writer_expression_number bypassing_write_buffer
              new_value s in
  if   not (expression_valid exp)
     || not (object_value_valid new_value)
     || neqb (object_value_to_td new_value) (expression_to_td exp) then
    ()
  else
    ()
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')) =
  ()

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')

let rec push_stack_parameters_maintains_status
  (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 (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' -> status_unchanged actor s 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
      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_parameters_maintains_status actor writer_pc
             (writer_expression_number + 1) method_id frame_uniq remaining_var_ids remaining_parameters 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

    exp: Armada.Expression.expression_t ->
    actor: Armada.Base.tid_t ->
    writer_pc: Armada.Base.pc_t ->
    writer_expression_number: Prims.nat ->
    bypassing_write_buffer: Prims.bool ->
    new_value: Armada.Type.object_value_t ->
    s: Armada.State.t
  -> FStar.Pervasives.Lemma
    (ensures
      ((match
            Armada.Expression.update_expression exp
              actor
              writer_pc
              writer_expression_number
              bypassing_write_buffer
              new_value
              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))
Armada.Expression.expression_t Armada.Base.tid_t Armada.Base.pc_t Prims.nat Prims.bool Armada.Type.object_value_t Armada.State.t Prims.op_BarBar Prims.op_Negation Armada.Expression.expression_valid Armada.Type.object_value_valid Spec.Ubool.neqb Armada.Type.object_td_t Armada.Type.object_value_to_td Armada.Expression.expression_to_td Prims.unit Armada.Computation.conditional_computation_t Armada.Expression.update_expression Prims.l_True Prims.squash Strategies.ArmadaStatement.Status.status_unchanged Prims.Nil FStar.Pervasives.pattern
let update_expression_maintains_status
      (exp: expression_t)
      (actor: tid_t)
      (writer_pc: pc_t)
      (writer_expression_number: nat)
      (bypassing_write_buffer: bool)
      (new_value: object_value_t)
      (s: Armada.State.t)
    : Lemma
    (ensures
      (match
          update_expression exp
            actor
            writer_pc
            writer_expression_number
            bypassing_write_buffer
            new_value
            s
        with
        | ComputationImpossible | ComputationUndefined -> True
        | ComputationProduces s' -> status_unchanged actor s s')) =
  
let cs' =
  update_expression exp actor writer_pc writer_expression_number bypassing_write_buffer new_value s
in
if
  not (expression_valid exp) || not (object_value_valid new_value) ||
  neqb (object_value_to_td new_value) (expression_to_td exp)
then ()