val rvalues_computation_when_gvars_unaddressed_at_top_level_produce_values_with_gvars_unaddressed
      (vs: list var_id_t)
      (exps: list expression_t)
      (actor: tid_t)
      (s: Armada.State.t)
    : Lemma
      (requires
        global_variables_unaddressed_at_top_level_in_rvalue_expressions vs exps /\
        inductive_invariant vs s)
      (ensures
        (match rvalues_computation exps actor s with
          | ComputationProduces values -> global_variables_unaddressed_in_object_values vs values
          | _ -> True))
      (decreases exps)
val rvalues_computation_when_gvars_unaddressed_at_top_level_produce_values_with_gvars_unaddressed
      (vs: list var_id_t)
      (exps: list expression_t)
      (actor: tid_t)
      (s: Armada.State.t)
    : Lemma
      (requires
        global_variables_unaddressed_at_top_level_in_rvalue_expressions vs exps /\
        inductive_invariant vs s)
      (ensures
        (match rvalues_computation exps actor s with
          | ComputationProduces values -> global_variables_unaddressed_in_object_values vs values
          | _ -> True))
      (decreases exps)
let rec rvalues_computation_when_gvars_unaddressed_at_top_level_produce_values_with_gvars_unaddressed
  (vs: list var_id_t)
  (exps: list expression_t)
  (actor: tid_t)
  (s: Armada.State.t)
  : Lemma (requires   global_variables_unaddressed_at_top_level_in_rvalue_expressions vs exps
                    /\ inductive_invariant vs s)
          (ensures  (match rvalues_computation exps actor s with
                     | ComputationProduces values -> global_variables_unaddressed_in_object_values vs values
                     | _ -> True))
          (decreases exps) =
  match exps with
  | [] -> ()
  | exp :: exps' ->
    rvalue_computation_when_gvars_unaddressed_at_top_level_produces_value_with_gvars_unaddressed vs exp actor s;
    rvalues_computation_when_gvars_unaddressed_at_top_level_produce_values_with_gvars_unaddressed vs exps' actor s
module Strategies.GlobalVars.UnaddressedStatement

open FStar.Sequence.Ambient
open FStar.Sequence.Base

open Util.Seq
open Util.Trigger
open Spec.List
open Spec.Ubool

open Armada.Base
open Armada.BinaryOp
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.Type
open Armada.Transition
open Armada.UnaryOp

open Strategies.Invariant
open Strategies.ArmadaInvariant.PositionsValid
open Strategies.ArmadaInvariant.RootsMatch
open Strategies.GlobalVars
open Strategies.GlobalVars.Util
open Strategies.GlobalVars.Unaddressed
open Strategies.ArmadaStatement

#push-options "--z3rlimit 10"

let inductive_invariant (vs: list var_id_t) (s: Armada.State.t) =
  global_variables_unaddressed_in_memory vs s.mem /\ positions_valid_in_state s /\ roots_match s.mem

let rec object_lacking_pointer_field_global_variables_unaddressed
  (vs: list var_id_t)
  (value: object_value_t)
  : Lemma (requires   object_td_lacks_pointer_field (object_value_to_td value)
                    /\ object_value_valid value)
          (ensures    global_variables_unaddressed_in_object_value vs value)
          (decreases  rank value)
  = match value with
    | ObjectValuePrimitive value ->
      ()
    | ObjectValueStruct fields ->
      objects_lacking_pointer_field_global_variables_unaddressed vs fields
    | ObjectValueArray element_td elements -> begin
        objects_lacking_pointer_field_global_variables_unaddressed vs elements;
        global_variables_unaddressed_in_object_value_seq_equivalent_to_forall vs elements
      end
    | ObjectValueAbstract _ _ -> ()

