val external_method_take_snapshot_of_reads_clauses_computation_maintains_positions_valid_in_state
      (actor: tid_t)
      (writer_pc: pc_t)
      (writer_expression_number: nat)
      (bypassing_write_buffer: bool)
      (reads_clauses: list (var_id_t * expression_t))
      (s: Armada.State.t)
    : Lemma (requires positions_valid_in_state s)
      (ensures
        (match
            external_method_take_snapshot_of_reads_clauses_computation actor
              writer_pc
              writer_expression_number
              bypassing_write_buffer
              reads_clauses
              s
          with
          | ComputationImpossible | ComputationUndefined -> True
          | ComputationProduces s' -> positions_valid_in_state s'))
      (decreases reads_clauses)
val external_method_take_snapshot_of_reads_clauses_computation_maintains_positions_valid_in_state
      (actor: tid_t)
      (writer_pc: pc_t)
      (writer_expression_number: nat)
      (bypassing_write_buffer: bool)
      (reads_clauses: list (var_id_t * expression_t))
      (s: Armada.State.t)
    : Lemma (requires positions_valid_in_state s)
      (ensures
        (match
            external_method_take_snapshot_of_reads_clauses_computation actor
              writer_pc
              writer_expression_number
              bypassing_write_buffer
              reads_clauses
              s
          with
          | ComputationImpossible | ComputationUndefined -> True
          | ComputationProduces s' -> positions_valid_in_state s'))
      (decreases reads_clauses)
