val assume_predicate_statement_computation
      (actor: tid_t)
      (nd: nondeterminism_t)
      (start_pc: pc_t)
      (pred: (Armada.State.t -> GTot bool))
      (s: Armada.State.t)
    : GTot (conditional_computation_t Armada.State.t)
val assume_predicate_statement_computation
      (actor: tid_t)
      (nd: nondeterminism_t)
      (start_pc: pc_t)
      (pred: (Armada.State.t -> GTot bool))
      (s: Armada.State.t)
    : GTot (conditional_computation_t Armada.State.t)
let assume_predicate_statement_computation
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (pred: Armada.State.t -> GTot bool)
  (s: Armada.State.t)
  : GTot (conditional_computation_t Armada.State.t) =
  if   Cons? nd
     || not (pred s) then
    ComputationImpossible
  else
    return s
module Armada.Statement

open Armada.Base
open Armada.Computation
open Armada.Expression
open Armada.Init
open Armada.Memory
open Armada.Pointer
open Armada.State
open Armada.Thread
open Armada.Threads
open Armada.Type
open FStar.Sequence.Base
open Spec.List
open Spec.Map
open Spec.Ubool

noeq type t =
  | AssumeExpressionStatement: (exp: expression_t) -> t
  | AssumePredicateStatement: (pred: Armada.State.t -> GTot bool) -> t
  | AssertTrueStatement: (exp: expression_t) -> t
  | AssertFalseStatement: (exp: expression_t) -> t
  | ConditionalJumpStatement: (cond: expression_t) -> t // if or while
  | UnconditionalJumpStatement: t // skip, jump past else, jump back to loop head, break, continue, goto, if *, while *
  | UpdateStatement: (bypassing_write_buffer: bool) -> // whether ::= is used
                     (dst: expression_t) -> (src: expression_t) -> t
  | NondeterministicUpdateStatement: (bypassing_write_buffer: bool) -> // whether ::= is used
                                     (dst: expression_t) -> t
  | PropagateWriteMessageStatement: t
  | CompareAndSwapStatement: (target: expression_t) ->  // the location to compare to and possibly store into
                             (old_val: expression_t) -> // the value to compare the current value to
                             (new_val: expression_t) -> // the value to swap in if the equality comparison succeeds
                             (bypassing_write_buffer: bool) -> // whether ::= is used for assigning optional_result
                             (optional_result: option expression_t) -> t // where to write the boolean "did swap happen?"
  | AtomicExchangeStatement: (old_val: expression_t) -> // where the old value of target will be put
                             (target: expression_t) ->  // where the new value should be assigned to 
                             (new_val: expression_t) -> t // the new value
                             // e.g., x := atomic_exchange(y, 3) has old_val x, target y, and new_val 3,
                             // and means to atomically set x := y then y := 3
  | CreateThreadStatement: (method_id: method_id_t) ->
                           (initial_pc: pc_t) ->              // initial PC of created thread
                           (bypassing_write_buffer: bool) ->  // whether ::= is used for assigning the new thread ID
                           (optional_result: option expression_t) -> // where the resulting thread ID should be
                                                                    // written (optional)
                           (parameter_var_ids: list var_id_t) ->  // local variables to store parameters
                                                                 // (assumed strongly consistent)
                           (parameter_expressions: list expression_t) -> // expressions to be stored as parameters
                           (local_variable_initializers: list initializer_t) ->  t
  | MethodCallStatement: (method_id: method_id_t) ->
                         (return_pc: pc_t) ->
                         (parameter_var_ids: list var_id_t) -> // local variables to store parameters
                                                              // (assumed strongly consistent)
                         (parameter_expressions: list expression_t) -> // expressions to be stored as parameters
                         (local_variable_initializers: list initializer_t) ->
                            // If this is an external method, there should be one local variable initializer for
                            // each reads clause. The types of these initializers should match the types of those
                            // reads clauses, in order. So, for instance if it has "reads p[3], x" and the types of
                            // p[3] and x are t1 and t2, then the local variable initializers should be a list
                            // whose first element is an initializer with type t1 and whose second element is
                            // an initializer of type t2.
                         (stack_overflow: bool) -> t
  | ReturnStatement: (method_id: method_id_t) ->
                     (bypassing_write_buffer: bool) ->   // whether ::= is used for assigning output variables
                     (output_dsts: list expression_t) ->
                     (output_srcs: list expression_t) -> // output sources to be evaluated before popping the stack;
                                                        // generally, each of these will be an ExpressionLocalVariable
                                                        // corresponding to an output stack variable
                     t
  | TerminateThreadStatement: (method_id: method_id_t) -> t  // top-level method being returned from
  | TerminateProcessStatement: (method_id: method_id_t) -> t // main method ID being returned from
  | JoinStatement: (join_tid: expression_t) -> t // in concrete levels, this expression shouldn't read shared state
  | MallocSuccessfulStatement: (bypassing_write_buffer: bool) -> // whether ::= is used to write the resulting pointer
                               (result: expression_t) ->         // where the resulting pointer is written
                               (allocation_td: object_td_t) ->   // type being allocated
                               (count: expression_t) ->          // count must be a nat
                               t
  | MallocReturningNullStatement: (bypassing_write_buffer: bool) -> (result: expression_t) -> (count: expression_t) -> t
  | CallocSuccessfulStatement: (bypassing_write_buffer: bool) -> (result: expression_t) -> // result must be a pointer
                               (allocation_td: object_td_t) -> (count: expression_t) ->    // count must be a nat
                               t
  | CallocReturningNullStatement: (bypassing_write_buffer: bool) ->
                                  (result: expression_t) -> // result must be a pointer
                                  (count: expression_t) ->  // count must be a nat
                                  t
  | DeallocStatement: (ptr: expression_t) -> t
  | SomehowStatement: (undefined_unless_cond: expression_t) -> // undefined_unless conditions combined with &&
                      (bypassing_write_buffer: bool) ->        // whether updates to modifies clauses
                                                              //   bypass write buffers
                      (modifies_clauses: list expression_t) ->
                      (ensures_cond: expression_t) ->          // ensures conditions combined with &&
                      t
  | FenceStatement: t
  | ExternalMethodStartStatement: (await_cond: expression_t) ->            // awaits conditions combined with &&
                                  (undefined_unless_cond: expression_t) -> // undefined_unless conditions
                                                                          //   combined with &&
                                  (bypassing_write_buffer: bool) ->        // whether havocs of modifies clauses
                                                                          //   bypass write buffer
                                  (modifies_clauses: list expression_t) -> // modifies clauses to havoc
                                  (reads_clauses: list (var_id_t * expression_t)) -> // reads clauses to snapshot
                                  t
  | ExternalMethodMiddleStatement: (bypassing_write_buffer: bool) ->        // whether havocs of modifies clauses
                                                                           //   bypass write buffer
                                   (modifies_clauses: list expression_t) -> // modifies clauses to havoc
                                   (reads_clauses: list (var_id_t * expression_t)) -> // reads clauses to snapshot
                                   t
  | ExternalMethodEndStatement: (ensures_cond: expression_t) ->             // ensures clauses combined with &&
                                (logs_clauses: list expression_t) ->        // values to be appended to
                                                                           //   external-event trace
                                t

