val 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)
val 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)
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
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
/
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 -> value: Armada.Type.object_value_t
  -> FStar.Pervasives.Lemma
      (requires
        Strategies.GlobalVars.object_td_lacks_pointer_field (Armada.Type.object_value_to_td value) /\
        Armada.Type.object_value_valid value)
      (ensures Strategies.GlobalVars.global_variables_unaddressed_in_object_value vs value)
      (decreases FStar.Sequence.Base.rank value)
Prims.list Armada.Base.var_id_t Armada.Type.object_value_t Armada.Type.primitive_box_t FStar.Sequence.Base.seq Strategies.GlobalVars.UnaddressedStatement.objects_lacking_pointer_field_global_variables_unaddressed Armada.Type.object_td_t Strategies.GlobalVars.global_variables_unaddressed_in_object_value_seq_equivalent_to_forall Prims.unit Prims.l_and Prims.b2t Strategies.GlobalVars.object_td_lacks_pointer_field Armada.Type.object_value_to_td Armada.Type.object_value_valid Prims.squash Strategies.GlobalVars.global_variables_unaddressed_in_object_value Prims.Nil FStar.Pervasives.pattern
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 ->
  objects_lacking_pointer_field_global_variables_unaddressed vs elements;
  global_variables_unaddressed_in_object_value_seq_equivalent_to_forall vs elements
| ObjectValueAbstract _ _ -> ()