Commit 693db5a7 authored by Léon Gondelman's avatar Léon Gondelman
Browse files

mini-compiler: proved (4 goals by coq)

parent 057b8d9f
......@@ -185,6 +185,35 @@ module Compile_com
meta rewrite_def function exn_bool_old
function loop_invariant (c: com) : ('a,machine_state) -> pos -> pred =
\ x p msi. let ms0 = snd x in
match ms0, msi with
| VMS _ s0 m0, VMS pi si mi ->
pi = p /\ s0 = si /\ exists mf. ceval m0 c mf /\ ceval mi c mf
end
meta rewrite_def function loop_invariant
function loop_post (c : com) (len: pos) : ('a,machine_state) -> pos -> pred =
\ x p msf. let ms0 = snd x in
match ms0, msf with
| VMS _ s0 m0, VMS pf sf mf ->
pf = p + len /\ s0 = sf /\ ceval m0 c mf
end
meta rewrite_def function loop_post
function loop_variant (c : com) (test: bexpr) : ('a -> pos -> post) =
\ x p msj msi.
match msj, msi with
| VMS pj sj mj, VMS pi si mi ->
pj = pi /\ sj = si /\ ceval mi c mj /\ beval mi test = True
end
meta rewrite_def function loop_variant
let rec compile_com (cmd: com) : hl 'a
variant { cmd }
ensures { result.pre = com_pre cmd }
......@@ -201,12 +230,45 @@ module Compile_com
$ compile_bexpr cond False (code_true.code.length + 1) ~
(($ code_true ~ $ ibranchf code_false.code.length) % exn_bool cond False) ~
($ code_false % exn_bool_old cond True)
| _ -> absurd
| Cwhile test body ->
let code_body = compile_com body in
let body_length = length code_body.code + 1 in
let code_test = compile_bexpr test False (body_length) in
let ofs = (length code_test.code + body_length) in
let wp_while = $ code_test ~
($ code_body ~ $ ibranchf (- ofs)) % exn_bool test False in
let ghost inv = loop_invariant cmd in
let ghost var = loop_variant body test in
let ghost post = loop_post cmd ofs in
let hl_while = hoare inv wp_while (loop_preservation inv var post) in
$ inil () ~ $ make_loop_hl hl_while inv var post
end
in
let ghost pre = com_pre cmd in
let ghost post = com_post cmd res.wcode.length in
hoare pre res post
hoare pre res post
let compile_com_natural (com: com) : code
ensures {
forall c p s m m'.
ceval m com m' ->
codeseq_at c p result ->
transition_star c
(VMS p s m)
(VMS (p + length result) s m') }
= let res = compile_com com : hl unit in
assert { forall p s m m'. ceval m com m' -> res.pre () p (VMS p s m) };
res.code
let compile_program (prog : com) : code
ensures { forall mi mf: state.
ceval mi prog mf -> vm_terminates result mi mf }
= compile_com_natural prog ++ ihalt
end
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.EuclideanDivision.
Require list.List.
Require list.Length.
Require list.Mem.
Require map.Map.
Require bool.Bool.
Require list.Append.
(* Why3 assumption *)
Definition unit := unit.
Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.
Axiom map : forall (a:Type) (b:Type), 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 id :=
| Id : Z -> id.
Axiom id_WhyType : WhyType id.
Existing Instance id_WhyType.
(* Why3 assumption *)
Definition state := (map id Z).
(* Why3 assumption *)
Inductive aexpr :=
| Anum : Z -> aexpr
| Avar : id -> aexpr
| Aadd : aexpr -> aexpr -> aexpr
| Asub : aexpr -> aexpr -> aexpr
| Amul : aexpr -> aexpr -> aexpr.
Axiom aexpr_WhyType : WhyType aexpr.
Existing Instance aexpr_WhyType.
(* Why3 assumption *)
Inductive bexpr :=
| Btrue : bexpr
| Bfalse : bexpr
| Band : bexpr -> bexpr -> bexpr
| Bnot : bexpr -> bexpr
| Beq : aexpr -> aexpr -> bexpr
| Ble : aexpr -> aexpr -> bexpr.
Axiom bexpr_WhyType : WhyType bexpr.
Existing Instance bexpr_WhyType.
(* Why3 assumption *)
Inductive com :=
| Cskip : com
| Cassign : id -> aexpr -> com
| Cseq : com -> com -> com
| Cif : bexpr -> com -> com -> com
| Cwhile : bexpr -> com -> com.
Axiom com_WhyType : WhyType com.
Existing Instance com_WhyType.
(* Why3 assumption *)
Fixpoint aeval (st:(map id Z)) (e:aexpr) {struct e}: Z :=
match e with
| (Anum n) => n
| (Avar x) => (get st x)
| (Aadd e1 e2) => ((aeval st e1) + (aeval st e2))%Z
| (Asub e1 e2) => ((aeval st e1) - (aeval st e2))%Z
| (Amul e1 e2) => ((aeval st e1) * (aeval st e2))%Z
end.
Parameter beval: (map id Z) -> bexpr -> bool.
Axiom beval_def : forall (st:(map id Z)) (b:bexpr),
match b with
| Btrue => ((beval st b) = true)
| Bfalse => ((beval st b) = false)
| (Bnot b') => ((beval st b) = (Init.Datatypes.negb (beval st b')))
| (Band b1 b2) => ((beval st b) = (Init.Datatypes.andb (beval st
b1) (beval st b2)))
| (Beq a1 a2) => (((aeval st a1) = (aeval st a2)) -> ((beval st
b) = true)) /\ ((~ ((aeval st a1) = (aeval st a2))) -> ((beval st
b) = false))
| (Ble a1 a2) => (((aeval st a1) <= (aeval st a2))%Z -> ((beval st
b) = true)) /\ ((~ ((aeval st a1) <= (aeval st a2))%Z) -> ((beval st
b) = false))
end.
Axiom inversion_beval_t : forall (a1:aexpr) (a2:aexpr) (m:(map id Z)),
((beval m (Beq a1 a2)) = true) -> ((aeval m a1) = (aeval m a2)).
Axiom inversion_beval_f : forall (a1:aexpr) (a2:aexpr) (m:(map id Z)),
((beval m (Beq a1 a2)) = false) -> ~ ((aeval m a1) = (aeval m a2)).
(* Why3 assumption *)
Inductive ceval: (map id Z) -> com -> (map id Z) -> Prop :=
| E_Skip : forall (m:(map id Z)), (ceval m Cskip m)
| E_Ass : forall (m:(map id Z)) (a:aexpr) (n:Z) (x:id), ((aeval m
a) = n) -> (ceval m (Cassign x a) (set m x n))
| E_Seq : forall (cmd1:com) (cmd2:com) (m0:(map id Z)) (m1:(map id Z))
(m2:(map id Z)), (ceval m0 cmd1 m1) -> ((ceval m1 cmd2 m2) -> (ceval m0
(Cseq cmd1 cmd2) m2))
| E_IfTrue : forall (m0:(map id Z)) (m1:(map id Z)) (cond:bexpr) (cmd1:com)
(cmd2:com), ((beval m0 cond) = true) -> ((ceval m0 cmd1 m1) -> (ceval
m0 (Cif cond cmd1 cmd2) m1))
| E_IfFalse : forall (m0:(map id Z)) (m1:(map id Z)) (cond:bexpr)
(cmd1:com) (cmd2:com), ((beval m0 cond) = false) -> ((ceval m0 cmd2
m1) -> (ceval m0 (Cif cond cmd1 cmd2) m1))
| E_WhileEnd : forall (cond:bexpr) (m:(map id Z)) (body:com), ((beval m
cond) = false) -> (ceval m (Cwhile cond body) m)
| E_WhileLoop : forall (mi:(map id Z)) (mj:(map id Z)) (mf:(map id Z))
(cond:bexpr) (body:com), ((beval mi cond) = true) -> ((ceval mi body
mj) -> ((ceval mj (Cwhile cond body) mf) -> (ceval mi (Cwhile cond
body) mf))).
(* Why3 assumption *)
Definition pos := Z.
(* Why3 assumption *)
Definition stack := (list Z).
(* Why3 assumption *)
Inductive machine_state :=
| VMS : Z -> (list Z) -> (map id Z) -> machine_state.
Axiom machine_state_WhyType : WhyType machine_state.
Existing Instance machine_state_WhyType.
(* Why3 assumption *)
Inductive instr :=
| Iconst : Z -> instr
| Ivar : id -> instr
| Isetvar : id -> instr
| Ibranch_fwd : Z -> instr
| Ibranch_bwd : Z -> instr
| Iadd : instr
| Isub : instr
| Imul : instr
| Ibeq : Z -> instr
| Ibne : Z -> instr
| Ible : Z -> instr
| Ibgt : Z -> instr
| Ihalt : instr.
Axiom instr_WhyType : WhyType instr.
Existing Instance instr_WhyType.
(* Why3 assumption *)
Definition code := (list instr).
(* Why3 assumption *)
Inductive codeseq_at: (list instr) -> Z -> (list instr) -> Prop :=
| codeseq_at_intro : forall (c1:(list instr)) (c2:(list instr))
(c3:(list instr)) (pc:Z), (pc = (list.Length.length c1)) -> (codeseq_at
(Init.Datatypes.app (Init.Datatypes.app c1 c2) c3) pc c2).
Axiom codeseq_at_app_right : forall (c:(list instr)) (c1:(list instr))
(c2:(list instr)) (p:Z), (codeseq_at c p (Init.Datatypes.app c1 c2)) ->
(codeseq_at c (p + (list.Length.length c1))%Z c2).
Axiom codeseq_at_app_left : forall (c:(list instr)) (c1:(list instr))
(c2:(list instr)) (p:Z), (codeseq_at c p (Init.Datatypes.app c1 c2)) ->
(codeseq_at c p c1).
(* Why3 assumption *)
Definition iconst (n:Z): (list instr) :=
(Init.Datatypes.cons (Iconst n) Init.Datatypes.nil).
(* Why3 assumption *)
Definition ivar (x:id): (list instr) :=
(Init.Datatypes.cons (Ivar x) Init.Datatypes.nil).
(* Why3 assumption *)
Definition isetvar (x:id): (list instr) :=
(Init.Datatypes.cons (Isetvar x) Init.Datatypes.nil).
(* Why3 assumption *)
Definition ibeq (ofs:Z): (list instr) :=
(Init.Datatypes.cons (Ibeq ofs) Init.Datatypes.nil).
(* Why3 assumption *)
Definition ible (ofs:Z): (list instr) :=
(Init.Datatypes.cons (Ible ofs) Init.Datatypes.nil).
(* Why3 assumption *)
Definition ibne (ofs:Z): (list instr) :=
(Init.Datatypes.cons (Ibne ofs) Init.Datatypes.nil).
(* Why3 assumption *)
Definition ibgt (ofs:Z): (list instr) :=
(Init.Datatypes.cons (Ibgt ofs) Init.Datatypes.nil).
(* Why3 assumption *)
Definition ibranchf (ofs:Z): (list instr) :=
(Init.Datatypes.cons (Ibranch_fwd ofs) Init.Datatypes.nil).
(* Why3 assumption *)
Definition ibranchb (ofs:Z): (list instr) :=
(Init.Datatypes.cons (Ibranch_bwd ofs) Init.Datatypes.nil).
(* Why3 assumption *)
Inductive transition: (list instr) -> machine_state -> machine_state ->
Prop :=
| trans_const : forall (c:(list instr)) (p:Z) (n:Z), (codeseq_at c p
(iconst n)) -> forall (m:(map id Z)) (s:(list Z)), (transition c (VMS p
s m) (VMS (p + 1%Z)%Z (Init.Datatypes.cons n s) m))
| trans_var : forall (c:(list instr)) (p:Z) (x:id), (codeseq_at c p
(ivar x)) -> forall (m:(map id Z)) (s:(list Z)), (transition c (VMS p s
m) (VMS (p + 1%Z)%Z (Init.Datatypes.cons (get m x) s) m))
| trans_set_var : forall (c:(list instr)) (p:Z) (s:(list Z)) (x:id),
(codeseq_at c p (isetvar x)) -> forall (n:Z) (m:(map id Z)),
(transition c (VMS p (Init.Datatypes.cons n s) m) (VMS (p + 1%Z)%Z s
(set m x n)))
| trans_add : forall (c:(list instr)) (p:Z), (codeseq_at c p
(Init.Datatypes.cons Iadd Init.Datatypes.nil)) -> forall (n1:Z) (n2:Z)
(s:(list Z)) (m:(map id Z)), (transition c (VMS p
(Init.Datatypes.cons n2 (Init.Datatypes.cons n1 s)) m) (VMS (p + 1%Z)%Z
(Init.Datatypes.cons (n1 + n2)%Z s) m))
| trans_sub : forall (c:(list instr)) (p:Z), (codeseq_at c p
(Init.Datatypes.cons Isub Init.Datatypes.nil)) -> forall (n1:Z) (n2:Z)
(s:(list Z)) (m:(map id Z)), (transition c (VMS p
(Init.Datatypes.cons n2 (Init.Datatypes.cons n1 s)) m) (VMS (p + 1%Z)%Z
(Init.Datatypes.cons (n1 - n2)%Z s) m))
| trans_mul : forall (c:(list instr)) (p:Z), (codeseq_at c p
(Init.Datatypes.cons Imul Init.Datatypes.nil)) -> forall (n1:Z) (n2:Z)
(s:(list Z)) (m:(map id Z)), (transition c (VMS p
(Init.Datatypes.cons n2 (Init.Datatypes.cons n1 s)) m) (VMS (p + 1%Z)%Z
(Init.Datatypes.cons (n1 * n2)%Z s) m))
| trans_beq : forall (c:(list instr)) (p1:Z) (p2:Z) (ofs:Z) (n1:Z) (n2:Z),
(codeseq_at c p1 (ibeq ofs)) -> ((((n1 = n2) /\
(p2 = ((p1 + 1%Z)%Z + ofs)%Z)) \/ ((~ (n1 = n2)) /\
(p2 = (p1 + 1%Z)%Z))) -> forall (s:(list Z)) (m:(map id Z)),
(transition c (VMS p1
(Init.Datatypes.cons n2 (Init.Datatypes.cons n1 s)) m) (VMS p2 s m)))
| trans_bne : forall (c:(list instr)) (p1:Z) (p2:Z) (ofs:Z) (n1:Z) (n2:Z),
(codeseq_at c p1 (ibne ofs)) -> ((((n1 = n2) /\ (p2 = (p1 + 1%Z)%Z)) \/
((~ (n1 = n2)) /\ (p2 = ((p1 + 1%Z)%Z + ofs)%Z))) ->
forall (s:(list Z)) (m:(map id Z)), (transition c (VMS p1
(Init.Datatypes.cons n2 (Init.Datatypes.cons n1 s)) m) (VMS p2 s m)))
| trans_ble : forall (c:(list instr)) (p1:Z) (p2:Z) (ofs:Z) (n1:Z) (n2:Z),
(codeseq_at c p1 (ible ofs)) -> ((((n1 <= n2)%Z /\
(p2 = ((p1 + 1%Z)%Z + ofs)%Z)) \/ ((~ (n1 <= n2)%Z) /\
(p2 = (p1 + 1%Z)%Z))) -> forall (s:(list Z)) (m:(map id Z)),
(transition c (VMS p1
(Init.Datatypes.cons n2 (Init.Datatypes.cons n1 s)) m) (VMS p2 s m)))
| trans_bgt : forall (c:(list instr)) (p1:Z) (p2:Z) (ofs:Z) (n1:Z) (n2:Z),
(codeseq_at c p1 (ibgt ofs)) -> ((((n1 <= n2)%Z /\
(p2 = (p1 + 1%Z)%Z)) \/ ((~ (n1 <= n2)%Z) /\
(p2 = ((p1 + 1%Z)%Z + ofs)%Z))) -> forall (s:(list Z)) (m:(map id Z)),
(transition c (VMS p1
(Init.Datatypes.cons n2 (Init.Datatypes.cons n1 s)) m) (VMS p2 s m)))
| trans_branch_fwd : forall (c:(list instr)) (p:Z) (ofs:Z), (codeseq_at c p
(ibranchf ofs)) -> forall (m:(map id Z)) (s:(list Z)), (transition c
(VMS p s m) (VMS ((p + 1%Z)%Z + ofs)%Z s m))
| trans_branch_bwd : forall (c:(list instr)) (p:Z) (ofs:Z), (codeseq_at c p
(ibranchb ofs)) -> forall (m:(map id Z)) (s:(list Z)), (transition c
(VMS p s m) (VMS ((p + 1%Z)%Z - ofs)%Z s m)).
(* Why3 assumption *)
Inductive trans :=
| TransZero : trans
| TransOne : machine_state -> trans -> trans.
Axiom trans_WhyType : WhyType trans.
Existing Instance trans_WhyType.
(* Why3 assumption *)
Fixpoint transition_star_proof (p:(list instr)) (s1:machine_state)
(s3:machine_state) (pi:trans) {struct pi}: Prop :=
match pi with
| TransZero => (s1 = s3)
| (TransOne s2 pi') => (transition p s1 s2) /\ (transition_star_proof p s2
s3 pi')
end.
Parameter transition_star: (list instr) -> machine_state -> machine_state ->
Prop.
Axiom transition_star_def : forall (p:(list instr)) (s1:machine_state)
(s3:machine_state), (transition_star p s1 s3) <-> exists pi:trans,
(transition_star_proof p s1 s3 pi).
Axiom transZero : forall (p:(list instr)) (s:machine_state), (transition_star
p s s).
Axiom transOne : forall (p:(list instr)) (s1:machine_state)
(s2:machine_state) (s3:machine_state), (transition p s1 s2) ->
((transition_star p s2 s3) -> (transition_star p s1 s3)).
Axiom transition_star_one : forall (p:(list instr)) (s1:machine_state)
(s2:machine_state), (transition p s1 s2) -> (transition_star p s1 s2).
Axiom trans_star : forall (p:(list instr)) (s1:machine_state)
(s2:machine_state) (s3:machine_state) (pi:trans), ((transition_star_proof p
s1 s2 pi) /\ (transition_star p s2 s3)) -> (transition_star p s1 s3).
Axiom transition_star_transitive : forall (p:(list instr)) (s1:machine_state)
(s2:machine_state) (s3:machine_state), (transition_star p s1 s2) ->
((transition_star p s2 s3) -> (transition_star p s1 s3)).
(* Why3 assumption *)
Definition vm_terminates (c:(list instr)) (mi:(map id Z)) (mf:(map id
Z)): Prop := exists p:Z, (codeseq_at c p
(Init.Datatypes.cons Ihalt Init.Datatypes.nil)) /\ (transition_star c
(VMS 0%Z Init.Datatypes.nil mi) (VMS p Init.Datatypes.nil mf)).
Axiom func : forall (a:Type) (b:Type), Type.
Parameter func_WhyType : forall (a:Type) {a_WT:WhyType a}
(b:Type) {b_WT:WhyType b}, WhyType (func a b).
Existing Instance func_WhyType.
(* Why3 assumption *)
Definition pred (a:Type) := (func a bool).
Parameter infix_at: forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, (func a b) -> a -> b.
(* Why3 assumption *)
Definition pred1 := (func machine_state bool).
(* Why3 assumption *)
Definition post := (func machine_state (func machine_state bool)).
(* Why3 assumption *)
Inductive codespec :=
| mk_codespec : (list instr) -> (func Z (func machine_state bool)) -> (func
Z (func machine_state (func machine_state bool))) -> codespec.
Axiom codespec_WhyType : WhyType codespec.
Existing Instance codespec_WhyType.
(* Why3 assumption *)
Definition post1 (v:codespec): (func Z (func machine_state (func
machine_state bool))) := match v with
| (mk_codespec x x1 x2) => x2
end.
(* Why3 assumption *)
Definition pre (v:codespec): (func Z (func machine_state bool)) :=
match v with
| (mk_codespec x x1 x2) => x1
end.
(* Why3 assumption *)
Definition code1 (v:codespec): (list instr) :=
match v with
| (mk_codespec x x1 x2) => x
end.
(* Why3 assumption *)
Inductive wp :=
| mk_wp : (list instr) -> (func Z (func (func machine_state bool) (func
machine_state bool))) -> wp.
Axiom wp_WhyType : WhyType wp.
Existing Instance wp_WhyType.
(* Why3 assumption *)
Definition wp1 (v:wp): (func Z (func (func machine_state bool) (func
machine_state bool))) := match v with
| (mk_wp x x1) => x1
end.
(* Why3 assumption *)
Definition wcode (v:wp): (list instr) := match v with
| (mk_wp x x1) => x
end.
(* Why3 assumption *)
Definition contextual_irrelevance (c:(list instr)) (p:Z) (ms1:machine_state)
(ms2:machine_state): Prop := forall (c_global:(list instr)), (codeseq_at
c_global p c) -> (transition_star c_global ms1 ms2).
(* Why3 assumption *)
Definition total_correctness (cs:codespec): Prop := forall (p:Z)
(ms:machine_state), ((infix_at (infix_at (pre cs) p) ms) = true) ->
exists ms':machine_state, ((infix_at (infix_at (infix_at (post1 cs) p) ms)
ms') = true) /\ (contextual_irrelevance (code1 cs) p ms ms').
(* Why3 assumption *)
Definition transformer (code2:wp): Prop := forall (p:Z) (post2:(func
machine_state bool)) (ms:machine_state),
((infix_at (infix_at (infix_at (wp1 code2) p) post2) ms) = true) ->
exists ms':machine_state, ((infix_at post2 ms') = true) /\
(contextual_irrelevance (wcode code2) p ms ms').
Parameter seq_wp: wp -> wp -> (func Z (func (func machine_state bool) (func
machine_state bool))).
Axiom seq_wp_def : forall (s1:wp) (s2:wp) (p:Z) (q:(func machine_state
bool)), ((infix_at (infix_at (seq_wp s1 s2) p)
q) = (infix_at (infix_at (wp1 s1) p) (infix_at (infix_at (wp1 s2)
(p + (list.Length.length (wcode s1)))%Z) q))).
(* Why3 goal *)
Theorem WP_parameter_seq : forall (s1:(list instr)) (s11:(func Z (func (func
machine_state bool) (func machine_state bool)))) (s2:(list instr))
(s21:(func Z (func (func machine_state bool) (func machine_state bool)))),
let s22 := (mk_wp s2 s21) in let s12 := (mk_wp s1 s11) in (((transformer
s12) /\ (transformer s22)) -> forall (p:Z) (post2:(func machine_state
bool)) (ms:machine_state), ((infix_at (infix_at (infix_at (seq_wp s12 s22)
p) post2) ms) = true) -> exists ms':machine_state, ((infix_at post2
ms') = true) /\ (contextual_irrelevance (Init.Datatypes.app s1 s2) p ms
ms')).
intros s1 s11 s2 s21 s22 s12 (h1,h2) p post2 ms h3.
unfold transformer in *.
specialize (h1
p
(infix_at (infix_at (wp1 s22) (p + (list.Length.length (wcode s12)))%Z) post2)
ms).
rewrite seq_wp_def in h3.
apply h1 in h3.
destruct h3 as [ms' [h3 h4]].
specialize (h2 (p + (list.Length.length (wcode s12)))%Z post2 ms').
apply h2 in h3.
destruct h3 as [ms'' [h5 h6]].
exists ms''.