Inductive bsm_instr n : Set :=
| bsm_pop : pos n -> nat -> nat -> bsm_instr n
| bsm_push : pos n -> bool -> bsm_instr n
.
Section Binary_Stack_Machine.
Variable (n : nat).
Notation POP := (bsm_pop n).
Notation PUSH := (bsm_push n).
Local Notation "e #> x" := (vec_pos e x).
Local Notation "e [ x := v ]" := (vec_change e x v) (no associativity, at level 50).
Local Reserved Notation "P // e ▷ v" (at level 50, no associativity).
Inductive eval : nat * list (bsm_instr n) -> (nat*vec (list bool) n) -> (nat*vec (list bool) n) -> Prop :=
| eval_bsm_out i P c v :
c < i \/ i + length P <= c ->
(i,P) // (c, v) ▷ (c, v)
| eval_bsm_push i P c v j b c' v' :
c >= i -> nth_error P (c - i) = Some (PUSH j b) ->
(i, P) // (c + 1, v[j := b :: v #> j]) ▷ (c', v') ->
(i,P) // (c, v) ▷ (c', v')
| eval_bsm_pop_true i P c v j c1 c2 c' v' l :
c >= i -> nth_error P (c - i) = Some (POP j c1 c2) ->
v #> j = true :: l -> (i, P) // (c +1, v [j := l]) ▷ (c',v') ->
(i,P) // (c, v) ▷ (c', v')
| eval_bsm_pop_false i P c v j c1 c2 c' v' l :
c >= i -> nth_error P (c - i) = Some (POP j c1 c2) ->
v #> j = false :: l -> (i, P) // (c1, v [j := l]) ▷ (c',v') ->
(i,P) // (c, v) ▷ (c', v')
| eval_bsm_pop_empty i P c v j c1 c2 c' v' :
c >= i -> nth_error P (c - i) = Some (POP j c1 c2) ->
v #> j = nil -> (i, P) // (c2, v) ▷ (c',v') ->
(i,P) // (c, v) ▷ (c', v')
where "P // e ▷ v" := (eval P e v).
End Binary_Stack_Machine.
Definition Halt_BSM :
{ n : nat & { i : nat & { P : list (bsm_instr n) & vec (list bool) n } } } -> Prop:=
fun '(existT _ n (existT _ i (existT _ P v))) => exists c' v', eval n (i,P) (i,v) (c', v').