val get_propagate_lifter_case_skip_helper
      (vr: var_intro_relation_t)
      (actor: tid_t)
      (nd: nondeterminism_t)
      (ls hs: Armada.State.t)
      (receiver_tid: tid_t)
      (step: Armada.Step.t)
    : Lemma
      (requires
        var_intro_lh_relation vr () ls hs /\ NotStopped? hs.stop_reason /\
        ThreadStatusRunning? (hs.threads actor).status /\
        step == { nd = nd; action = propagate_action } /\ list_len nd = 1 /\
        object_value_to_td (Cons?.hd nd) == ObjectTDAbstract tid_t /\
        receiver_tid == ObjectValueAbstract?.value (Cons?.hd nd) /\ receiver_tid <> actor /\
        ComputationProduces? (propagate_write_message_statement_computation actor nd ls) /\
        (let lthread = ls.threads actor in
          let lwrite_buffer = lthread.write_buffer in
          let lposition = (ls.threads receiver_tid).position_in_other_write_buffers actor in
          let lwrite_message = index lwrite_buffer lposition in
          let lunread_write_buffer = unread_write_buffer ls.threads actor receiver_tid in
          ThreadStatusRunning? lthread.status /\
          not (global_variables_unaddressed_in_write_message vr.vs lwrite_message)))
      (ensures
        (match propagate_write_message_statement_computation actor nd ls with
          | ComputationProduces ls' -> var_intro_lh_relation vr () ls' hs))
val get_propagate_lifter_case_skip_helper
      (vr: var_intro_relation_t)
      (actor: tid_t)
      (nd: nondeterminism_t)
      (ls hs: Armada.State.t)
      (receiver_tid: tid_t)
      (step: Armada.Step.t)
    : Lemma
      (requires
        var_intro_lh_relation vr () ls hs /\ NotStopped? hs.stop_reason /\
        ThreadStatusRunning? (hs.threads actor).status /\
        step == { nd = nd; action = propagate_action } /\ list_len nd = 1 /\
        object_value_to_td (Cons?.hd nd) == ObjectTDAbstract tid_t /\
        receiver_tid == ObjectValueAbstract?.value (Cons?.hd nd) /\ receiver_tid <> actor /\
        ComputationProduces? (propagate_write_message_statement_computation actor nd ls) /\
        (let lthread = ls.threads actor in
          let lwrite_buffer = lthread.write_buffer in
          let lposition = (ls.threads receiver_tid).position_in_other_write_buffers actor in
          let lwrite_message = index lwrite_buffer lposition in
          let lunread_write_buffer = unread_write_buffer ls.threads actor receiver_tid in
          ThreadStatusRunning? lthread.status /\
          not (global_variables_unaddressed_in_write_message vr.vs lwrite_message)))
      (ensures
        (match propagate_write_message_statement_computation actor nd ls with
          | ComputationProduces ls' -> var_intro_lh_relation vr () ls' hs))
