val compare_and_swap_statement_computation_maintains_positions_valid_in_state
      (actor: tid_t)
      (nd: nondeterminism_t)
      (start_pc: pc_t)
      (target old_val new_val: expression_t)
      (bypassing_write_buffer: bool)
      (optional_result: option expression_t)
      (s: Armada.State.t)
    : Lemma (requires positions_valid_in_state s)
      (ensures
        (match
            compare_and_swap_statement_computation actor
              nd
              start_pc
              target
              old_val
              new_val
              bypassing_write_buffer
              optional_result
              s
          with
          | ComputationImpossible | ComputationUndefined -> True
          | ComputationProduces s' -> positions_valid_in_state s'))
val compare_and_swap_statement_computation_maintains_positions_valid_in_state
      (actor: tid_t)
      (nd: nondeterminism_t)
      (start_pc: pc_t)
      (target old_val new_val: expression_t)
      (bypassing_write_buffer: bool)
      (optional_result: option expression_t)
      (s: Armada.State.t)
    : Lemma (requires positions_valid_in_state s)
      (ensures
        (match
            compare_and_swap_statement_computation actor
              nd
              start_pc
              target
              old_val
              new_val
              bypassing_write_buffer
              optional_result
              s
          with
          | ComputationImpossible | ComputationUndefined -> True
          | ComputationProduces s' -> positions_valid_in_state s'))