let rec external_method_take_snapshot_of_reads_clauses_computation_maintains_positions_valid_in_state
  (actor: tid_t)
  (writer_pc: pc_t)
  (writer_expression_number: nat)
  (bypassing_write_buffer: bool)
  (reads_clauses: list (var_id_t * expression_t))
  (s: Armada.State.t)
  : Lemma (requires positions_valid_in_state s)
          (ensures  (match external_method_take_snapshot_of_reads_clauses_computation actor writer_pc
                             writer_expression_number bypassing_write_buffer reads_clauses s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> positions_valid_in_state s'))
          (decreases reads_clauses) =
  match reads_clauses with
  | [] -> ()
  | (first_var_id, first_reads_expression) :: remaining_reads_clauses ->
      (match rvalue_computation first_reads_expression actor s with
       | ComputationImpossible | ComputationUndefined -> ()
       | ComputationProduces first_value ->
           let td = expression_to_td first_reads_expression in
           let local_var = ExpressionLocalVariable td first_var_id in
           update_expression_maintains_positions_valid_in_state local_var actor writer_pc writer_expression_number
             bypassing_write_buffer first_value s;
           (match update_expression local_var actor writer_pc writer_expression_number bypassing_write_buffer
                    first_value s with
            | ComputationImpossible | ComputationUndefined -> ()
            | ComputationProduces s' ->
                external_method_take_snapshot_of_reads_clauses_computation_maintains_positions_valid_in_state
                  actor writer_pc (writer_expression_number + 1) bypassing_write_buffer remaining_reads_clauses 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')

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

#push-options "--z3rlimit 10"

let update_pointed_to_value_maintains_positions_valid_in_state
  (p: Armada.Pointer.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 (requires positions_valid_in_state s)
          (ensures  (match update_pointed_to_value p actor writer_pc writer_expression_number bypassing_write_buffer
                             new_value s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> positions_valid_in_state s')) =
  ()

let update_expression_maintains_positions_valid_in_state
  (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 (requires positions_valid_in_state s)
          (ensures  (match update_expression exp actor writer_pc writer_expression_number bypassing_write_buffer
                             new_value s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> positions_valid_in_state s')) =
  ()

#pop-options

let rec update_expressions_maintains_positions_valid_in_state
  (exps: list expression_t)
  (actor: tid_t)
  (writer_pc: pc_t)
  (writer_expression_number: nat)
  (bypassing_write_buffer: bool)
  (new_values: list object_value_t)
  (s: Armada.State.t)
  : Lemma (requires positions_valid_in_state s)
          (ensures  (match update_expressions exps actor writer_pc writer_expression_number bypassing_write_buffer
                             new_values s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> positions_valid_in_state s'))
          (decreases exps) =
  match exps, new_values with
  | [], [] -> ()
  | first_exp :: remaining_exps, first_new_value :: remaining_new_values ->
      update_expression_maintains_positions_valid_in_state first_exp actor writer_pc writer_expression_number
        bypassing_write_buffer first_new_value s;
      (match update_expression first_exp actor writer_pc writer_expression_number
               bypassing_write_buffer first_new_value s with
       | ComputationImpossible | ComputationUndefined -> ()
       | ComputationProduces s' ->
           update_expressions_maintains_positions_valid_in_state remaining_exps actor writer_pc
             (writer_expression_number + 1) bypassing_write_buffer remaining_new_values 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 ->
    bypassing_write_buffer: Prims.bool ->
    reads_clauses: Prims.list (Armada.Base.var_id_t * Armada.Expression.expression_t) ->
    s: Armada.State.t
  -> FStar.Pervasives.Lemma
      (requires Strategies.ArmadaInvariant.PositionsValid.positions_valid_in_state s)
      (ensures
        ((match
              Armada.Statement.external_method_take_snapshot_of_reads_clauses_computation actor
                writer_pc
                writer_expression_number
                bypassing_write_buffer
                reads_clauses
                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 reads_clauses)
Armada.Base.tid_t Armada.Base.pc_t Prims.nat Prims.bool Prims.list FStar.Pervasives.Native.tuple2 Armada.Base.var_id_t Armada.Expression.expression_t Armada.State.t Armada.Expression.rvalue_computation Armada.Type.valid_object_value_t Armada.Expression.expression_to_td Armada.Expression.update_expression Strategies.ArmadaInvariant.PositionsValid.external_method_take_snapshot_of_reads_clauses_computation_maintains_positions_valid_in_state Prims.op_Addition Prims.unit Strategies.ArmadaInvariant.PositionsValid.update_expression_maintains_positions_valid_in_state Armada.Expression.ExpressionLocalVariable Armada.Type.object_td_t Strategies.ArmadaInvariant.PositionsValid.positions_valid_in_state Prims.squash Armada.Statement.external_method_take_snapshot_of_reads_clauses_computation Prims.l_True Prims.Nil FStar.Pervasives.pattern
let rec external_method_take_snapshot_of_reads_clauses_computation_maintains_positions_valid_in_state
      (actor: tid_t)
      (writer_pc: pc_t)
      (writer_expression_number: nat)
      (bypassing_write_buffer: bool)
      (reads_clauses: list (var_id_t * expression_t))
      (s: Armada.State.t)
    : Lemma (requires positions_valid_in_state s)
      (ensures
        (match
            external_method_take_snapshot_of_reads_clauses_computation actor
              writer_pc
              writer_expression_number
              bypassing_write_buffer
              reads_clauses
              s
          with
          | ComputationImpossible | ComputationUndefined -> True
          | ComputationProduces s' -> positions_valid_in_state s'))
      (decreases reads_clauses) =
  
match reads_clauses with
| [] -> ()
| (first_var_id, first_reads_expression) :: remaining_reads_clauses ->
  (match rvalue_computation first_reads_expression actor s with
    | ComputationImpossible | ComputationUndefined -> ()
    | ComputationProduces first_value ->
      let td = expression_to_td first_reads_expression in
      let local_var = ExpressionLocalVariable td first_var_id in
      update_expression_maintains_positions_valid_in_state local_var
        actor
        writer_pc
        writer_expression_number
        bypassing_write_buffer
        first_value
        s;
      (match
          update_expression local_var
            actor
            writer_pc
            writer_expression_number
            bypassing_write_buffer
            first_value
            s
        with
        | ComputationImpossible | ComputationUndefined -> ()
        | ComputationProduces s' ->
          external_method_take_snapshot_of_reads_clauses_computation_maintains_positions_valid_in_state
            actor
            writer_pc
            (writer_expression_number + 1)
            bypassing_write_buffer
            remaining_reads_clauses
            s'))
| _ -> ()