let assume_expression_statement_computation
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (exp: expression_t)
  (s: Armada.State.t)
  : GTot (conditional_computation_t Armada.State.t) =
  if   Cons? nd
     || neqb (expression_to_td exp) (ObjectTDAbstract bool) then
     ComputationImpossible
  else (
    let? value = rvalue_computation exp actor s in
    if ObjectValueAbstract?.value value <> true then
      ComputationImpossible
    else
      return s
  )
/
Spec.Ubool.fst.checked Spec.Map.fst.checked Spec.List.fst.checked prims.fst.checked FStar.Sequence.Base.fsti.checked FStar.Pervasives.fsti.checked Armada.Type.fst.checked Armada.Threads.fst.checked Armada.Thread.fst.checked Armada.State.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.Statement.fst

    actor: Armada.Base.tid_t ->
    nd: Armada.Type.nondeterminism_t ->
    start_pc: Armada.Base.pc_t ->
    pred: (_: Armada.State.t -> Prims.GTot Prims.bool) ->
    s: Armada.State.t
  -> Prims.GTot (Armada.Computation.conditional_computation_t Armada.State.t)
Armada.Base.tid_t Armada.Type.nondeterminism_t Armada.Base.pc_t Armada.State.t Prims.bool Prims.op_BarBar Prims.uu___is_Cons Armada.Type.object_value_t Prims.op_Negation Armada.Computation.ComputationImpossible Armada.Computation.return Armada.Computation.conditional_computation_t
let assume_predicate_statement_computation
      (actor: tid_t)
      (nd: nondeterminism_t)
      (start_pc: pc_t)
      (pred: (Armada.State.t -> GTot bool))
      (s: Armada.State.t)
    : GTot (conditional_computation_t Armada.State.t) =
  
if Cons? nd || not (pred s) then ComputationImpossible else return s