val 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)
val 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)
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
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
/
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 ->
    actor: Armada.Base.tid_t ->
    step: Armada.Step.t ->
    starts_atomic_block: Prims.bool ->
    ends_atomic_block: Prims.bool ->
    s: Armada.State.t
  -> FStar.Pervasives.Lemma
      (requires
        UpdateStatement? (Mkprogram_statement_t?.statement (Mkt?.program_statement (Mkt?.action step
                  ))) /\
        Strategies.GlobalVars.global_variables_unaddressable_in_statement vs
          (Mkprogram_statement_t?.statement (Mkt?.program_statement (Mkt?.action step))) /\
        Some? (Armada.Transition.step_computation actor starts_atomic_block ends_atomic_block step s
          ) /\ Strategies.GlobalVars.UnaddressedStatement.inductive_invariant vs s)
      (ensures
        Strategies.GlobalVars.global_variables_unaddressed_in_memory vs
          (Mkt?.mem (Some?.v (Armada.Transition.step_computation actor
                      starts_atomic_block
                      ends_atomic_block
                      step
                      s))))
Prims.list Armada.Base.var_id_t Armada.Base.tid_t Armada.Step.t Prims.bool Armada.State.t Armada.Action.__proj__Mkt__item__ok Armada.Step.__proj__Mkt__item__action Strategies.GlobalVars.Unaddressed.update_expression_with_gvars_unaddressed_maintains_gvars_unaddressed Armada.Thread.__proj__Mkt__item__pc Prims.unit Strategies.GlobalVars.UnaddressedStatement.rvalue_computation_when_gvars_unaddressed_at_top_level_produces_value_with_gvars_unaddressed Armada.Type.valid_object_value_t Armada.Expression.expression_to_td Armada.Computation.__proj__ComputationProduces__item__result Armada.Expression.rvalue_computation Armada.Statement.__proj__UpdateStatement__item__bypassing_write_buffer Armada.Expression.expression_t Armada.Statement.__proj__UpdateStatement__item__src Armada.Statement.__proj__UpdateStatement__item__dst Armada.Thread.t Armada.State.__proj__Mkt__item__threads Armada.Statement.t Armada.Action.__proj__Mkprogram_statement_t__item__statement Armada.Action.__proj__Mkt__item__program_statement Prims.l_and Prims.b2t Armada.Statement.uu___is_UpdateStatement Strategies.GlobalVars.global_variables_unaddressable_in_statement FStar.Pervasives.Native.uu___is_Some Armada.Transition.step_computation Strategies.GlobalVars.UnaddressedStatement.inductive_invariant Prims.squash Strategies.GlobalVars.global_variables_unaddressed_in_memory Armada.State.__proj__Mkt__item__mem FStar.Pervasives.Native.__proj__Some__item__v Prims.Nil FStar.Pervasives.pattern
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
  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