val push_stack_variable_maintains_roots_match
      (actor: tid_t)
      (writer_pc: pc_t)
      (writer_expression_number: nat)
      (method_id: method_id_t)
      (frame_uniq: root_id_uniquifier_t)
      (initializer: initializer_t)
      (s: Armada.State.t)
    : Lemma (requires roots_match s.mem)
      (ensures
        (match
            push_stack_variable actor
              writer_pc
              writer_expression_number
              method_id
              frame_uniq
              initializer
              s
          with
          | ComputationImpossible | ComputationUndefined -> True
          | ComputationProduces s' -> roots_match s'.mem))
val push_stack_variable_maintains_roots_match
      (actor: tid_t)
      (writer_pc: pc_t)
      (writer_expression_number: nat)
      (method_id: method_id_t)
      (frame_uniq: root_id_uniquifier_t)
      (initializer: initializer_t)
      (s: Armada.State.t)
    : Lemma (requires roots_match s.mem)
      (ensures
        (match
            push_stack_variable actor
              writer_pc
              writer_expression_number
              method_id
              frame_uniq
              initializer
              s
          with
          | ComputationImpossible | ComputationUndefined -> True
          | ComputationProduces s' -> roots_match s'.mem))
let push_stack_variable_maintains_roots_match
  (actor: tid_t)
  (writer_pc: pc_t)
  (writer_expression_number: nat)
  (method_id: method_id_t)
  (frame_uniq: root_id_uniquifier_t)
  (initializer: initializer_t)
  (s: Armada.State.t)
  : Lemma (requires roots_match s.mem)
          (ensures  (match push_stack_variable actor writer_pc writer_expression_number method_id frame_uniq
                             initializer s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> roots_match s'.mem)) =
  let root_id = RootIdStack actor method_id frame_uniq initializer.var_id in
  let root = s.mem root_id in
  if not (stack_variable_ready_for_push root initializer) then
    ()
  else
    let thread = s.threads actor in
    let var_id = initializer.var_id in
    if list_contains var_id thread.top.local_variables then
      ()
    else
      let local_variables' = var_id :: thread.top.local_variables in
      let top' = { thread.top with local_variables = local_variables' } in
      let thread' = { thread with top = top' } in
      let threads' = Spec.Map.upd s.threads actor thread' in
      let root' = RootStackVariable true false (RootStackVariable?.storage root) in
      let mem' = upd s.mem root_id root' in
      let s' = { s with mem = mem'; threads = threads' } in
      (match initializer.iv with
       | InitializerArbitrary td -> ()
       | InitializerSpecific value ->
           let td = (object_value_to_td value) in
           update_expression_maintains_roots_match (ExpressionLocalVariable td var_id) actor writer_pc
             writer_expression_number false value s')
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)
  )

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 -> ()
       | _ -> ())

#push-options "--z3rlimit 10"