let get_propagate_lifter_case_skip_helper
  (vr: var_intro_relation_t)
  (actor: tid_t)
  (nd: nondeterminism_t)
  (ls: Armada.State.t)
  (hs: Armada.State.t)
  (receiver_tid: tid_t)
  (step: Armada.Step.t)
  : Lemma (requires   var_intro_lh_relation vr () ls hs
                    /\ NotStopped? hs.stop_reason
                    /\ ThreadStatusRunning? (hs.threads actor).status
                    /\ step == { nd = nd; action = propagate_action }
                    /\ list_len nd = 1
                    /\ object_value_to_td (Cons?.hd nd) == ObjectTDAbstract tid_t
                    /\ receiver_tid == ObjectValueAbstract?.value (Cons?.hd nd)
                    /\ receiver_tid <> actor
                    /\ ComputationProduces? (propagate_write_message_statement_computation actor nd ls)
                    /\ (let lthread = ls.threads actor in
                       let lwrite_buffer = lthread.write_buffer in
                       let lposition = (ls.threads receiver_tid).position_in_other_write_buffers actor in
                       let lwrite_message = index lwrite_buffer lposition in
                       let lunread_write_buffer = unread_write_buffer ls.threads actor receiver_tid in
                         ThreadStatusRunning? lthread.status
                       /\ not (global_variables_unaddressed_in_write_message vr.vs lwrite_message)))
          (ensures  (match propagate_write_message_statement_computation actor nd ls with
                     | ComputationProduces ls' -> var_intro_lh_relation vr () ls' hs)) =
  let lunread_write_buffer = unread_write_buffer ls.threads actor receiver_tid in
  let hunread_write_buffer = unread_write_buffer hs.threads actor receiver_tid in
  let pc_relation = var_intro_pc_relation vr.hpc_to_lpc vr.return_hpcs vr.return_pcs_unique_proof in
  if   list_len nd <> 1
     || neqb (object_value_to_td (Cons?.hd nd)) (ObjectTDAbstract tid_t) then
    false_elim ()
  else
    let receiver_tid: tid_t = ObjectValueAbstract?.value (Cons?.hd nd) in
    if receiver_tid = actor then // can't propagate to the same thread
      false_elim ()
    else
      let propagator_thread = ls.threads actor in
      let receiver_thread = ls.threads receiver_tid in
      let which_message = receiver_thread.position_in_other_write_buffers actor in
      if which_message >= length propagator_thread.write_buffer then
        false_elim ()
      else (
        let write_message = index propagator_thread.write_buffer which_message in
        let position_in_other_write_buffers' =
          Spec.Map.upd receiver_thread.position_in_other_write_buffers actor (which_message + 1) in
        let receiver_thread' =
          { receiver_thread with position_in_other_write_buffers = position_in_other_write_buffers' } in
        let threads' = Spec.Map.upd ls.threads receiver_tid receiver_thread' in
        assert (positions_valid_in_threads threads');
        let lem () : Lemma (positions_in_write_buffers_match_except_global_variables vr.vs threads' hs.threads) =
        (
          introduce forall sender_tid' receiver_tid'. sender_receiver_trigger sender_tid' receiver_tid' ==>
                        write_buffers_match_except_global_variables vr.vs
                          (unread_write_buffer threads' sender_tid' receiver_tid')
                          (unread_write_buffer hs.threads sender_tid' receiver_tid')
          with introduce _ ==> _
          with _. (
            assert (position_valid ls.threads sender_tid' receiver_tid');
            assert (write_buffers_match_except_global_variables vr.vs
                      (unread_write_buffer ls.threads sender_tid' receiver_tid')
                      (unread_write_buffer hs.threads sender_tid' receiver_tid'));
            if receiver_tid <> receiver_tid' then
              ()
            else if actor <> sender_tid' then
              ()
            else (
              assert (unread_write_buffer hs.threads sender_tid' receiver_tid' == hunread_write_buffer);
              assert (unread_write_buffer threads' sender_tid' receiver_tid' == drop lunread_write_buffer 1);
              seq_to_list_drop_equals_tail lunread_write_buffer
            )
          )
        ) in
        lem ();
        assert (positions_in_write_buffers_match_except_global_variables vr.vs threads' hs.threads);
        match propagate_write_message write_message receiver_tid ls.mem with
        | ComputationImpossible
        | ComputationUndefined ->
            // If propagate would trigger undefined behavior (e.g., by propagating to freed memory),
            // it just leaves memory unchanged.
            let ls' = { ls with threads = threads'; } in
            assert (states_match_except_global_variables vr.vs pc_relation ls' hs);
            assert (unstarted_threads_have_empty_write_buffers ls');
            assert (global_variables_unaddressed_in_memory vr.vs ls'.mem);
            assert (roots_match ls'.mem);
            assert (var_intro_lh_relation vr () ls' hs)
        | ComputationProduces mem' ->
            let ls' = { ls with mem = mem'; threads = threads'; } in
            propagate_write_message_statement_computation_s1_only_maintains_states_match vr.vs pc_relation actor nd
              ls hs;
            assert (unstarted_threads_have_empty_write_buffers ls');
            propagate_write_message_maintains_gvars_unaddressed vr.vs write_message receiver_tid ls.mem;
            assert (global_variables_unaddressed_in_memory vr.vs ls'.mem);
            assert (roots_match ls'.mem);
            assert (var_intro_lh_relation vr () ls' hs)
      )
module Strategies.VarIntro.Propagate

open Armada.Action
open Armada.Base
open Armada.Computation
open Armada.Init
open Armada.Memory
open Armada.Program
open Armada.State
open Armada.Step
open Armada.Statement
open Armada.Thread
open Armada.Threads
open Armada.Transition
open Armada.Type
open FStar.Sequence.Ambient
open FStar.Sequence.Base
open FStar.WellFoundedRelation
open Spec.Behavior
open Spec.List
open Spec.Ubool
open Strategies.ArmadaInvariant.RootsMatch
open Strategies.ArmadaInvariant.PositionsValid
open Strategies.ArmadaStatement.Propagate
open Strategies.ArmadaInvariant.UnstartedThreads
open Strategies.ArmadaStatement.Status
open Strategies.ArmadaStatement.ThreadState
open Strategies.Atomic
open Strategies.GlobalVars
open Strategies.GlobalVars.Init
open Strategies.GlobalVars.Statement
open Strategies.GlobalVars.Types
open Strategies.GlobalVars.Unaddressed
open Strategies.GlobalVars.Util
open Strategies.GlobalVars.VarHiding
open Strategies.GlobalVars.VarIntro
open Strategies.Lift.Generic
open Strategies.Invariant
open Strategies.PCRelation
open Strategies.Semantics
open Strategies.Semantics.Armada
open Strategies.VarIntro.Defs
open Strategies.VarIntro.Helpers
open Strategies.VarIntro.Initialization
open Strategies.VarIntro.Invariant
open Util.List
open Util.Nth
open Util.Seq

let propagate_action: Armada.Action.t =
  { ok = true; program_statement = propagate_program_statement }

#push-options "--z3rlimit 20"
/
Util.Seq.fsti.checked Util.Nth.fst.checked Util.List.fst.checked Strategies.VarIntro.Invariant.fst.checked Strategies.VarIntro.Initialization.fsti.checked Strategies.VarIntro.Helpers.fst.checked Strategies.VarIntro.Defs.fst.checked Strategies.Semantics.Armada.fsti.checked Strategies.Semantics.fst.checked Strategies.PCRelation.fst.checked Strategies.Lift.Generic.fsti.checked Strategies.Invariant.fsti.checked Strategies.GlobalVars.VarIntro.fsti.checked Strategies.GlobalVars.VarHiding.fsti.checked Strategies.GlobalVars.Util.fst.checked Strategies.GlobalVars.Unaddressed.fst.checked Strategies.GlobalVars.Types.fst.checked Strategies.GlobalVars.Statement.fsti.checked Strategies.GlobalVars.Init.fst.checked Strategies.GlobalVars.fst.checked Strategies.Atomic.fst.checked Strategies.ArmadaStatement.ThreadState.fst.checked Strategies.ArmadaStatement.Status.fsti.checked Strategies.ArmadaStatement.Propagate.fst.checked Strategies.ArmadaInvariant.UnstartedThreads.fsti.checked Strategies.ArmadaInvariant.RootsMatch.fst.checked Strategies.ArmadaInvariant.PositionsValid.fsti.checked Spec.Ubool.fst.checked Spec.Map.fst.checked Spec.List.fst.checked Spec.Behavior.fst.checked prims.fst.checked FStar.WellFoundedRelation.fsti.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.Type.fst.checked Armada.Transition.fst.checked Armada.Threads.fst.checked Armada.Thread.fst.checked Armada.Step.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Memory.fst.checked Armada.Init.fst.checked Armada.Computation.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
Strategies.VarIntro.Propagate.fst

    vr: Strategies.VarIntro.Defs.var_intro_relation_t ->
    actor: Armada.Base.tid_t ->
    nd: Armada.Type.nondeterminism_t ->
    ls: Armada.State.t ->
    hs: Armada.State.t ->
    receiver_tid: Armada.Base.tid_t ->
    step: Armada.Step.t
  -> FStar.Pervasives.Lemma
      (requires
        Strategies.VarIntro.Invariant.var_intro_lh_relation vr () ls hs /\
        NotStopped? (Mkt?.stop_reason hs) /\
        ThreadStatusRunning? (Mkt?.status (Mkt?.threads hs actor)) /\
        step == Armada.Step.Mkt nd Strategies.VarIntro.Propagate.propagate_action /\
        Spec.List.list_len nd = 1 /\
        Armada.Type.object_value_to_td (Cons?.hd nd) ==
        Armada.Type.ObjectTDAbstract Armada.Base.tid_t /\
        receiver_tid == ObjectValueAbstract?.value (Cons?.hd nd) /\ receiver_tid <> actor /\
        ComputationProduces? (Armada.Statement.propagate_write_message_statement_computation actor
              nd
              ls) /\
        (let lthread = Mkt?.threads ls actor in
          let lwrite_buffer = Mkt?.write_buffer lthread in
          let lposition =
            Mkt?.position_in_other_write_buffers (Mkt?.threads ls receiver_tid) actor
          in
          let lwrite_message = FStar.Sequence.Base.index lwrite_buffer lposition in
          let lunread_write_buffer =
            Strategies.GlobalVars.unread_write_buffer (Mkt?.threads ls) actor receiver_tid
          in
          ThreadStatusRunning? (Mkt?.status lthread) /\
          Prims.op_Negation (Strategies.GlobalVars.global_variables_unaddressed_in_write_message (Mkvar_intro_relation_t?.vs
                    vr)
                lwrite_message)))
      (ensures
        ((let Armada.Computation.ComputationProduces #_ ls' =
              Armada.Statement.propagate_write_message_statement_computation actor nd ls
            in
            Strategies.VarIntro.Invariant.var_intro_lh_relation vr () ls' hs)
          <:
          Type0))
Strategies.VarIntro.Defs.var_intro_relation_t Armada.Base.tid_t Armada.Type.nondeterminism_t Armada.State.t Armada.Step.t Prims.op_BarBar Prims.op_disEquality Prims.int Spec.List.list_len Armada.Type.object_value_t Spec.Ubool.neqb Armada.Type.object_td_t Armada.Type.object_value_to_td Prims.__proj__Cons__item__hd Armada.Type.ObjectTDAbstract FStar.Pervasives.false_elim Prims.unit Prims.bool Prims.op_Equality Prims.op_GreaterThanOrEqual FStar.Sequence.Base.length Armada.Thread.write_message_t Armada.Thread.__proj__Mkt__item__write_buffer Armada.Memory.propagate_write_message Armada.State.__proj__Mkt__item__mem Prims._assert Strategies.VarIntro.Invariant.var_intro_lh_relation Strategies.ArmadaInvariant.RootsMatch.roots_match Strategies.GlobalVars.global_variables_unaddressed_in_memory Strategies.VarIntro.Defs.__proj__Mkvar_intro_relation_t__item__vs Strategies.ArmadaInvariant.UnstartedThreads.unstarted_threads_have_empty_write_buffers Strategies.GlobalVars.states_match_except_global_variables 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 Armada.Memory.t Strategies.GlobalVars.Unaddressed.propagate_write_message_maintains_gvars_unaddressed Strategies.GlobalVars.VarHiding.propagate_write_message_statement_computation_s1_only_maintains_states_match Strategies.GlobalVars.positions_in_write_buffers_match_except_global_variables Armada.State.__proj__Mkt__item__threads Prims.l_True Prims.squash Prims.Nil FStar.Pervasives.pattern FStar.Classical.Sugar.forall_intro Prims.l_Forall Prims.l_imp Prims.b2t Strategies.ArmadaInvariant.PositionsValid.sender_receiver_trigger Strategies.GlobalVars.write_buffers_match_except_global_variables Strategies.GlobalVars.unread_write_buffer FStar.Classical.Sugar.implies_intro Util.Seq.seq_to_list_drop_equals_tail Prims.eq2 FStar.Sequence.Base.seq FStar.Sequence.Base.drop Strategies.ArmadaInvariant.PositionsValid.position_valid Strategies.ArmadaInvariant.PositionsValid.positions_valid_in_threads Spec.Map.t Armada.Thread.t Spec.Map.upd Armada.Thread.Mkt Armada.Thread.__proj__Mkt__item__status Armada.Thread.__proj__Mkt__item__pc Armada.Thread.__proj__Mkt__item__top Armada.Thread.__proj__Mkt__item__stack Prims.nat Armada.Thread.__proj__Mkt__item__position_in_other_write_buffers Prims.op_Addition FStar.Sequence.Base.index Armada.Type.__proj__ObjectValueAbstract__item__value Strategies.PCRelation.pc_relation_t Strategies.VarIntro.Helpers.var_intro_pc_relation Strategies.VarIntro.Defs.__proj__Mkvar_intro_relation_t__item__hpc_to_lpc Strategies.VarIntro.Defs.__proj__Mkvar_intro_relation_t__item__return_hpcs Strategies.VarIntro.Defs.__proj__Mkvar_intro_relation_t__item__return_pcs_unique_proof Prims.l_and Armada.State.uu___is_NotStopped Armada.Thread.uu___is_ThreadStatusRunning Armada.Step.Mkt Strategies.VarIntro.Propagate.propagate_action Armada.Type.__proj__ObjectValueAbstract__item__ty Armada.Computation.uu___is_ComputationProduces Armada.Statement.propagate_write_message_statement_computation Prims.op_Negation Strategies.GlobalVars.global_variables_unaddressed_in_write_message
let get_propagate_lifter_case_skip_helper
      (vr: var_intro_relation_t)
      (actor: tid_t)
      (nd: nondeterminism_t)
      (ls hs: Armada.State.t)
      (receiver_tid: tid_t)
      (step: Armada.Step.t)
    : Lemma
      (requires
        var_intro_lh_relation vr () ls hs /\ NotStopped? hs.stop_reason /\
        ThreadStatusRunning? (hs.threads actor).status /\
        step == { nd = nd; action = propagate_action } /\ list_len nd = 1 /\
        object_value_to_td (Cons?.hd nd) == ObjectTDAbstract tid_t /\
        receiver_tid == ObjectValueAbstract?.value (Cons?.hd nd) /\ receiver_tid <> actor /\
        ComputationProduces? (propagate_write_message_statement_computation actor nd ls) /\
        (let lthread = ls.threads actor in
          let lwrite_buffer = lthread.write_buffer in
          let lposition = (ls.threads receiver_tid).position_in_other_write_buffers actor in
          let lwrite_message = index lwrite_buffer lposition in
          let lunread_write_buffer = unread_write_buffer ls.threads actor receiver_tid in
          ThreadStatusRunning? lthread.status /\
          not (global_variables_unaddressed_in_write_message vr.vs lwrite_message)))
      (ensures
        (match propagate_write_message_statement_computation actor nd ls with
          | ComputationProduces ls' -> var_intro_lh_relation vr () ls' hs)) =
  
let lunread_write_buffer = unread_write_buffer ls.threads actor receiver_tid in
let hunread_write_buffer = unread_write_buffer hs.threads actor receiver_tid in
let pc_relation = var_intro_pc_relation vr.hpc_to_lpc vr.return_hpcs vr.return_pcs_unique_proof in
if list_len nd <> 1 || neqb (object_value_to_td (Cons?.hd nd)) (ObjectTDAbstract tid_t)
then false_elim ()
else
  let receiver_tid:tid_t = ObjectValueAbstract?.value (Cons?.hd nd) in
  if receiver_tid = actor
  then false_elim ()
  else
    let propagator_thread = ls.threads actor in
    let receiver_thread = ls.threads receiver_tid in
    let which_message = receiver_thread.position_in_other_write_buffers actor in
    if which_message >= length propagator_thread.write_buffer
    then false_elim ()
    else
      (let write_message = index propagator_thread.write_buffer which_message in
        let position_in_other_write_buffers' =
          Spec.Map.upd receiver_thread.position_in_other_write_buffers actor (which_message + 1)
        in
        let receiver_thread' =
          {
            receiver_thread with
            position_in_other_write_buffers = position_in_other_write_buffers'
          }
        in
        let threads' = Spec.Map.upd ls.threads receiver_tid receiver_thread' in
        assert (positions_valid_in_threads threads');
        let lem ()
            : Lemma
            (positions_in_write_buffers_match_except_global_variables vr.vs threads' hs.threads) =
          (introduce forall sender_tid' receiver_tid' . sender_receiver_trigger sender_tid'
              receiver_tid' ==>
            write_buffers_match_except_global_variables vr.vs
              (unread_write_buffer threads' sender_tid' receiver_tid')
              (unread_write_buffer hs.threads sender_tid' receiver_tid')
            with introduce _ ==> _
            with _. (assert (position_valid ls.threads sender_tid' receiver_tid');
              assert (write_buffers_match_except_global_variables vr.vs
                    (unread_write_buffer ls.threads sender_tid' receiver_tid')
                    (unread_write_buffer hs.threads sender_tid' receiver_tid'));
              if receiver_tid <> receiver_tid'
              then ()
              else
                if actor <> sender_tid'
                then ()
                else
                  (assert (unread_write_buffer hs.threads sender_tid' receiver_tid' ==
                        hunread_write_buffer);
                    assert (unread_write_buffer threads' sender_tid' receiver_tid' ==
                        drop lunread_write_buffer 1);
                    seq_to_list_drop_equals_tail lunread_write_buffer)))
        in
        lem ();
        assert (positions_in_write_buffers_match_except_global_variables vr.vs threads' hs.threads);
        match propagate_write_message write_message receiver_tid ls.mem with
        | ComputationImpossible
        | ComputationUndefined ->
          let ls' = { ls with threads = threads' } in
          assert (states_match_except_global_variables vr.vs pc_relation ls' hs);
          assert (unstarted_threads_have_empty_write_buffers ls');
          assert (global_variables_unaddressed_in_memory vr.vs ls'.mem);
          assert (roots_match ls'.mem);
          assert (var_intro_lh_relation vr () ls' hs)
        | ComputationProduces mem' ->
          let ls' = { ls with mem = mem'; threads = threads' } in
          propagate_write_message_statement_computation_s1_only_maintains_states_match vr.vs
            pc_relation
            actor
            nd
            ls
            hs;
          assert (unstarted_threads_have_empty_write_buffers ls');
          propagate_write_message_maintains_gvars_unaddressed vr.vs
            write_message
            receiver_tid
            ls.mem;
          assert (global_variables_unaddressed_in_memory vr.vs ls'.mem);
          assert (roots_match ls'.mem);
          assert (var_intro_lh_relation vr () ls' hs))