and objects_lacking_pointer_field_global_variables_unaddressed
  (vs: list var_id_t)
  (values: seq object_value_t)
  : Lemma (requires    (forall value. contains values value ==> object_value_valid value)
                    /\ (forall value. contains values value ==> object_td_lacks_pointer_field (object_value_to_td value)))
          (ensures     forall value. contains values value ==> global_variables_unaddressed_in_object_value vs value)
          (decreases   rank values)
  = if length values = 0 then
      ()
    else begin
      object_lacking_pointer_field_global_variables_unaddressed vs (index values 0);
      objects_lacking_pointer_field_global_variables_unaddressed vs (drop values 1)
    end

let rvalue_computation_lacking_pointer_field_global_variable_unaddrsessed
  (vs: list var_id_t)
  (exp: expression_t)
  (actor: tid_t)
  (s: Armada.State.t)
  : Lemma (requires expression_lacks_pointer_field exp)
          (ensures  otherwise true begin
                      let? value = rvalue_computation exp actor s in
                      return (global_variables_unaddressed_in_object_value vs value)
                    end)
  = match rvalue_computation exp actor s with
    | ComputationProduces value -> begin
      assert (object_value_valid value /\ object_value_to_td value == expression_to_td exp);
      object_lacking_pointer_field_global_variables_unaddressed vs value
      end
    | _ -> ()

let rvalue_computation_when_gvars_unaddressed_at_top_level_produces_value_with_gvars_unaddressed
  (vs: list var_id_t)
  (exp: expression_t)
  (actor: tid_t)
  (s: Armada.State.t)
  : Lemma (requires   global_variables_unaddressed_at_top_level_in_rvalue_expression vs exp
                    /\ inductive_invariant vs s)
          (ensures    otherwise true begin
                        let? value = rvalue_computation exp actor s in
                        return (global_variables_unaddressed_in_object_value vs value)
                      end)
    = if global_variables_unaddressed_in_rvalue_expression vs exp then
        rvalue_computation_when_gvars_unaddressed_produces_value_with_gvars_unaddressed vs exp actor s
      else
        rvalue_computation_lacking_pointer_field_global_variable_unaddrsessed vs exp actor s

let update_statement_unaddressable_global_vars_unaddressed_in_memory
  (vs: list var_id_t)
  (actor: tid_t)
  (step: Armada.Step.t)
  (starts_atomic_block ends_atomic_block: bool)
  (s: Armada.State.t)
  : Lemma (requires   UpdateStatement? step.action.program_statement.statement
                    /\ global_variables_unaddressable_in_statement vs step.action.program_statement.statement
                    /\ Some? (step_computation actor starts_atomic_block ends_atomic_block step s)
                    /\ inductive_invariant vs s)
          (ensures  global_variables_unaddressed_in_memory vs (Some?.v (step_computation actor starts_atomic_block ends_atomic_block step s)).mem)
  = if step.action.ok then begin
       let stmt = step.action.program_statement.statement in
       let thread = s.threads actor in
       let dst = UpdateStatement?.dst stmt in
       let src = UpdateStatement?.src stmt in
       let bypassing_write_buffer = UpdateStatement?.bypassing_write_buffer stmt in
       let new_value = ComputationProduces?.result (rvalue_computation src actor s) in
       rvalue_computation_when_gvars_unaddressed_at_top_level_produces_value_with_gvars_unaddressed vs src actor s;
       update_expression_with_gvars_unaddressed_maintains_gvars_unaddressed vs dst actor thread.pc 0 bypassing_write_buffer new_value s
    end

