val update_pointer_directly_maintains_roots_match
      (p: Armada.Pointer.t)
      (new_storage: valid_object_storage_t)
      (mem: Armada.Memory.t)
    : Lemma (requires roots_match mem)
      (ensures
        (match update_pointer_directly p new_storage mem with
          | ComputationProduces mem' -> roots_match mem'
          | _ -> True))
val update_pointer_directly_maintains_roots_match
      (p: Armada.Pointer.t)
      (new_storage: valid_object_storage_t)
      (mem: Armada.Memory.t)
    : Lemma (requires roots_match mem)
      (ensures
        (match update_pointer_directly p new_storage mem with
          | ComputationProduces mem' -> roots_match mem'
          | _ -> True))
let rec update_pointer_directly_maintains_roots_match
  (p: Armada.Pointer.t)
  (new_storage: valid_object_storage_t)
  (mem: Armada.Memory.t)
  : Lemma (requires roots_match mem)
          (ensures  (match update_pointer_directly p new_storage mem with
                     | ComputationProduces mem' -> roots_match mem'
                     | _ -> True)) =
  match update_pointer_directly p new_storage mem with
  | ComputationImpossible | ComputationUndefined -> ()
  | ComputationProduces mem' ->
      (match p with
       | PointerField struct_ptr field_id ->
           let parent = ComputationProduces?.result (dereference_computation struct_ptr mem) in
           (match parent with
            | ObjectStorageStruct fields ->
                let new_parent = update_storage_child parent field_id new_storage in
                update_pointer_directly_maintains_roots_match struct_ptr new_parent mem)
       | PointerIndex array_ptr idx ->
           let parent = ComputationProduces?.result (dereference_computation array_ptr mem) in
           (match parent with
            | ObjectStorageArray element_td elements ->
                let new_parent = update_storage_child parent idx new_storage in
                update_pointer_directly_maintains_roots_match array_ptr new_parent mem)
       | PointerRoot root_id -> ()
       | _ -> ())
module Strategies.ArmadaInvariant.RootsMatch

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.Transition
open Armada.Type
open FStar.Sequence.Base
open FStar.Tactics.V2
open Spec.List
open Spec.Map
open Spec.Ubool
open Strategies.ArmadaStatement
open Util.Tactics

let root_matches_root_id (root: root_t) (root_id: root_id_t) : GTot bool =
  match root with
  | RootGlobal _ -> RootIdGlobal? root_id
  | RootStackVariable _ _ _ -> RootIdStack? root_id
  | RootAllocated _ _ _ -> RootIdAllocation? root_id
  | RootFence storage ->
          RootIdFence? root_id
       && eqb (object_storage_to_td storage) (ObjectTDPrimitive PrimitiveTDBool)
  | RootInvalid -> true

let roots_match (mem: Armada.Memory.t) : ubool =
  forall root_id. root_matches_root_id (mem root_id) root_id

let init_implies_roots_match (program: Armada.Program.t) (s: Armada.State.t)
  : Lemma (requires init_program program s)
          (ensures  roots_match s.mem) =
  let thread = s.threads s.initial_tid in
  let initial_frame_uniq = Cons?.hd s.uniqs_used in
  introduce forall root_id. root_matches_root_id (s.mem root_id) root_id
  with (
    let thread = s.threads s.initial_tid in
    let initial_frame_uniq = Cons?.hd s.uniqs_used in
    assert (root_invalid_outside_initializations s.mem program.global_initializers s.initial_tid
              program.main_method_id initial_frame_uniq thread.top.local_variables root_id)
  )
/
Util.Tactics.fst.checked Strategies.ArmadaStatement.fst.checked Spec.Ubool.fst.checked Spec.Map.fst.checked Spec.List.fst.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Sequence.Base.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked Armada.Type.fst.checked Armada.Transition.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.RootsMatch.fst
p: Armada.Pointer.t -> new_storage: Armada.Memory.valid_object_storage_t -> mem: Armada.Memory.t
  -> FStar.Pervasives.Lemma (requires Strategies.ArmadaInvariant.RootsMatch.roots_match mem)
      (ensures
        ((match Armada.Memory.update_pointer_directly p new_storage mem with
            | Armada.Computation.ComputationProduces #_ mem' ->
              Strategies.ArmadaInvariant.RootsMatch.roots_match mem'
            | _ -> Prims.l_True)
          <:
          Type0))
Armada.Pointer.t Armada.Memory.valid_object_storage_t Armada.Memory.t Armada.Memory.update_pointer_directly Prims.nat FStar.Sequence.Base.seq Armada.Memory.object_storage_t Strategies.ArmadaInvariant.RootsMatch.update_pointer_directly_maintains_roots_match Armada.Memory.update_storage_child Prims.unit Armada.Computation.__proj__ComputationProduces__item__result Armada.Memory.dereference_computation Armada.Type.object_td_t Armada.Base.root_id_t Strategies.ArmadaInvariant.RootsMatch.roots_match Prims.squash Armada.Computation.conditional_computation_t Prims.l_True Prims.Nil FStar.Pervasives.pattern
let rec update_pointer_directly_maintains_roots_match
      (p: Armada.Pointer.t)
      (new_storage: valid_object_storage_t)
      (mem: Armada.Memory.t)
    : Lemma (requires roots_match mem)
      (ensures
        (match update_pointer_directly p new_storage mem with
          | ComputationProduces mem' -> roots_match mem'
          | _ -> True)) =
  
match update_pointer_directly p new_storage mem with
| ComputationImpossible | ComputationUndefined -> ()
| ComputationProduces mem' ->
  (match p with
    | PointerField struct_ptr field_id ->
      let parent = ComputationProduces?.result (dereference_computation struct_ptr mem) in
      (match parent with
        | ObjectStorageStruct fields ->
          let new_parent = update_storage_child parent field_id new_storage in
          update_pointer_directly_maintains_roots_match struct_ptr new_parent mem)
    | PointerIndex array_ptr idx ->
      let parent = ComputationProduces?.result (dereference_computation array_ptr mem) in
      (match parent with
        | ObjectStorageArray element_td elements ->
          let new_parent = update_storage_child parent idx new_storage in
          update_pointer_directly_maintains_roots_match array_ptr new_parent mem)
    | PointerRoot root_id -> ()
    | _ -> ())