let update_pointer_maintains_roots_match
  (p: Armada.Pointer.t)
  (actor: tid_t)
  (writer_pc: pc_t)
  (writer_expression_number: nat)
  (bypassing_write_buffer: bool)
  (new_value: object_value_t)
  (mem: Armada.Memory.t)
  : Lemma (requires roots_match mem)
          (ensures  (match update_pointer p actor writer_pc writer_expression_number bypassing_write_buffer
                             new_value mem with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces (optional_write_message, mem') -> roots_match mem')) =
  match p with
  | PointerUninitialized -> ()
  | PointerNull -> ()
  | PointerRoot root_id -> ()
  | PointerField struct_ptr field_id ->
      (match dereference_computation struct_ptr mem with
       | ComputationImpossible | ComputationUndefined -> ()
       | ComputationProduces parent ->
           (match parent with
            | ObjectStorageStruct fields ->
                if field_id >= length fields then
                  ()
                else
                  let field = index fields field_id in
                  if   not (object_storage_valid field)
                     || neqb (object_storage_to_td field) (object_value_to_td new_value) then
                    ()
                  else
                    (match update_storage p actor writer_pc writer_expression_number
                             bypassing_write_buffer field new_value with
                     | ComputationImpossible | ComputationUndefined -> ()
                     | ComputationProduces (write_message, new_field) ->
                         if (not (can_update_storage_child parent field_id new_field)) then
                           ()
                         else
                           let new_parent = update_storage_child parent field_id new_field in
                           update_pointer_directly_maintains_roots_match struct_ptr new_parent mem)
            | _ -> ()))
  | PointerIndex array_ptr idx ->
      (match dereference_computation array_ptr mem with
       | ComputationImpossible | ComputationUndefined -> ()
       | ComputationProduces parent ->
           (match parent with
            | ObjectStorageArray element_td elements ->
                if idx < 0 || idx >= length elements then
                  ()
                else
                  let element = index elements idx in
                  if not (object_storage_valid element) then
                    ()
                  else
                    (match update_storage p actor writer_pc writer_expression_number
                             bypassing_write_buffer element new_value with
                     | ComputationImpossible | ComputationUndefined -> ()
                     | ComputationProduces (write_message, new_element) ->
                         if not (can_update_storage_child parent idx new_element) then
                           ()
                         else
                           let new_parent = update_storage_child parent idx new_element in
                           update_pointer_directly_maintains_roots_match array_ptr new_parent mem)
            | _ -> ()))

#pop-options

let update_pointed_to_value_maintains_roots_match
  (p: Armada.Pointer.t)
  (actor: tid_t)
  (writer_pc: pc_t)
  (writer_expression_number: nat)
  (bypassing_write_buffer: bool)
  (new_value: object_value_t)
  (s: Armada.State.t)
  : Lemma (requires roots_match s.mem)
          (ensures  (match update_pointed_to_value p actor writer_pc writer_expression_number bypassing_write_buffer
                             new_value s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> roots_match s'.mem)) =
  update_pointer_maintains_roots_match p actor writer_pc writer_expression_number bypassing_write_buffer
    new_value s.mem

let update_expression_maintains_roots_match
  (exp: expression_t)
  (actor: tid_t)
  (writer_pc: pc_t)
  (writer_expression_number: nat)
  (bypassing_write_buffer: bool)
  (new_value: object_value_t)
  (s: Armada.State.t)
  : Lemma (requires roots_match s.mem)
          (ensures  (match update_expression exp actor writer_pc writer_expression_number bypassing_write_buffer
                             new_value s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> roots_match s'.mem)) =
  let s' = update_expression exp actor writer_pc writer_expression_number bypassing_write_buffer
             new_value s in
  if   not (expression_valid exp)
     || not (object_value_valid new_value)
     || neqb (object_value_to_td new_value) (expression_to_td exp) then
    ()
  else (
    match lvalue_computation exp actor s with
    | ComputationImpossible | ComputationUndefined -> ()
    | ComputationProduces p ->
        update_pointed_to_value_maintains_roots_match p actor writer_pc writer_expression_number
          bypassing_write_buffer new_value s
  )

let rec update_expressions_maintains_roots_match
  (exps: list expression_t)
  (actor: tid_t)
  (writer_pc: pc_t)
  (writer_expression_number: nat)
  (bypassing_write_buffer: bool)
  (new_values: list object_value_t)
  (s: Armada.State.t)
  : Lemma (requires roots_match s.mem)
          (ensures  (match update_expressions exps actor writer_pc writer_expression_number bypassing_write_buffer
                             new_values s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> roots_match s'.mem))
          (decreases exps) =
  match exps, new_values with
  | [], [] -> ()
  | first_exp :: remaining_exps, first_new_value :: remaining_new_values ->
      update_expression_maintains_roots_match first_exp actor writer_pc writer_expression_number
        bypassing_write_buffer first_new_value s;
      (match update_expression first_exp actor writer_pc writer_expression_number
               bypassing_write_buffer first_new_value s with
       | ComputationImpossible | ComputationUndefined -> ()
       | ComputationProduces s' ->
           update_expressions_maintains_roots_match remaining_exps actor writer_pc
             (writer_expression_number + 1) bypassing_write_buffer remaining_new_values s')
  | _ -> ()
/
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

    actor: Armada.Base.tid_t ->
    writer_pc: Armada.Base.pc_t ->
    writer_expression_number: Prims.nat ->
    method_id: Armada.Base.method_id_t ->
    frame_uniq: Armada.Base.root_id_uniquifier_t ->
    initializer: Armada.Init.initializer_t ->
    s: Armada.State.t
  -> FStar.Pervasives.Lemma
      (requires Strategies.ArmadaInvariant.RootsMatch.roots_match (Mkt?.mem s))
      (ensures
        ((match
              Armada.Init.push_stack_variable actor
                writer_pc
                writer_expression_number
                method_id
                frame_uniq
                initializer
                s
            with
            | Armada.Computation.ComputationImpossible #_ -> Prims.l_True
            | Armada.Computation.ComputationUndefined #_ -> Prims.l_True
            | Armada.Computation.ComputationProduces #_ s' ->
              Strategies.ArmadaInvariant.RootsMatch.roots_match (Mkt?.mem s'))
          <:
          Type0))
Armada.Base.tid_t Armada.Base.pc_t Prims.nat Armada.Base.method_id_t Armada.Base.root_id_uniquifier_t Armada.Init.initializer_t Armada.State.t Prims.op_Negation Armada.Init.stack_variable_ready_for_push Prims.bool Spec.List.list_contains Armada.Base.var_id_t Armada.Thread.__proj__Mkstack_frame_t__item__local_variables Armada.Thread.__proj__Mkt__item__top Armada.Init.__proj__Mkinitializer_t__item__iv Armada.Type.object_td_t Armada.Type.object_value_t Strategies.ArmadaInvariant.RootsMatch.update_expression_maintains_roots_match Armada.Expression.ExpressionLocalVariable Armada.Type.object_value_to_td Prims.unit Armada.State.Mkt Armada.State.__proj__Mkt__item__initial_tid Armada.State.__proj__Mkt__item__uniqs_used Armada.State.__proj__Mkt__item__trace Armada.State.__proj__Mkt__item__stop_reason Spec.Map.t Armada.Base.root_id_t Armada.Memory.root_t Spec.Map.upd Armada.State.__proj__Mkt__item__mem Armada.Memory.RootStackVariable Armada.Memory.__proj__RootStackVariable__item__storage Armada.Thread.t Armada.State.__proj__Mkt__item__threads Armada.Thread.Mkt Armada.Thread.__proj__Mkt__item__status Armada.Thread.__proj__Mkt__item__pc Armada.Thread.__proj__Mkt__item__stack Armada.Thread.__proj__Mkt__item__write_buffer Armada.Thread.__proj__Mkt__item__position_in_other_write_buffers Armada.Thread.stack_frame_t Armada.Thread.Mkstack_frame_t Armada.Thread.__proj__Mkstack_frame_t__item__method_id Armada.Thread.__proj__Mkstack_frame_t__item__frame_uniq Prims.list Prims.Cons Armada.Init.__proj__Mkinitializer_t__item__var_id Armada.Base.RootIdStack Strategies.ArmadaInvariant.RootsMatch.roots_match Prims.squash Armada.Init.push_stack_variable Prims.l_True Prims.Nil FStar.Pervasives.pattern
let push_stack_variable_maintains_roots_match
      (actor: tid_t)
      (writer_pc: pc_t)
      (writer_expression_number: nat)
      (method_id: method_id_t)
      (frame_uniq: root_id_uniquifier_t)
      (initializer: initializer_t)
      (s: Armada.State.t)
    : Lemma (requires roots_match s.mem)
      (ensures
        (match
            push_stack_variable actor
              writer_pc
              writer_expression_number
              method_id
              frame_uniq
              initializer
              s
          with
          | ComputationImpossible | ComputationUndefined -> True
          | ComputationProduces s' -> roots_match s'.mem)) =
  
let root_id = RootIdStack actor method_id frame_uniq initializer.var_id in
let root = s.mem root_id in
if not (stack_variable_ready_for_push root initializer)
then ()
else
  let thread = s.threads actor in
  let var_id = initializer.var_id in
  if list_contains var_id thread.top.local_variables
  then ()
  else
    let local_variables' = var_id :: thread.top.local_variables in
    let top' = { thread.top with local_variables = local_variables' } in
    let thread' = { thread with top = top' } in
    let threads' = Spec.Map.upd s.threads actor thread' in
    let root' = RootStackVariable true false (RootStackVariable?.storage root) in
    let mem' = upd s.mem root_id root' in
    let s' = { s with mem = mem'; threads = threads' } in
    (match initializer.iv with
      | InitializerArbitrary td -> ()
      | InitializerSpecific value ->
        let td = (object_value_to_td value) in
        update_expression_maintains_roots_match (ExpressionLocalVariable td var_id)
          actor
          writer_pc
          writer_expression_number
          false
          value
          s')