let nondeterministic_update_statement_unaddressable_global_vars_unaddressed_in_memory
  (vs: list var_id_t)
  (actor: tid_t)
  (step: Armada.Step.t)
  (starts_atomic_block ends_atomic_block: bool)
  (s: Armada.State.t)
  : Lemma (requires   NondeterministicUpdateStatement? step.action.program_statement.statement
                    /\ global_variables_unaddressable_in_statement vs step.action.program_statement.statement
                    /\ Some? (step_computation actor starts_atomic_block ends_atomic_block step s)
                    /\ inductive_invariant vs s)
          (ensures  global_variables_unaddressed_in_memory vs (Some?.v (step_computation actor starts_atomic_block ends_atomic_block step s)).mem)
  = if step.action.ok then begin
       let stmt = step.action.program_statement.statement in
       let thread = s.threads actor in
       let dst = NondeterministicUpdateStatement?.dst stmt in
       let nd_value = Cons?.hd step.nd in
       let bypassing_write_buffer = NondeterministicUpdateStatement?.bypassing_write_buffer stmt in
       update_expression_lacking_pointer_field_maintains_gvars_unaddressed vs dst actor thread.pc 0 bypassing_write_buffer nd_value s
    end

let propagate_write_message_statement_unaddressable_global_vars_unaddressed_in_memory
  (vs: list var_id_t)
  (actor: tid_t)
  (step: Armada.Step.t)
  (starts_atomic_block ends_atomic_block: bool)
  (s: Armada.State.t)
  : Lemma (requires   PropagateWriteMessageStatement? step.action.program_statement.statement
                    /\ global_variables_unaddressable_in_statement vs step.action.program_statement.statement
                    /\ Some? (step_computation actor starts_atomic_block ends_atomic_block step s)
                    /\ inductive_invariant vs s)
          (ensures  global_variables_unaddressed_in_memory vs (Some?.v (step_computation actor starts_atomic_block ends_atomic_block step s)).mem)
  = if step.action.ok then begin
       let ps = step.action.program_statement in
       let stmt = ps.statement in
       match stmt with
       | PropagateWriteMessageStatement -> begin
         let thread = s.threads actor in
         let start_pc = thread.pc in
         let receiver_tid: tid_t = ObjectValueAbstract?.value (Cons?.hd step.nd) in
         let propagator_thread = s.threads actor in
         let receiver_thread = s.threads receiver_tid in
         let which_message = receiver_thread.position_in_other_write_buffers actor in
         let write_message = index propagator_thread.write_buffer which_message in
         let position_in_other_write_buffers' =
           Spec.Map.upd receiver_thread.position_in_other_write_buffers actor (which_message + 1) in
         let receiver_thread' =
           { receiver_thread with position_in_other_write_buffers = position_in_other_write_buffers' } in
         let threads' = Spec.Map.upd s.threads receiver_tid receiver_thread' in
         match propagate_write_message write_message receiver_tid s.mem with
         | ComputationProduces mem' -> begin
           let p = write_message.location in
           let storage = ComputationProduces?.result (dereference_computation p s.mem) in
           dereference_computation_when_gvars_unaddressed_produces_storage_with_gvars_unaddressed vs p s.mem;
           match storage with
           | ObjectStorageWeaklyConsistentPrimitive primitive_td values local_versions ->
             let new_local_versions = Spec.Map.upd local_versions receiver_tid write_message.version in
             let new_storage = ObjectStorageWeaklyConsistentPrimitive primitive_td values new_local_versions in
             assert (global_variables_unaddressed_in_storage vs new_storage);
             update_pointer_directly_with_gvars_unaddressed_maintains_gvars_unaddressed vs p new_storage s.mem
           | _ -> ()
         end
         | _ -> ()
       end
       | _ -> ()
    end


let compare_and_swap_statement_unaddressable_global_vars_unaddressed_in_memory
  (vs: list var_id_t)
  (actor: tid_t)
  (step: Armada.Step.t)
  (starts_atomic_block ends_atomic_block: bool)
  (s: Armada.State.t)
  : Lemma (requires   CompareAndSwapStatement? step.action.program_statement.statement
                    /\ global_variables_unaddressable_in_statement vs step.action.program_statement.statement
                    /\ Some? (step_computation actor starts_atomic_block ends_atomic_block step s)
                    /\ inductive_invariant vs s)
          (ensures  global_variables_unaddressed_in_memory vs (Some?.v (step_computation actor starts_atomic_block ends_atomic_block step s)).mem)
  = if step.action.ok then begin
      let ps = step.action.program_statement in
      let thread = s.threads actor in
      let stmt = ps.statement in
      let target = CompareAndSwapStatement?.target stmt in
      let old_val = CompareAndSwapStatement?.old_val stmt in
      let new_val = CompareAndSwapStatement?.new_val stmt in
      let optional_result = CompareAndSwapStatement?.optional_result stmt in
      let bypassing_write_buffer = CompareAndSwapStatement?.bypassing_write_buffer stmt in
      let target_value = ComputationProduces?.result (rvalue_computation target actor s) in
      let old_value = ComputationProduces?.result (rvalue_computation old_val actor s) in
      let new_value = ComputationProduces?.result (rvalue_computation new_val actor s) in
      let target_ptr = ComputationProduces?.result (lvalue_computation target actor s) in
      rvalue_computation_when_gvars_unaddressed_at_top_level_produces_value_with_gvars_unaddressed vs new_val actor s;
      update_pointed_to_value_with_gvars_unaddressed_maintains_gvars_unaddressed
        vs target_ptr actor thread.pc 0 false new_value s;
      let swap = eqb target_value old_value in
      let s' = ComputationProduces?.result (if swap then update_expression target actor thread.pc 0 false new_value s
                                                    else return s) in
      match optional_result with
      | Some result ->
        let swap_value = ObjectValuePrimitive (PrimitiveBoxBool swap) in
        let result_ptr = ComputationProduces?.result (lvalue_computation result actor s) in
        assert (global_variables_unaddressed_in_object_value vs swap_value);
        update_pointed_to_value_with_gvars_unaddressed_maintains_gvars_unaddressed
          vs result_ptr actor thread.pc 1 bypassing_write_buffer swap_value s'
      | _ -> ()
    end

