val is_nonyielding_lpc:array_t bool
val is_nonyielding_lpc:array_t bool
let is_nonyielding_lpc: array_t bool = list_to_array
  [
    false; // A.main.1 is not nonyielding
    false; // A.main.2.1 is not nonyielding
    true;  // A.main.2.2 is nonyielding
    false; // A.main.3 is not nonyielding
    false; // A.main.3.R is not nonyielding
    false; // A.main.End is not nonyielding
    false; // A.subroutine.1 is not nonyielding
    false; // A.subroutine.End is not nonyielding
  ]
module MyVarIntroProof

open Armada.Action
open Armada.Base
open Armada.Computation
open Armada.Expression
open Armada.State
open Armada.Statement
open Armada.Thread
open Armada.Transition
open Armada.Type
open Spec.Behavior
open Strategies.ArmadaStatement.ThreadState
open Strategies.Atomic
open Strategies.GlobalVars.Types
open Strategies.Semantics
open Strategies.Semantics.Armada
open Strategies.PCIndices
open Strategies.VarIntro.Defs
open Strategies.VarIntro.Efficient
open Util.ImmutableArray

let vs: list var_id_t = // introduced variables in no particular order
  [
    "b";
    "d";
  ]

let tds: list object_td_t = // object type descriptors for the introduced variables in the order corresponding to `vs`
  [
    (ObjectTDAbstract int); // "b" is an abstract int
    (ObjectTDAbstract int); // "d" is an abstract int
  ]

let which_initializers_are_intros: list bool =
  [
    false; // The first initializer in B.global_initializers is a, which is not being introduced
    true;  // b *is* being introduced
    false; // c is not being introduced
    true;  // d is being introduced
    false; // e is not being introduced
  ]

let lpcs: array_t pc_t = list_to_array
  [
    "main.1";         // by index, known as A.PC #0
    "main.2.1";       // by index, known as A.PC #1
    "main.2.2";       // by index, known as A.PC #2
    "main.3";         // by index, known as A.PC #3
    "main.3.R";       // by index, known as A.PC #4
    "main.End";       // by index, known as A.PC #5
    "subroutine.1";   // by index, known as A.PC #6
    "subroutine.End"; // by index, known as A.PC #7
  ]

let hpcs: array_t pc_t = list_to_array
  [
    "main.1.1";       // by index, known as B.PC #0
    "main.1.2";       // by index, known as B.PC #1
    "main.1.3";       // by index, known as B.PC #2
    "main.2.1";       // by index, known as B.PC #3
    "main.2.2";       // by index, known as B.PC #4
    "main.2.3";       // by index, known as B.PC #5
    "main.3";         // by index, known as B.PC #6
    "main.3.R";       // by index, known as B.PC #7
    "main.4.1";       // by index, known as B.PC #8
    "main.4.2";       // by index, known as B.PC #9
    "main.End";       // by index, known as B.PC #10
    "subroutine.1";   // by index, known as B.PC #11
    "subroutine.2";   // by index, known as B.PC #12
    "subroutine.3";   // by index, known as B.PC #13
    "subroutine.End"; // by index, known as B.PC #14
  ]

let hpc_to_lpc: array_t nat = list_to_array
  [
    0; // B.main.1.1 (which is B.PC #0) maps to A.main.1 (which is A.PC #0)
    0; // B.main.1.2 (which is B.PC #1) maps to A.main.1 (which is A.PC #0)
    1; // B.main.1.3 (which is B.PC #2) maps to A.main.2.1 (which is A.PC #1)
    1; // B.main.2.1 (which is B.PC #3) maps to A.main.2.1 (which is A.PC #1)
    2; // B.main.2.2 (which is B.PC #4) maps to A.main.2.2 (which is A.PC #2)
    2; // B.main.2.3 (which is B.PC #5) maps to A.main.2.2 (which is A.PC #2)
    3; // B.main.3 (which is B.PC #6) maps to A.main.3 (which is A.PC #3)
    4; // B.main.3.R (which is B.PC #7) maps to A.main.3.R (which is A.PC #4)
    5; // B.main.4.1 (which is B.PC #8) maps to A.main.End (which is A.PC #5)
    5; // B.main.4.2 (which is B.PC #9) maps to A.main.End (which is A.PC #5)
    5; // B.main.End (which is B.PC #10) maps to A.main.End (which is A.PC #5)
    6; // B.subroutine.1 (which is B.PC #11) maps to A.subroutine.1 (which is A.PC #6)
    7; // B.subroutine.2 (which is B.PC #12) maps to A.subroutine.End (which is A.PC #7)
    7; // B.subroutine.3 (which is B.PC #13) maps to A.subroutine.End (which is A.PC #7)
    7; // B.subroutine.End (which is B.PC #14) maps to A.subroutine.End (which is A.PC #7)
  ]

let lpc_to_hpcs: array_t (list nat) = list_to_array
  [
    [0; 1];     // A.main.1 (which is A.PC #0) maps to B.PCs #0, #1
    [2; 3];     // A.main.2.1 (which is A.PC #1) maps to B.PCs #2, #3
    [4; 5];     // A.main.2.2 (which is A.PC #2) maps to B.PCs #4, #5
    [6];        // A.main.3 (which is A.PC #3) maps to B.PC #6
    [7];        // A.main.3.R (which is A.PC #4) maps to B.PC #7
    [8; 9; 10]; // A.main.End (which is A.PC #5) maps to B.PCs #8, #9, #10
    [11];       // A.subroutine.1 (which is A.PC #6) maps to B.PC #11
    [12; 13; 14];  // A.subroutine.End (which is A.PC #7) maps to B.PCs #12, #13, #14
  ]

let is_return_hpc: array_t bool = list_to_array
  [
    false; // B.PC #0 isn't a return PC
    false; // B.PC #1 isn't a return PC
    false; // ...
    false;
    false;
    false;
    false;
    true;  // only B.main.3.R (which is B.PC #7) is a return PC (one that's pushed on the stack to be returned to)
    false;
    false;
    false;
    false;
    false;
    false;
    false;
  ]
/
Util.ImmutableArray.fsti.checked Strategies.VarIntro.Efficient.fsti.checked Strategies.VarIntro.Defs.fst.checked Strategies.Semantics.Armada.fsti.checked Strategies.Semantics.fst.checked Strategies.PCIndices.fst.checked Strategies.GlobalVars.Types.fst.checked Strategies.Atomic.fst.checked Strategies.ArmadaStatement.ThreadState.fst.checked Spec.Behavior.fst.checked prims.fst.checked MyBProg.fst.checked MyAtomicBProg.fst.checked MyAtomicBInvariant.fst.checked MyAtomicAProg.fst.checked MyAProg.fst.checked FStar.Tactics.V2.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Pervasives.fsti.checked Armada.Type.fst.checked Armada.Transition.fst.checked Armada.Thread.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Expression.fst.checked Armada.Computation.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
MyVarIntroProof.fst
Util.ImmutableArray.array_t Prims.bool
Util.ImmutableArray.list_to_array Prims.bool Prims.Cons Prims.Nil
let is_nonyielding_lpc:array_t bool =
  
list_to_array [false; false; true; false; false; false; false; false]