val 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)
val 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)
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 -> values: FStar.Sequence.Base.seq Armada.Type.object_value_t
  -> FStar.Pervasives.Lemma
      (requires
        (forall (value: Armada.Type.object_value_t).
            FStar.Sequence.Base.contains values value ==> Armada.Type.object_value_valid value) /\
        (forall (value: Armada.Type.object_value_t).
            FStar.Sequence.Base.contains values value ==>
            Strategies.GlobalVars.object_td_lacks_pointer_field (Armada.Type.object_value_to_td value
                )))
      (ensures
        forall (value: Armada.Type.object_value_t).
          FStar.Sequence.Base.contains values value ==>
          Strategies.GlobalVars.global_variables_unaddressed_in_object_value vs value)
      (decreases FStar.Sequence.Base.rank values)
Prims.list Armada.Base.var_id_t FStar.Sequence.Base.seq Armada.Type.object_value_t Prims.op_Equality Prims.int FStar.Sequence.Base.length Prims.bool Strategies.GlobalVars.UnaddressedStatement.objects_lacking_pointer_field_global_variables_unaddressed FStar.Sequence.Base.drop Prims.unit Strategies.GlobalVars.UnaddressedStatement.object_lacking_pointer_field_global_variables_unaddressed FStar.Sequence.Base.index Prims.l_and Prims.l_Forall Prims.l_imp FStar.Sequence.Base.contains Prims.b2t Armada.Type.object_value_valid Strategies.GlobalVars.object_td_lacks_pointer_field Armada.Type.object_value_to_td Prims.squash Strategies.GlobalVars.global_variables_unaddressed_in_object_value Prims.Nil FStar.Pervasives.pattern
let rec 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
  (object_lacking_pointer_field_global_variables_unaddressed vs (index values 0);
    objects_lacking_pointer_field_global_variables_unaddressed vs (drop values 1))