val root_matches_root_id (root: root_t) (root_id: root_id_t) : GTot bool
val root_matches_root_id (root: root_t) (root_id: root_id_t) : GTot bool
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
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
/
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
root: Armada.Memory.root_t -> root_id: Armada.Base.root_id_t -> Prims.GTot Prims.bool
Armada.Memory.root_t Armada.Base.root_id_t Armada.Memory.valid_object_storage_t Armada.Base.uu___is_RootIdGlobal Prims.bool Armada.Base.uu___is_RootIdStack Armada.Base.uu___is_RootIdAllocation Prims.op_AmpAmp Armada.Base.uu___is_RootIdFence Spec.Ubool.eqb Armada.Type.object_td_t Armada.Memory.object_storage_to_td Armada.Type.ObjectTDPrimitive Armada.Type.PrimitiveTDBool
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