let expression_lvalue_computable_gvars_unaddressed_in_rvalue
  (vs: list var_id_t)
  (e: expression_t)
  (actor: tid_t)
  (s: Armada.State.t)
  : Lemma (requires begin match lvalue_computation e actor s with
                          | ComputationImpossible -> false
                          | _ -> true
                    end)
          (ensures  global_variables_unaddressed_in_rvalue_expression vs e)
  = ()

#push-options "--z3rlimit 30"

let atomic_exchange_statement_unaddressable_global_vars_unaddressed_in_memory
  (vs: list var_id_t)
  (actor: tid_t)
  (step: Armada.Step.t)
  (starts_atomic_block ends_atomic_block: bool)
  (s: Armada.State.t)
  : Lemma (requires   AtomicExchangeStatement? step.action.program_statement.statement
                    /\ global_variables_unaddressable_in_statement vs step.action.program_statement.statement
                    /\ Some? (step_computation actor starts_atomic_block ends_atomic_block step s)
                    /\ inductive_invariant vs s)
          (ensures  global_variables_unaddressed_in_memory vs (Some?.v (step_computation actor starts_atomic_block ends_atomic_block step s)).mem)
  = if step.action.ok then begin
       let ps = step.action.program_statement in
       let stmt = ps.statement in
       let thread = s.threads actor in
       let old_val = AtomicExchangeStatement?.old_val stmt in
       let old_ptr = ComputationProduces?.result (lvalue_computation old_val actor s) in
       let new_val = AtomicExchangeStatement?.new_val stmt in
       let new_value = ComputationProduces?.result (rvalue_computation new_val actor s) in
       let target = AtomicExchangeStatement?.target stmt in
       let target_value = ComputationProduces?.result (rvalue_computation target actor s) in
       let target_ptr = ComputationProduces?.result (lvalue_computation target actor s) in
       let s' = ComputationProduces?.result (update_pointed_to_value old_ptr actor thread.pc 0 false target_value s) in
       rvalue_computation_when_gvars_unaddressed_produces_value_with_gvars_unaddressed vs target actor s;
       expression_lvalue_computable_gvars_unaddressed_in_rvalue vs target actor s;
       update_pointed_to_value_with_gvars_unaddressed_maintains_gvars_unaddressed vs old_ptr actor thread.pc 0 false target_value s;
       rvalue_computation_when_gvars_unaddressed_at_top_level_produces_value_with_gvars_unaddressed vs new_val actor s;
       update_pointed_to_value_with_gvars_unaddressed_maintains_gvars_unaddressed vs target_ptr actor thread.pc 0 false new_value s'
    end

