val get_propagate_lifter_case_match
      (vr: var_intro_relation_t)
      (actor: tid_t)
      (ls hs: Armada.State.t)
      (nd: nondeterminism_t)
      (receiver_tid: tid_t)
      (step: Armada.Step.t)
      (lifter: step_lifter_t (list Armada.Step.t) unit)
    : Lemma
      (requires
        (var_intro_lh_relation vr () ls hs /\
          ComputationProduces? (propagate_write_message_statement_computation actor nd ls) /\
          NotStopped? ls.stop_reason /\ list_len nd = 1 /\
          object_value_to_td (Cons?.hd nd) == ObjectTDAbstract tid_t /\
          receiver_tid == ObjectValueAbstract?.value (Cons?.hd nd) /\
          (let lthread = ls.threads actor in
            let hthread = hs.threads actor in
            let lwrite_buffer = lthread.write_buffer in
            let hwrite_buffer = hthread.write_buffer in
            let lposition = (ls.threads receiver_tid).position_in_other_write_buffers actor in
            let hposition = (hs.threads receiver_tid).position_in_other_write_buffers actor in
            ThreadStatusRunning? lthread.status /\ length hwrite_buffer > hposition /\
            (let lwrite_message = index lwrite_buffer lposition in
              let hwrite_message = index hwrite_buffer hposition in
              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 hstep = [step] in
              step == { nd = nd; action = propagate_action } /\
              program_contains_action_of_step_generic (make_atomic_semantics armada_semantics)
                vr.hatomic_prog
                [step] /\ lifter == StepLifterLift hstep () /\
              global_variables_unaddressed_in_write_message vr.vs lwrite_message /\
              global_variables_unaddressed_in_write_message vr.vs hwrite_message /\
              write_messages_match lwrite_message hwrite_message))))
      (ensures
        step_lifter_works (make_atomic_semantics armada_semantics)
          (make_atomic_semantics armada_semantics) vr.latomic_prog vr.hatomic_prog unit
          (var_intro_lh_relation vr) (nat * nat)
          (lex_nondep_wfr (default_wfr nat) (default_wfr nat)) (var_intro_progress_measure vr) actor
          true true [step] ls hs lifter)
val get_propagate_lifter_case_match
      (vr: var_intro_relation_t)
      (actor: tid_t)
      (ls hs: Armada.State.t)
      (nd: nondeterminism_t)
      (receiver_tid: tid_t)
      (step: Armada.Step.t)
      (lifter: step_lifter_t (list Armada.Step.t) unit)
    : Lemma
      (requires
        (var_intro_lh_relation vr () ls hs /\
          ComputationProduces? (propagate_write_message_statement_computation actor nd ls) /\
          NotStopped? ls.stop_reason /\ list_len nd = 1 /\
          object_value_to_td (Cons?.hd nd) == ObjectTDAbstract tid_t /\
          receiver_tid == ObjectValueAbstract?.value (Cons?.hd nd) /\
          (let lthread = ls.threads actor in
            let hthread = hs.threads actor in
            let lwrite_buffer = lthread.write_buffer in
            let hwrite_buffer = hthread.write_buffer in
            let lposition = (ls.threads receiver_tid).position_in_other_write_buffers actor in
            let hposition = (hs.threads receiver_tid).position_in_other_write_buffers actor in
            ThreadStatusRunning? lthread.status /\ length hwrite_buffer > hposition /\
            (let lwrite_message = index lwrite_buffer lposition in
              let hwrite_message = index hwrite_buffer hposition in
              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 hstep = [step] in
              step == { nd = nd; action = propagate_action } /\
              program_contains_action_of_step_generic (make_atomic_semantics armada_semantics)
                vr.hatomic_prog
                [step] /\ lifter == StepLifterLift hstep () /\
              global_variables_unaddressed_in_write_message vr.vs lwrite_message /\
              global_variables_unaddressed_in_write_message vr.vs hwrite_message /\
              write_messages_match lwrite_message hwrite_message))))
      (ensures
        step_lifter_works (make_atomic_semantics armada_semantics)
          (make_atomic_semantics armada_semantics) vr.latomic_prog vr.hatomic_prog unit
          (var_intro_lh_relation vr) (nat * nat)
          (lex_nondep_wfr (default_wfr nat) (default_wfr nat)) (var_intro_progress_measure vr) actor
          true true [step] ls hs lifter)
