val init_implies_roots_match (program: Armada.Program.t) (s: Armada.State.t)
    : Lemma (requires init_program program s) (ensures roots_match s.mem)
val init_implies_roots_match (program: Armada.Program.t) (s: Armada.State.t)
    : Lemma (requires init_program program s) (ensures roots_match s.mem)
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)
  )
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
/
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
program: Armada.Program.t -> s: Armada.State.t
  -> FStar.Pervasives.Lemma (requires Armada.Program.init_program program s)
      (ensures Strategies.ArmadaInvariant.RootsMatch.roots_match (Mkt?.mem s))
Armada.Program.t Armada.State.t FStar.Classical.Sugar.forall_intro Armada.Base.root_id_t Prims.b2t Strategies.ArmadaInvariant.RootsMatch.root_matches_root_id Armada.State.__proj__Mkt__item__mem Prims._assert Armada.Init.root_invalid_outside_initializations Armada.Program.__proj__Mkt__item__global_initializers Armada.State.__proj__Mkt__item__initial_tid Armada.Program.__proj__Mkt__item__main_method_id Armada.Thread.__proj__Mkstack_frame_t__item__local_variables Armada.Thread.__proj__Mkt__item__top Armada.Base.root_id_uniquifier_t Prims.__proj__Cons__item__hd Armada.State.__proj__Mkt__item__uniqs_used Armada.Thread.t Armada.State.__proj__Mkt__item__threads Prims.squash Prims.unit Armada.Program.init_program Strategies.ArmadaInvariant.RootsMatch.roots_match Prims.Nil FStar.Pervasives.pattern
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))