Commit c2252ec0 authored by Asma Tafat-Bouzid's avatar Asma Tafat-Bouzid

update preuve blocking semantic 5

parent 0e1516d0
......@@ -578,6 +578,4 @@ simpl in H.
inversion H1; subst; clear H1.
inversion H2; subst; clear H2; auto.
inversion H0.
Qed.
Qed.
\ No newline at end of file
......@@ -4,7 +4,6 @@ Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.MinMax.
Require set.Set.
(* Why3 assumption *)
Inductive list (a:Type) {a_WT:WhyType a} :=
......@@ -576,32 +575,109 @@ Definition total_valid_triple(p:fmla) (s:stmt) (q:fmla): Prop :=
exists pi':(list (ident* value)%type), exists n:Z, (many_steps sigma pi s
sigma' pi' Sskip n) /\ (eval_fmla sigma' pi' q).
Axiom set1 : forall (a:Type) {a_WT:WhyType a}, Type.
Parameter set1_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (set1 a).
Existing Instance set1_WhyType.
Parameter mem1: forall {a:Type} {a_WT:WhyType a}, a -> (set1 a) -> Prop.
(* Why3 assumption *)
Definition infix_eqeq {a:Type} {a_WT:WhyType a}(s1:(set1 a)) (s2:(set1
a)): Prop := forall (x:a), (mem1 x s1) <-> (mem1 x s2).
Axiom extensionality : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)), (infix_eqeq s1 s2) -> (s1 = s2).
(* Why3 assumption *)
Definition subset {a:Type} {a_WT:WhyType a}(s1:(set1 a)) (s2:(set1
a)): Prop := forall (x:a), (mem1 x s1) -> (mem1 x s2).
Axiom subset_trans : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)) (s3:(set1 a)), (subset s1 s2) -> ((subset s2 s3) ->
(subset s1 s3)).
Parameter empty: forall {a:Type} {a_WT:WhyType a}, (set1 a).
(* Why3 assumption *)
Definition assigns(sigma:(map mident value)) (a:(set.Set.set mident))
(sigma':(map mident value)): Prop := forall (i:mident), (~ (set.Set.mem i
a)) -> ((get sigma i) = (get sigma' i)).
Definition is_empty {a:Type} {a_WT:WhyType a}(s:(set1 a)): Prop :=
forall (x:a), ~ (mem1 x s).
Axiom empty_def1 : forall {a:Type} {a_WT:WhyType a}, (is_empty (empty :(set1
a))).
Parameter add: forall {a:Type} {a_WT:WhyType a}, a -> (set1 a) -> (set1 a).
Axiom add_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a),
forall (s:(set1 a)), (mem1 x (add y s)) <-> ((x = y) \/ (mem1 x s)).
Parameter remove: forall {a:Type} {a_WT:WhyType a}, a -> (set1 a) -> (set1
a).
Axiom remove_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(s:(set1 a)), (mem1 x (remove y s)) <-> ((~ (x = y)) /\ (mem1 x s)).
Axiom subset_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set1
a)), (subset (remove x s) s).
Parameter union: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> (set1 a) ->
(set1 a).
Axiom assigns_refl : forall (sigma:(map mident value)) (a:(set.Set.set
mident)), (assigns sigma a sigma).
Axiom union_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)) (x:a), (mem1 x (union s1 s2)) <-> ((mem1 x s1) \/ (mem1 x
s2)).
Parameter inter: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> (set1 a) ->
(set1 a).
Axiom inter_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)) (x:a), (mem1 x (inter s1 s2)) <-> ((mem1 x s1) /\ (mem1 x
s2)).
Parameter diff: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> (set1 a) ->
(set1 a).
Axiom diff_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)) (x:a), (mem1 x (diff s1 s2)) <-> ((mem1 x s1) /\ ~ (mem1 x
s2)).
Axiom subset_diff : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)), (subset (diff s1 s2) s1).
Parameter choose: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> a.
Axiom choose_def : forall {a:Type} {a_WT:WhyType a}, forall (s:(set1 a)),
(~ (is_empty s)) -> (mem1 (choose s) s).
Parameter all: forall {a:Type} {a_WT:WhyType a}, (set1 a).
Axiom all_def : forall {a:Type} {a_WT:WhyType a}, forall (x:a), (mem1 x
(all :(set1 a))).
(* Why3 assumption *)
Definition assigns(sigma:(map mident value)) (a:(set1 mident)) (sigma':(map
mident value)): Prop := forall (i:mident), (~ (mem1 i a)) -> ((get sigma
i) = (get sigma' i)).
Axiom assigns_refl : forall (sigma:(map mident value)) (a:(set1 mident)),
(assigns sigma a sigma).
Axiom assigns_trans : forall (sigma1:(map mident value)) (sigma2:(map mident
value)) (sigma3:(map mident value)) (a:(set.Set.set mident)),
((assigns sigma1 a sigma2) /\ (assigns sigma2 a sigma3)) -> (assigns sigma1
a sigma3).
value)) (sigma3:(map mident value)) (a:(set1 mident)), ((assigns sigma1 a
sigma2) /\ (assigns sigma2 a sigma3)) -> (assigns sigma1 a sigma3).
Axiom assigns_union_left : forall (sigma:(map mident value)) (sigma':(map
mident value)) (s1:(set.Set.set mident)) (s2:(set.Set.set mident)),
(assigns sigma s1 sigma') -> (assigns sigma (set.Set.union s1 s2) sigma').
mident value)) (s1:(set1 mident)) (s2:(set1 mident)), (assigns sigma s1
sigma') -> (assigns sigma (union s1 s2) sigma').
Axiom assigns_union_right : forall (sigma:(map mident value)) (sigma':(map
mident value)) (s1:(set.Set.set mident)) (s2:(set.Set.set mident)),
(assigns sigma s2 sigma') -> (assigns sigma (set.Set.union s1 s2) sigma').
mident value)) (s1:(set1 mident)) (s2:(set1 mident)), (assigns sigma s2
sigma') -> (assigns sigma (union s1 s2) sigma').
(* Why3 assumption *)
Fixpoint stmt_writes(s:stmt) (w:(set.Set.set mident)) {struct s}: Prop :=
Fixpoint stmt_writes(s:stmt) (w:(set1 mident)) {struct s}: Prop :=
match s with
| (Sskip|(Sassert _)) => True
| (Sassign id _) => (set.Set.mem id w)
| (Sassign id _) => (mem1 id w)
| (Sseq s1 s2) => (stmt_writes s1 w) /\ (stmt_writes s2 w)
| (Sif t s1 s2) => (stmt_writes s1 w) /\ (stmt_writes s2 w)
| (Swhile _ _ body) => (stmt_writes body w)
......@@ -617,10 +693,16 @@ Axiom abstract_effects_generalize : forall (sigma:(map mident value))
(pi:(list (ident* value)%type)) (s:stmt) (f:fmla), (eval_fmla sigma pi
(abstract_effects s f)) -> (eval_fmla sigma pi f).
Axiom abstract_effects_monotonic : forall (s:stmt) (f:fmla),
forall (sigma:(map mident value)) (pi:(list (ident* value)%type)),
(eval_fmla sigma pi f) -> forall (sigma1:(map mident value)) (pi1:(list
(ident* value)%type)), (eval_fmla sigma1 pi1 (abstract_effects s f)).
Axiom abstract_effects_monotonic : forall (s:stmt) (p:fmla) (q:fmla),
(valid_fmla (Fimplies p q)) -> forall (sigma:(map mident value)) (pi:(list
(ident* value)%type)), (eval_fmla sigma pi (abstract_effects s p)) ->
(eval_fmla sigma pi (abstract_effects s q)).
Axiom abstract_effects_distrib_conj : forall (s:stmt) (p:fmla) (q:fmla)
(sigma:(map mident value)) (pi:(list (ident* value)%type)),
((eval_fmla sigma pi (abstract_effects s p)) /\ (eval_fmla sigma pi
(abstract_effects s q))) -> (eval_fmla sigma pi (abstract_effects s (Fand p
q))).
(* Why3 assumption *)
Fixpoint wp(s:stmt) (q:fmla) {struct s}: fmla :=
......
......@@ -206,15 +206,12 @@ lemma steps_non_neg:
many_steps sigma1 pi1 s1 sigma2 pi2 s2 n -> n >= 0
predicate reducible (sigma:env) (pi:stack) (s:stmt) =
predicate reductible (sigma:env) (pi:stack) (s:stmt) =
exists sigma':env, pi':stack, s':stmt.
one_step sigma pi s sigma' pi' s'
end
......@@ -478,27 +475,6 @@ function msubst_term (t:term) (r:mident) (v:ident) : term =
Tbin (msubst_term t1 r v) op (msubst_term t2 r v)
end
(*
function subst_term (t:term) (r:ident) (v:ident) : term =
match t with
| Tvalue _ | Tderef _ -> t
| Tvar x ->
if r = x then Tvar v else t
| Tbin t1 op t2 ->
Tbin (subst_term t1 r v) op (subst_term t2 r v)
end
function subst (f:fmla) (x:ident) (v:ident) : fmla =
match f with
| Fterm e -> Fterm (subst_term e x v)
| Fand f1 f2 -> Fand (subst f1 x v) (subst f2 x v)
| Fnot f -> Fnot (subst f x v)
| Fimplies f1 f2 -> Fimplies (subst f1 x v) (subst f2 x v)
| Flet y t f -> Flet y (subst_term t x v) (subst f x v)
| Fforall y ty f -> Fforall y ty (subst f x v)
end
*)
function msubst (f:fmla) (x:mident) (v:ident) : fmla =
match f with
| Fterm e -> Fterm (msubst_term e x v)
......@@ -509,17 +485,6 @@ function msubst (f:fmla) (x:mident) (v:ident) : fmla =
| Fforall y ty f -> Fforall y ty (msubst f x v)
end
(*
lemma subst_fresh_term :
forall t:term, x:ident, v:ident.
fresh_in_term x t -> subst_term t x v = t
*)
(*
lemma subst_fresh :
forall f:fmla, x:ident, v:ident.
fresh_in_fmla x f -> subst f x v = f
*)
(* Needed for monotonicity and wp_reduction *)
lemma eval_msubst_term:
......@@ -657,67 +622,59 @@ use import Typing
use import TypingAndSemantics
use import FreshVariables
(*
use set.Set
*)
(*
(** [assigns sigma W sigma'] is true when the only differences between
[sigma] and [sigma'] are the value of references in [W] *)
predicate assigns (sigma:env) (a:Set.set mident) (sigma':env) =
forall i:mident. not (Set.mem i a) ->
IdMap.get sigma i = IdMap.get sigma' i
lemma assigns_refl:
forall sigma:env, a:Set.set mident. assigns sigma a sigma
lemma assigns_trans:
forall sigma1 sigma2 sigma3:env, a:Set.set mident.
assigns sigma1 a sigma2 /\ assigns sigma2 a sigma3 ->
assigns sigma1 a sigma3
lemma assigns_union_left:
forall sigma sigma':env, s1 s2:Set.set mident.
assigns sigma s1 sigma' -> assigns sigma (Set.union s1 s2) sigma'
lemma assigns_union_right:
forall sigma sigma':env, s1 s2:Set.set mident.
assigns sigma s2 sigma' -> assigns sigma (Set.union s1 s2) sigma'
*)
(*
(** [stmt_writes e W] is true when the only references modified by [e] are in [W] *)
predicate stmt_writes (s:stmt) (w:Set.set mident) =
match s with
| Sskip | Sassert _ -> true
| Sassign id _ -> Set.mem id w
| Sseq s1 s2 -> stmt_writes s1 w /\ stmt_writes s2 w
| Sif t s1 s2 -> stmt_writes s1 w /\ stmt_writes s2 w
| Swhile _ _ body -> stmt_writes body w
end
*)
function fresh_from (f:fmla) : ident
function fresh_from (f:fmla) : ident
(* Need it for monotonicity*)
axiom fresh_from_fmla: forall f:fmla.
fresh_in_fmla (fresh_from f) f
axiom fresh_from_fmla: forall f:fmla.
fresh_in_fmla (fresh_from f) f
(* intention:
abstract_effects s f = "forall w. f"
avec w = writes(s)
*)
function abstract_effects (s:stmt) (f:fmla) : fmla
(* hypothese 1: si
sigma, pi |= forall w. f
alors
sigma, pi |= f
*)
axiom abstract_effects_generalize :
forall sigma:env, pi:stack, s:stmt, f:fmla.
eval_fmla sigma pi (abstract_effects s f) ->
eval_fmla sigma pi f
axiom abstract_effects_monotonic :
forall s:stmt, f:fmla.
forall sigma:env, pi:stack. eval_fmla sigma pi f ->
forall sigma:env, pi:stack. eval_fmla sigma pi (abstract_effects s f)
(* hypothese 2: si
|= p -> q
alors
|= (forall w, p) -> (forall w, q)
remarque : il est essentiel de parler de validité dans tous les etats:
on n'a pas
sigma,pi |= p -> q
implique
sigma,pi |= (forall w, p) -> (forall w, q)
function wp (s:stmt) (q:fmla) : fmla =
contre-exemple: sigma(x) = 42 alors true -> x=42
mais on n'a
(forall x, true) -> (forall x, x=42)
*)
axiom abstract_effects_monotonic :
forall s:stmt, p q:fmla.
valid_fmla (Fimplies p q) ->
forall sigma:env, pi:stack.
eval_fmla sigma pi (abstract_effects s p) ->
eval_fmla sigma pi (abstract_effects s q)
axiom abstract_effects_distrib_conj :
forall s:stmt, p q:fmla, sigma:env, pi:stack.
eval_fmla sigma pi (abstract_effects s p) /\
eval_fmla sigma pi (abstract_effects s q) ->
eval_fmla sigma pi (abstract_effects s (Fand p q))
function wp (s:stmt) (q:fmla) : fmla =
match s with
| Sskip -> q
| Sassert f ->
......@@ -749,6 +706,17 @@ predicate stmt_writes (s:stmt) (w:Set.set mident) =
valid_fmla (Fimplies p q)
-> valid_fmla (Fimplies (wp s p) (wp s q) )
(* remarque l'ordre des quantifications est essentiel, on n'a pas
sigma,pi |= p -> q
implique
sigma,pi |= (wp s p) -> (wp s q)
meme contre-exemple: sigma(x) = 42 alors true -> x=42
mais
wp (x := 7) true = true
wp (x := 7) x=42 = 7=42
*)
lemma distrib_conj:
forall s:stmt, sigma:env, pi:stack, p q:fmla.
(eval_fmla sigma pi (wp s p)) /\
......@@ -768,7 +736,7 @@ predicate stmt_writes (s:stmt) (w:Set.set mident) =
compatible_env sigma sigmat pi pit ->
type_stmt sigmat pit s ->
eval_fmla sigma pi (wp s q) ->
s <> Sskip -> reducible sigma pi s
s <> Sskip -> reductible sigma pi s
(** {3 main soundness result} *)
......@@ -778,7 +746,7 @@ predicate stmt_writes (s:stmt) (w:Set.set mident) =
compatible_env sigma sigmat pi pit ->
type_stmt sigmat pit s ->
many_steps sigma pi s sigma' pi' s' n /\
not (reducible sigma' pi' s') /\
not (reductible sigma' pi' s') /\
eval_fmla sigma pi (wp s q) ->
s' = Sskip /\ eval_fmla sigma' pi' q
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
(* Why3 assumption *)
Inductive datatype :=
| TYunit : datatype
| TYint : datatype
| TYbool : datatype .
Axiom datatype_WhyType : WhyType datatype.
Existing Instance datatype_WhyType.
(* Why3 assumption *)
Inductive value :=
| Vvoid : value
| Vint : Z -> value
| Vbool : bool -> value .
Axiom value_WhyType : WhyType value.
Existing Instance value_WhyType.
(* Why3 assumption *)
Inductive operator :=
| Oplus : operator
| Ominus : operator
| Omult : operator
| Ole : operator .
Axiom operator_WhyType : WhyType operator.
Existing Instance operator_WhyType.
Axiom mident : Type.
Parameter mident_WhyType : WhyType mident.
Existing Instance mident_WhyType.
Axiom mident_decide : forall (m1:mident) (m2:mident), (m1 = m2) \/
~ (m1 = m2).
Axiom ident : Type.
Parameter ident_WhyType : WhyType ident.
Existing Instance ident_WhyType.
Axiom ident_decide : forall (m1:ident) (m2:ident), (m1 = m2) \/ ~ (m1 = m2).
(* Why3 assumption *)
Inductive term :=
| Tvalue : value -> term
| Tvar : ident -> term
| Tderef : mident -> term
| Tbin : term -> operator -> term -> term .
Axiom term_WhyType : WhyType term.
Existing Instance term_WhyType.
(* Why3 assumption *)
Inductive fmla :=
| Fterm : term -> fmla
| Fand : fmla -> fmla -> fmla
| Fnot : fmla -> fmla
| Fimplies : fmla -> fmla -> fmla
| Flet : ident -> term -> fmla -> fmla
| Fforall : ident -> datatype -> fmla -> fmla .
Axiom fmla_WhyType : WhyType fmla.
Existing Instance fmla_WhyType.
(* Why3 assumption *)
Inductive stmt :=
| Sskip : stmt
| Sassign : mident -> term -> stmt
| Sseq : stmt -> stmt -> stmt
| Sif : term -> stmt -> stmt -> stmt
| Sassert : fmla -> stmt
| Swhile : term -> fmla -> stmt -> stmt .
Axiom stmt_WhyType : WhyType stmt.
Existing Instance stmt_WhyType.
Axiom decide_is_skip : forall (s:stmt), (s = Sskip) \/ ~ (s = Sskip).
Axiom map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, Type.
Parameter map_WhyType : forall (a:Type) {a_WT:WhyType a}
(b:Type) {b_WT:WhyType b}, WhyType (map a b).
Existing Instance map_WhyType.
Parameter get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b.
Parameter set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b -> (map a b).
Axiom Select_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) ->
((get (set m a1 b1) a2) = b1).
Axiom Select_neq : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, forall (m:(map a b)), forall (a1:a) (a2:a),
forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1) a2) = (get m a2)).
Parameter const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
b -> (map a b).
Axiom Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (b1:b) (a1:a), ((get (const b1:(map a b)) a1) = b1).
(* Why3 assumption *)
Inductive list (a:Type) {a_WT:WhyType a} :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a).
Existing Instance list_WhyType.
Implicit Arguments Nil [[a] [a_WT]].
Implicit Arguments Cons [[a] [a_WT]].
(* Why3 assumption *)
Definition env := (map mident value).
(* Why3 assumption *)
Definition stack := (list (ident* value)%type).
Parameter get_stack: ident -> (list (ident* value)%type) -> value.
Axiom get_stack_def : forall (i:ident) (pi:(list (ident* value)%type)),
match pi with
| Nil => ((get_stack i pi) = Vvoid)
| (Cons (x, v) r) => ((x = i) -> ((get_stack i pi) = v)) /\ ((~ (x = i)) ->
((get_stack i pi) = (get_stack i r)))
end.
Axiom get_stack_eq : forall (x:ident) (v:value) (r:(list (ident*
value)%type)), ((get_stack x (Cons (x, v) r)) = v).
Axiom get_stack_neq : forall (x:ident) (i:ident) (v:value) (r:(list (ident*
value)%type)), (~ (x = i)) -> ((get_stack i (Cons (x, v) r)) = (get_stack i
r)).
Parameter eval_bin: value -> operator -> value -> value.
Axiom eval_bin_def : forall (x:value) (op:operator) (y:value), match (x,
y) with
| ((Vint x1), (Vint y1)) =>
match op with
| Oplus => ((eval_bin x op y) = (Vint (x1 + y1)%Z))
| Ominus => ((eval_bin x op y) = (Vint (x1 - y1)%Z))
| Omult => ((eval_bin x op y) = (Vint (x1 * y1)%Z))
| Ole => ((x1 <= y1)%Z -> ((eval_bin x op y) = (Vbool true))) /\
((~ (x1 <= y1)%Z) -> ((eval_bin x op y) = (Vbool false)))
end
| (_, _) => ((eval_bin x op y) = Vvoid)
end.
(* Why3 assumption *)
Fixpoint eval_term(sigma:(map mident value)) (pi:(list (ident* value)%type))
(t:term) {struct t}: value :=
match t with
| (Tvalue v) => v
| (Tvar id) => (get_stack id pi)
| (Tderef id) => (get sigma id)
| (Tbin t1 op t2) => (eval_bin (eval_term sigma pi t1) op (eval_term sigma
pi t2))
end.
(* Why3 assumption *)
Fixpoint eval_fmla(sigma:(map mident value)) (pi:(list (ident* value)%type))
(f:fmla) {struct f}: Prop :=
match f with
| (Fterm t) => ((eval_term sigma pi t) = (Vbool true))
| (Fand f1 f2) => (eval_fmla sigma pi f1) /\ (eval_fmla sigma pi f2)
| (Fnot f1) => ~ (eval_fmla sigma pi f1)
| (Fimplies f1 f2) => (eval_fmla sigma pi f1) -> (eval_fmla sigma pi f2)
| (Flet x t f1) => (eval_fmla sigma (Cons (x, (eval_term sigma pi t)) pi)
f1)
| (Fforall x TYint f1) => forall (n:Z), (eval_fmla sigma (Cons (x,
(Vint n)) pi) f1)
| (Fforall x TYbool f1) => forall (b:bool), (eval_fmla sigma (Cons (x,
(Vbool b)) pi) f1)
| (Fforall x TYunit f1) => (eval_fmla sigma (Cons (x, Vvoid) pi) f1)
end.
(* Why3 assumption *)
Definition valid_fmla(p:fmla): Prop := forall (sigma:(map mident value))
(pi:(list (ident* value)%type)), (eval_fmla sigma pi p).
(* Why3 assumption *)
Inductive one_step : (map mident value) -> (list (ident* value)%type) -> stmt
-> (map mident value) -> (list (ident* value)%type) -> stmt -> Prop :=
| one_step_assign : forall (sigma:(map mident value)) (sigma':(map mident
value)) (pi:(list (ident* value)%type)) (x:mident) (t:term),
(sigma' = (set sigma x (eval_term sigma pi t))) -> (one_step sigma pi
(Sassign x t) sigma' pi Sskip)
| one_step_seq_noskip : forall (sigma:(map mident value)) (sigma':(map
mident value)) (pi:(list (ident* value)%type)) (pi':(list (ident*
value)%type)) (s1:stmt) (s1':stmt) (s2:stmt), (one_step sigma pi s1
sigma' pi' s1') -> (one_step sigma pi (Sseq s1 s2) sigma' pi' (Sseq s1'