let compare_and_swap_statement_computation_maintains_positions_valid_in_state
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (target: expression_t)
  (old_val: expression_t)
  (new_val: expression_t)
  (bypassing_write_buffer: bool)
  (optional_result: option expression_t)
  (s: Armada.State.t)
  : Lemma (requires positions_valid_in_state s)
          (ensures  (match compare_and_swap_statement_computation actor nd start_pc target old_val new_val
                             bypassing_write_buffer optional_result s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> positions_valid_in_state s')) =
  let cs' = compare_and_swap_statement_computation actor nd start_pc target old_val new_val
              bypassing_write_buffer optional_result s in
  if   Cons? nd
     || neqb (expression_to_td target) (expression_to_td old_val)
     || neqb (expression_to_td target) (expression_to_td new_val)
     || (match optional_result with
        | Some result -> neqb (expression_to_td result) (ObjectTDPrimitive PrimitiveTDBool)
        | None -> false) then
    ()
  else begin
    match check_expression_up_to_date_for_rmw target actor s, rvalue_computation old_val actor s,
          rvalue_computation target actor s, rvalue_computation new_val actor s,
          lvalue_computation target actor s  with
    | ComputationProduces _, ComputationProduces old_value,
      ComputationProduces target_value, ComputationProduces new_value,
      ComputationProduces target_ptr -> begin
        let swap = eqb target_value old_value in
        update_pointed_to_value_maintains_positions_valid_in_state target_ptr actor start_pc 0 false new_value s;
        match optional_result with
        | None -> ()
        | Some result ->
          match lvalue_computation result actor s, (if swap then update_pointed_to_value target_ptr actor start_pc 0 false new_value s else return s) with
          | ComputationProduces result_ptr, ComputationProduces s' ->
              let swap_value = ObjectValuePrimitive (PrimitiveBoxBool swap) in
              update_pointed_to_value_maintains_positions_valid_in_state result_ptr actor start_pc 1 bypassing_write_buffer swap_value s'
          | _ -> ()
      end
    | _ -> ()
  end
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')
  | _ -> ()

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

let rec log_expressions_computation_maintains_positions_valid_in_state
  (actor: tid_t)
  (logs_clauses: list expression_t)
  (s: Armada.State.t)
  : Lemma (requires positions_valid_in_state s)
          (ensures  (match log_expressions_computation actor logs_clauses s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> positions_valid_in_state s'))
          (decreases logs_clauses) =
  match logs_clauses with
  | [] -> ()
  | first_logs_clause :: remaining_logs_clauses ->
      (match rvalue_computation first_logs_clause actor s with
       | ComputationImpossible | ComputationUndefined -> ()
       | ComputationProduces event ->
           let trace' = s.trace $:: event in
           let s' = { s with trace = trace' } in
           log_expressions_computation_maintains_positions_valid_in_state actor remaining_logs_clauses s')

#push-options "--z3rlimit 10"

let assume_expression_statement_computation_maintains_positions_valid_in_state
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (exp: expression_t)
  (s: Armada.State.t)
  : Lemma (requires positions_valid_in_state s)
          (ensures  (match assume_expression_statement_computation actor nd start_pc exp s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> positions_valid_in_state s')) =
  ()

let assume_predicate_statement_computation_maintains_positions_valid_in_state
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (pred: Armada.State.t -> GTot bool)
  (s: Armada.State.t)
  : Lemma (requires positions_valid_in_state s)
          (ensures  (match assume_predicate_statement_computation actor nd start_pc pred s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> positions_valid_in_state s')) =
  ()

let assert_true_statement_computation_maintains_positions_valid_in_state
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (exp: expression_t)
  (s: Armada.State.t)
  : Lemma (requires positions_valid_in_state s)
          (ensures  (match assert_true_statement_computation actor nd start_pc exp s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> positions_valid_in_state s')) =
  ()

let assert_false_statement_computation_maintains_positions_valid_in_state
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (exp: expression_t)
  (s: Armada.State.t)
  : Lemma (requires positions_valid_in_state s)
          (ensures  (match assert_false_statement_computation actor nd start_pc exp s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> positions_valid_in_state s')) =
  ()

let conditional_jump_statement_computation_maintains_positions_valid_in_state
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (exp: expression_t)
  (s: Armada.State.t)
  : Lemma (requires positions_valid_in_state s)
          (ensures  (match conditional_jump_statement_computation actor nd start_pc exp s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> positions_valid_in_state s')) =
  ()

let unconditional_jump_statement_computation_maintains_positions_valid_in_state
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (s: Armada.State.t)
  : Lemma (requires positions_valid_in_state s)
          (ensures  (match unconditional_jump_statement_computation actor nd start_pc s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> positions_valid_in_state s')) =
  ()

let update_statement_computation_maintains_positions_valid_in_state
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (bypassing_write_buffer: bool)
  (dst: expression_t)
  (src: expression_t)
  (s: Armada.State.t)
  : Lemma (requires positions_valid_in_state s)
          (ensures  (match update_statement_computation actor nd start_pc bypassing_write_buffer dst src s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> positions_valid_in_state s')) =
  let cs' = update_statement_computation actor nd start_pc bypassing_write_buffer dst src s in
  if   Cons? nd
     || neqb (expression_to_td dst) (expression_to_td src) then
    ()
  else (
    match rvalue_computation src actor s with
    | ComputationImpossible | ComputationUndefined -> ()
    | ComputationProduces src_value ->
        update_expression_maintains_positions_valid_in_state dst actor start_pc 0 bypassing_write_buffer src_value s
  )

let nondeterministic_update_statement_computation_maintains_positions_valid_in_state
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (bypassing_write_buffer: bool)
  (dst: expression_t)
  (s: Armada.State.t)
  : Lemma (requires positions_valid_in_state s)
          (ensures  (match nondeterministic_update_statement_computation actor nd start_pc bypassing_write_buffer
                             dst s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> positions_valid_in_state s')) =
  let cs' = nondeterministic_update_statement_computation actor nd start_pc bypassing_write_buffer dst s in
  if   list_len nd <> 1
     || neqb (object_value_to_td (Cons?.hd nd)) (expression_to_td dst) then
    ()
  else (
    let nd_value = Cons?.hd nd in
    if not (object_value_has_all_pointers_uninitialized nd_value) then
      ()
    else
      update_expression_maintains_positions_valid_in_state dst actor start_pc 0 bypassing_write_buffer nd_value s
  )

let propagate_write_message_statement_computation_maintains_positions_valid_in_state
  (actor: tid_t)
  (nd: nondeterminism_t)
  (s: Armada.State.t)
  : Lemma (requires positions_valid_in_state s)
          (ensures  (match propagate_write_message_statement_computation actor nd s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> positions_valid_in_state 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 ->
    nd: Armada.Type.nondeterminism_t ->
    start_pc: Armada.Base.pc_t ->
    target: Armada.Expression.expression_t ->
    old_val: Armada.Expression.expression_t ->
    new_val: Armada.Expression.expression_t ->
    bypassing_write_buffer: Prims.bool ->
    optional_result: FStar.Pervasives.Native.option Armada.Expression.expression_t ->
    s: Armada.State.t
  -> FStar.Pervasives.Lemma
      (requires Strategies.ArmadaInvariant.PositionsValid.positions_valid_in_state s)
      (ensures
        ((match
              Armada.Statement.compare_and_swap_statement_computation actor
                nd
                start_pc
                target
                old_val
                new_val
                bypassing_write_buffer
                optional_result
                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))
Armada.Base.tid_t Armada.Type.nondeterminism_t Armada.Base.pc_t Armada.Expression.expression_t Prims.bool FStar.Pervasives.Native.option Armada.State.t Prims.op_BarBar Prims.uu___is_Cons Armada.Type.object_value_t Spec.Ubool.neqb Armada.Type.object_td_t Armada.Expression.expression_to_td Armada.Type.ObjectTDPrimitive Armada.Type.PrimitiveTDBool FStar.Pervasives.Native.Mktuple5 Armada.Computation.conditional_computation_t Prims.unit Armada.Type.valid_object_value_t Armada.Pointer.t Armada.Expression.check_expression_up_to_date_for_rmw Armada.Expression.rvalue_computation Armada.Expression.lvalue_computation FStar.Pervasives.Native.Mktuple2 Armada.Expression.update_pointed_to_value Armada.Computation.return Strategies.ArmadaInvariant.PositionsValid.update_pointed_to_value_maintains_positions_valid_in_state Armada.Type.ObjectValuePrimitive Armada.Type.PrimitiveBoxBool FStar.Pervasives.Native.tuple2 Spec.Ubool.eqb Prims.l_or Prims.l_and Prims.b2t Armada.Type.object_value_valid Prims.eq2 Armada.Type.object_value_to_td FStar.Pervasives.Native.tuple5 Armada.Statement.compare_and_swap_statement_computation Strategies.ArmadaInvariant.PositionsValid.positions_valid_in_state Prims.squash Prims.l_True Prims.Nil FStar.Pervasives.pattern
let compare_and_swap_statement_computation_maintains_positions_valid_in_state
      (actor: tid_t)
      (nd: nondeterminism_t)
      (start_pc: pc_t)
      (target old_val new_val: expression_t)
      (bypassing_write_buffer: bool)
      (optional_result: option expression_t)
      (s: Armada.State.t)
    : Lemma (requires positions_valid_in_state s)
      (ensures
        (match
            compare_and_swap_statement_computation actor
              nd
              start_pc
              target
              old_val
              new_val
              bypassing_write_buffer
              optional_result
              s
          with
          | ComputationImpossible | ComputationUndefined -> True
          | ComputationProduces s' -> positions_valid_in_state s')) =
  
let cs' =
  compare_and_swap_statement_computation actor
    nd
    start_pc
    target
    old_val
    new_val
    bypassing_write_buffer
    optional_result
    s
in
if
  Cons? nd || neqb (expression_to_td target) (expression_to_td old_val) ||
  neqb (expression_to_td target) (expression_to_td new_val) ||
  (match optional_result with
    | Some result -> neqb (expression_to_td result) (ObjectTDPrimitive PrimitiveTDBool)
    | None -> false)
then ()
else
  match
    check_expression_up_to_date_for_rmw target actor s,
    rvalue_computation old_val actor s,
    rvalue_computation target actor s,
    rvalue_computation new_val actor s,
    lvalue_computation target actor s
  with
  | ComputationProduces _,
  ComputationProduces old_value,
  ComputationProduces target_value,
  ComputationProduces new_value,
  ComputationProduces target_ptr ->
    let swap = eqb target_value old_value in
    update_pointed_to_value_maintains_positions_valid_in_state target_ptr
      actor
      start_pc
      0
      false
      new_value
      s;
    (match optional_result with
      | None -> ()
      | Some result ->
        match
          lvalue_computation result actor s,
          (if swap
            then update_pointed_to_value target_ptr actor start_pc 0 false new_value s
            else return s)
        with
        | ComputationProduces result_ptr, ComputationProduces s' ->
          let swap_value = ObjectValuePrimitive (PrimitiveBoxBool swap) in
          update_pointed_to_value_maintains_positions_valid_in_state result_ptr
            actor
            start_pc
            1
            bypassing_write_buffer
            swap_value
            s'
        | _ -> ())
  | _ -> ()