#pop-options
/
Util.Trigger.fst.checked Util.Seq.fsti.checked Strategies.Invariant.fsti.checked Strategies.GlobalVars.Util.fst.checked Strategies.GlobalVars.Unaddressed.fst.checked Strategies.GlobalVars.fst.checked Strategies.ArmadaStatement.fst.checked Strategies.ArmadaInvariant.RootsMatch.fst.checked Strategies.ArmadaInvariant.PositionsValid.fsti.checked Spec.Ubool.fst.checked Spec.Map.fst.checked Spec.List.fst.checked prims.fst.checked FStar.Sequence.Base.fsti.checked FStar.Sequence.Ambient.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked Armada.UnaryOp.fst.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.BinaryOp.fst.checked Armada.Base.fst.checked
Strategies.GlobalVars.UnaddressedStatement.fst

    vs: Prims.list Armada.Base.var_id_t ->
    exps: Prims.list Armada.Expression.expression_t ->
    actor: Armada.Base.tid_t ->
    s: Armada.State.t
  -> FStar.Pervasives.Lemma
      (requires
        Strategies.GlobalVars.global_variables_unaddressed_at_top_level_in_rvalue_expressions vs
          exps /\ Strategies.GlobalVars.UnaddressedStatement.inductive_invariant vs s)
      (ensures
        ((match Armada.Expression.rvalues_computation exps actor s with
            | Armada.Computation.ComputationProduces #_ values ->
              Strategies.GlobalVars.global_variables_unaddressed_in_object_values vs values
            | _ -> Prims.l_True)
          <:
          Type0))
      (decreases exps)
Prims.list Armada.Base.var_id_t Armada.Expression.expression_t Armada.Base.tid_t Armada.State.t Strategies.GlobalVars.UnaddressedStatement.rvalues_computation_when_gvars_unaddressed_at_top_level_produce_values_with_gvars_unaddressed Prims.unit Strategies.GlobalVars.UnaddressedStatement.rvalue_computation_when_gvars_unaddressed_at_top_level_produces_value_with_gvars_unaddressed Prims.l_and Prims.b2t Strategies.GlobalVars.global_variables_unaddressed_at_top_level_in_rvalue_expressions Strategies.GlobalVars.UnaddressedStatement.inductive_invariant Prims.squash Armada.Expression.rvalues_computation Armada.Type.object_value_t Strategies.GlobalVars.global_variables_unaddressed_in_object_values Armada.Computation.conditional_computation_t Prims.l_True Prims.Nil FStar.Pervasives.pattern
let rec rvalues_computation_when_gvars_unaddressed_at_top_level_produce_values_with_gvars_unaddressed
      (vs: list var_id_t)
      (exps: list expression_t)
      (actor: tid_t)
      (s: Armada.State.t)
    : Lemma
      (requires
        global_variables_unaddressed_at_top_level_in_rvalue_expressions vs exps /\
        inductive_invariant vs s)
      (ensures
        (match rvalues_computation exps actor s with
          | ComputationProduces values -> global_variables_unaddressed_in_object_values vs values
          | _ -> True))
      (decreases exps) =
  
match exps with
| [] -> ()
| exp :: exps' ->
  rvalue_computation_when_gvars_unaddressed_at_top_level_produces_value_with_gvars_unaddressed vs
    exp
    actor
    s;
  rvalues_computation_when_gvars_unaddressed_at_top_level_produce_values_with_gvars_unaddressed vs
    exps'
    actor
    s