let get_propagate_lifter_case_match
  (vr: var_intro_relation_t)
  (actor: tid_t)
  (ls: Armada.State.t)
  (hs: Armada.State.t)
  (nd: nondeterminism_t)
  (receiver_tid: tid_t)
  (step: Armada.Step.t)
  (lifter: step_lifter_t (list Armada.Step.t) unit)
  : Lemma
    (requires (  var_intro_lh_relation vr () ls hs
               /\ ComputationProduces? (propagate_write_message_statement_computation actor nd ls)
               /\ NotStopped? ls.stop_reason
               /\ list_len nd = 1
               /\ object_value_to_td (Cons?.hd nd) == ObjectTDAbstract tid_t
               /\ receiver_tid == ObjectValueAbstract?.value (Cons?.hd nd)
               /\ (let lthread = ls.threads actor in
                  let hthread = hs.threads actor in
                  let lwrite_buffer = lthread.write_buffer in
                  let hwrite_buffer = hthread.write_buffer in
                  let lposition = (ls.threads receiver_tid).position_in_other_write_buffers actor in
                  let hposition = (hs.threads receiver_tid).position_in_other_write_buffers actor in
                    ThreadStatusRunning? lthread.status
                  /\ length hwrite_buffer > hposition
                  /\ (let lwrite_message = index lwrite_buffer lposition in
                     let hwrite_message = index hwrite_buffer hposition in
                     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 hstep = [step] in
                       step == { nd = nd; action = propagate_action }
                     /\ program_contains_action_of_step_generic (make_atomic_semantics armada_semantics)
                         vr.hatomic_prog [step]
                     /\ lifter == StepLifterLift hstep ()
                     /\ global_variables_unaddressed_in_write_message vr.vs lwrite_message
                     /\ global_variables_unaddressed_in_write_message vr.vs hwrite_message
                     /\ write_messages_match lwrite_message hwrite_message))))
    (ensures  step_lifter_works
                (make_atomic_semantics armada_semantics)
                (make_atomic_semantics armada_semantics)
                vr.latomic_prog vr.hatomic_prog unit (var_intro_lh_relation vr)
                (nat * nat) (lex_nondep_wfr (default_wfr nat) (default_wfr nat))
                (var_intro_progress_measure vr) actor true true [step] ls hs lifter) =
  let pc_relation = var_intro_pc_relation vr.hpc_to_lpc vr.return_hpcs vr.return_pcs_unique_proof in
  let lthread = ls.threads actor in
  let hthread = hs.threads actor in
  let lwrite_buffer = lthread.write_buffer in
  let hwrite_buffer = hthread.write_buffer in
  let lposition = (ls.threads receiver_tid).position_in_other_write_buffers actor in
  let hposition = (hs.threads receiver_tid).position_in_other_write_buffers actor in
  let lwrite_message = index lwrite_buffer lposition in
  let hwrite_message = index hwrite_buffer hposition in
  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
  assert (map_ghost armada_step_to_action [step] == propagate_action_list);
  propagate_write_message_statement_computation_maintains_states_match vr.vs pc_relation actor nd ls hs;
  match propagate_write_message_statement_computation actor nd ls,
        propagate_write_message_statement_computation actor nd hs with
  | ComputationProduces ls', ComputationProduces hs' ->
      assert (states_match_except_global_variables vr.vs pc_relation ls' hs');
      assert (global_variables_unaddressed_in_memory vr.vs ls'.mem);
      assert (global_variables_unaddressed_in_memory vr.vs hs'.mem);
      assert (roots_match ls'.mem);
      assert (roots_match hs'.mem);
      propagate_maintains_all_running_threads_have_pcs_in_list actor nd vr.hpcs hs;
      propagate_maintains_all_gvars_have_types vr.vs vr.tds actor nd hs;
      step_computation_is_propagate_computation actor nd ls step;
      step_computation_is_propagate_computation actor nd hs step;
      introduce NotStopped? hs'.stop_reason ==> vr.inv hs'
      with _. (
        vr.inv_is_substep_invariant_proof ();
        assert (vr.inv hs);
        assert (contains_ubool step.action propagate_action_list);
        assert (contains_ubool propagate_action_list vr.hatomic_prog.actions);
        assert (Some hs' == step_computation actor true true step hs)
      );
      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"

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

#pop-options

let get_propagate_lifter_case_skip
  (vr: var_intro_relation_t)
  (actor: tid_t)
  (ls: Armada.State.t)
  (hs: Armada.State.t)
  (nd: nondeterminism_t)
  (receiver_tid: tid_t)
  (step: Armada.Step.t)
  (lifter: step_lifter_t (list Armada.Step.t) unit)
  : Lemma
    (requires (  var_intro_lh_relation vr () ls hs
               /\ ComputationProduces? (propagate_write_message_statement_computation actor nd ls)
               /\ NotStopped? ls.stop_reason
               /\ list_len nd = 1
               /\ object_value_to_td (Cons?.hd nd) == ObjectTDAbstract tid_t
               /\ receiver_tid == ObjectValueAbstract?.value (Cons?.hd nd)
               /\ lifter == StepLifterSkip ()
               /\ step == { nd = nd; action = propagate_action }
               /\ (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
                    lposition < length lwrite_buffer
                  /\ (let lwrite_message = index lwrite_buffer lposition in
                       ThreadStatusRunning? lthread.status
                     /\ not (global_variables_unaddressed_in_write_message vr.vs lwrite_message)))))
    (ensures  step_lifter_works
                (make_atomic_semantics armada_semantics)
                (make_atomic_semantics armada_semantics)
                vr.latomic_prog vr.hatomic_prog unit (var_intro_lh_relation vr)
                (nat * nat) (lex_nondep_wfr (default_wfr nat) (default_wfr nat))
                (var_intro_progress_measure vr) actor true true [step] ls hs lifter) =
  let pc_relation = var_intro_pc_relation vr.hpc_to_lpc vr.return_hpcs vr.return_pcs_unique_proof in
  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
  assert_norm (map_ghost armada_step_to_action [step] == propagate_action_list);
  get_propagate_lifter_case_skip_helper vr actor nd ls hs receiver_tid step;
  step_computation_is_propagate_computation actor nd ls step

#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 ->
    ls: Armada.State.t ->
    hs: Armada.State.t ->
    nd: Armada.Type.nondeterminism_t ->
    receiver_tid: Armada.Base.tid_t ->
    step: Armada.Step.t ->
    lifter: Strategies.Lift.Generic.step_lifter_t (Prims.list Armada.Step.t) Prims.unit
  -> FStar.Pervasives.Lemma
      (requires
        Strategies.VarIntro.Invariant.var_intro_lh_relation vr () ls hs /\
        ComputationProduces? (Armada.Statement.propagate_write_message_statement_computation actor
              nd
              ls) /\ NotStopped? (Mkt?.stop_reason ls) /\ 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) /\
        (let lthread = Mkt?.threads ls actor in
          let hthread = Mkt?.threads hs actor in
          let lwrite_buffer = Mkt?.write_buffer lthread in
          let hwrite_buffer = Mkt?.write_buffer hthread in
          let lposition =
            Mkt?.position_in_other_write_buffers (Mkt?.threads ls receiver_tid) actor
          in
          let hposition =
            Mkt?.position_in_other_write_buffers (Mkt?.threads hs receiver_tid) actor
          in
          ThreadStatusRunning? (Mkt?.status lthread) /\
          FStar.Sequence.Base.length hwrite_buffer > hposition /\
          (let lwrite_message = FStar.Sequence.Base.index lwrite_buffer lposition in
            let hwrite_message = FStar.Sequence.Base.index hwrite_buffer hposition in
            let lunread_write_buffer =
              Strategies.GlobalVars.unread_write_buffer (Mkt?.threads ls) actor receiver_tid
            in
            let hunread_write_buffer =
              Strategies.GlobalVars.unread_write_buffer (Mkt?.threads hs) actor receiver_tid
            in
            let hstep = [step] in
            step == Armada.Step.Mkt nd Strategies.VarIntro.Propagate.propagate_action /\
            Strategies.Semantics.program_contains_action_of_step_generic (Strategies.Atomic.make_atomic_semantics
                  Strategies.Semantics.Armada.armada_semantics)
              (Mkvar_intro_relation_t?.hatomic_prog vr)
              [step] /\ lifter == Strategies.Lift.Generic.StepLifterLift hstep () /\
            Strategies.GlobalVars.global_variables_unaddressed_in_write_message (Mkvar_intro_relation_t?.vs
                  vr)
              lwrite_message /\
            Strategies.GlobalVars.global_variables_unaddressed_in_write_message (Mkvar_intro_relation_t?.vs
                  vr)
              hwrite_message /\
            Strategies.PCRelation.write_messages_match lwrite_message hwrite_message)))
      (ensures
        Strategies.Lift.Generic.step_lifter_works (Strategies.Atomic.make_atomic_semantics Strategies.Semantics.Armada.armada_semantics
            ) (Strategies.Atomic.make_atomic_semantics Strategies.Semantics.Armada.armada_semantics)
          (Mkvar_intro_relation_t?.latomic_prog vr) (Mkvar_intro_relation_t?.hatomic_prog vr)
          Prims.unit (Strategies.VarIntro.Invariant.var_intro_lh_relation vr)
          (Prims.nat * Prims.nat)
          (FStar.WellFoundedRelation.lex_nondep_wfr (FStar.WellFoundedRelation.default_wfr Prims.nat
              )
              (FStar.WellFoundedRelation.default_wfr Prims.nat))
          (Strategies.VarIntro.Invariant.var_intro_progress_measure vr) actor true true [step] ls hs
          lifter)
Strategies.VarIntro.Defs.var_intro_relation_t Armada.Base.tid_t Armada.State.t Armada.Type.nondeterminism_t Armada.Step.t Strategies.Lift.Generic.step_lifter_t Prims.list Prims.unit FStar.Pervasives.Native.Mktuple2 Armada.Computation.conditional_computation_t Armada.Statement.propagate_write_message_statement_computation Prims._assert Strategies.VarIntro.Invariant.var_intro_lh_relation FStar.Classical.Sugar.implies_intro Prims.b2t Armada.State.uu___is_NotStopped Armada.State.__proj__Mkt__item__stop_reason Prims.squash Strategies.VarIntro.Defs.__proj__Mkvar_intro_relation_t__item__inv Prims.eq2 FStar.Pervasives.Native.option FStar.Pervasives.Native.Some Armada.Transition.step_computation Spec.List.contains_ubool Strategies.Semantics.__proj__Mksemantics_t__item__action_t Strategies.Atomic.make_atomic_semantics Strategies.Semantics.Armada.armada_semantics Strategies.ArmadaStatement.Propagate.propagate_action_list Strategies.Semantics.__proj__Mkprogram_t__item__actions Strategies.VarIntro.Defs.__proj__Mkvar_intro_relation_t__item__hatomic_prog Armada.Action.t Armada.Step.__proj__Mkt__item__action Strategies.VarIntro.Defs.__proj__Mkvar_intro_relation_t__item__inv_is_substep_invariant_proof Strategies.ArmadaStatement.Propagate.step_computation_is_propagate_computation Strategies.VarIntro.Helpers.propagate_maintains_all_gvars_have_types Strategies.VarIntro.Defs.__proj__Mkvar_intro_relation_t__item__vs Strategies.VarIntro.Defs.__proj__Mkvar_intro_relation_t__item__tds Strategies.VarIntro.Helpers.propagate_maintains_all_running_threads_have_pcs_in_list Strategies.VarIntro.Defs.__proj__Mkvar_intro_relation_t__item__hpcs Strategies.ArmadaInvariant.RootsMatch.roots_match Armada.State.__proj__Mkt__item__mem Strategies.GlobalVars.global_variables_unaddressed_in_memory Strategies.GlobalVars.states_match_except_global_variables Strategies.GlobalVars.VarIntro.propagate_write_message_statement_computation_maintains_states_match Util.List.map_ghost Strategies.Semantics.Armada.armada_step_to_action Prims.Cons Prims.Nil FStar.Sequence.Base.seq Armada.Thread.write_message_t Strategies.GlobalVars.unread_write_buffer Armada.State.__proj__Mkt__item__threads FStar.Sequence.Base.index Prims.nat Armada.Thread.__proj__Mkt__item__position_in_other_write_buffers Armada.Thread.__proj__Mkt__item__write_buffer Armada.Thread.t 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.Computation.uu___is_ComputationProduces Prims.op_Equality Prims.int Spec.List.list_len Armada.Type.object_value_t Armada.Type.object_td_t Armada.Type.object_value_to_td Prims.__proj__Cons__item__hd Armada.Type.ObjectTDAbstract Armada.Type.__proj__ObjectValueAbstract__item__ty Armada.Type.__proj__ObjectValueAbstract__item__value Armada.Thread.uu___is_ThreadStatusRunning Armada.Thread.__proj__Mkt__item__status Prims.op_GreaterThan FStar.Sequence.Base.length Armada.Step.Mkt Strategies.VarIntro.Propagate.propagate_action Strategies.Semantics.program_contains_action_of_step_generic Strategies.Semantics.__proj__Mksemantics_t__item__step_t Strategies.Lift.Generic.StepLifterLift Strategies.GlobalVars.global_variables_unaddressed_in_write_message Strategies.PCRelation.write_messages_match Strategies.Lift.Generic.step_lifter_works Strategies.VarIntro.Defs.__proj__Mkvar_intro_relation_t__item__latomic_prog FStar.Pervasives.Native.tuple2 FStar.WellFoundedRelation.lex_nondep_wfr FStar.WellFoundedRelation.default_wfr Strategies.VarIntro.Invariant.var_intro_progress_measure FStar.Pervasives.pattern
let get_propagate_lifter_case_match
      (vr: var_intro_relation_t)
      (actor: tid_t)
      (ls hs: Armada.State.t)
      (nd: nondeterminism_t)
      (receiver_tid: tid_t)
      (step: Armada.Step.t)
      (lifter: step_lifter_t (list Armada.Step.t) unit)
    : Lemma
      (requires
        (var_intro_lh_relation vr () ls hs /\
          ComputationProduces? (propagate_write_message_statement_computation actor nd ls) /\
          NotStopped? ls.stop_reason /\ list_len nd = 1 /\
          object_value_to_td (Cons?.hd nd) == ObjectTDAbstract tid_t /\
          receiver_tid == ObjectValueAbstract?.value (Cons?.hd nd) /\
          (let lthread = ls.threads actor in
            let hthread = hs.threads actor in
            let lwrite_buffer = lthread.write_buffer in
            let hwrite_buffer = hthread.write_buffer in
            let lposition = (ls.threads receiver_tid).position_in_other_write_buffers actor in
            let hposition = (hs.threads receiver_tid).position_in_other_write_buffers actor in
            ThreadStatusRunning? lthread.status /\ length hwrite_buffer > hposition /\
            (let lwrite_message = index lwrite_buffer lposition in
              let hwrite_message = index hwrite_buffer hposition in
              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 hstep = [step] in
              step == { nd = nd; action = propagate_action } /\
              program_contains_action_of_step_generic (make_atomic_semantics armada_semantics)
                vr.hatomic_prog
                [step] /\ lifter == StepLifterLift hstep () /\
              global_variables_unaddressed_in_write_message vr.vs lwrite_message /\
              global_variables_unaddressed_in_write_message vr.vs hwrite_message /\
              write_messages_match lwrite_message hwrite_message))))
      (ensures
        step_lifter_works (make_atomic_semantics armada_semantics)
          (make_atomic_semantics armada_semantics) vr.latomic_prog vr.hatomic_prog unit
          (var_intro_lh_relation vr) (nat * nat)
          (lex_nondep_wfr (default_wfr nat) (default_wfr nat)) (var_intro_progress_measure vr) actor
          true true [step] ls hs lifter) =
  
let pc_relation = var_intro_pc_relation vr.hpc_to_lpc vr.return_hpcs vr.return_pcs_unique_proof in
let lthread = ls.threads actor in
let hthread = hs.threads actor in
let lwrite_buffer = lthread.write_buffer in
let hwrite_buffer = hthread.write_buffer in
let lposition = (ls.threads receiver_tid).position_in_other_write_buffers actor in
let hposition = (hs.threads receiver_tid).position_in_other_write_buffers actor in
let lwrite_message = index lwrite_buffer lposition in
let hwrite_message = index hwrite_buffer hposition in
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
assert (map_ghost armada_step_to_action [step] == propagate_action_list);
propagate_write_message_statement_computation_maintains_states_match vr.vs
  pc_relation
  actor
  nd
  ls
  hs;
match
  propagate_write_message_statement_computation actor nd ls,
  propagate_write_message_statement_computation actor nd hs
with
| ComputationProduces ls', ComputationProduces hs' ->
  assert (states_match_except_global_variables vr.vs pc_relation ls' hs');
  assert (global_variables_unaddressed_in_memory vr.vs ls'.mem);
  assert (global_variables_unaddressed_in_memory vr.vs hs'.mem);
  assert (roots_match ls'.mem);
  assert (roots_match hs'.mem);
  propagate_maintains_all_running_threads_have_pcs_in_list actor nd vr.hpcs hs;
  propagate_maintains_all_gvars_have_types vr.vs vr.tds actor nd hs;
  step_computation_is_propagate_computation actor nd ls step;
  step_computation_is_propagate_computation actor nd hs step;
  introduce NotStopped? hs'.stop_reason ==> vr.inv hs'
  with _. (vr.inv_is_substep_invariant_proof ();
    assert (vr.inv hs);
    assert (contains_ubool step.action propagate_action_list);
    assert (contains_ubool propagate_action_list vr.hatomic_prog.actions);
    assert (Some hs' == step_computation actor true true step hs));
  assert (var_intro_lh_relation vr () ls' hs')