(*
* Vericert: Verified high-level synthesis.
* Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
*
* This program is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as published by
* the Free Software Foundation, either version 3 of the License, or
* (at your option) any later version.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
From compcert Require Import Smallstep Linking Integers Globalenvs.
From vericert Require HTL.
From vericert Require Import Vericertlib Veriloggen Verilog ValueInt AssocMap.
Require Import Lia.
Local Open Scope assocmap.
Definition match_prog (prog : HTL.program) (tprog : Verilog.program) :=
match_program (fun cu f tf => tf = transl_fundef f) eq prog tprog.
Lemma transf_program_match :
forall prog , match_prog prog (transl_program prog).forall prog : HTL.program,
match_prog prog (transl_program prog)
Proof .forall prog : HTL.program,
match_prog prog (transl_program prog)
intros .match_prog prog (transl_program prog)
eapply match_transform_program_contextual.forall f : AST.fundef HTL.module,
transl_fundef f = transl_fundef f
auto .
Qed .
Inductive match_stacks : list HTL.stackframe -> list stackframe -> Prop :=
| match_stack :
forall res m pc reg_assoc arr_assoc hstk vstk ,
match_stacks hstk vstk ->
match_stacks (HTL.Stackframe res m pc reg_assoc arr_assoc :: hstk)
(Stackframe res (transl_module m) pc
reg_assoc arr_assoc :: vstk)
| match_stack_nil : match_stacks nil nil.
Inductive match_states : HTL.state -> state -> Prop :=
| match_state :
forall m st reg_assoc arr_assoc hstk vstk ,
match_stacks hstk vstk ->
match_states (HTL.State hstk m st reg_assoc arr_assoc)
(State vstk (transl_module m) st reg_assoc arr_assoc)
| match_returnstate :
forall v hstk vstk ,
match_stacks hstk vstk ->
match_states (HTL.Returnstate hstk v) (Returnstate vstk v)
| match_initial_call :
forall m ,
match_states (HTL.Callstate nil m nil) (Callstate nil (transl_module m) nil).
Lemma Vlit_inj :
forall a b , Vlit a = Vlit b -> a = b.forall a b : value, Vlit a = Vlit b -> a = b
Proof .forall a b : value, Vlit a = Vlit b -> a = b
inversion 1 .a, b : value
H : Vlit a = Vlit b
H1 : a = b
b = b
trivial . Qed .
Lemma posToValue_inj :
forall a b ,
0 <= Z.pos a <= Int.max_unsigned ->
0 <= Z.pos b <= Int.max_unsigned ->
posToValue a = posToValue b ->
a = b.forall a b : positive,
0 <= Z.pos a <= Int.max_unsigned ->
0 <= Z.pos b <= Int.max_unsigned ->
posToValue a = posToValue b -> a = b
Proof .forall a b : positive,
0 <= Z.pos a <= Int.max_unsigned ->
0 <= Z.pos b <= Int.max_unsigned ->
posToValue a = posToValue b -> a = b
intros .a, b : positive
H : 0 <= Z.pos a <= Int.max_unsigned
H0 : 0 <= Z.pos b <= Int.max_unsigned
H1 : posToValue a = posToValue b
a = b
rewrite <- Pos2Z.id at 1 .a, b : positive
H : 0 <= Z.pos a <= Int.max_unsigned
H0 : 0 <= Z.pos b <= Int.max_unsigned
H1 : posToValue a = posToValue b
Z.to_pos (Z.pos a) = b
rewrite <- Pos2Z.id.a, b : positive
H : 0 <= Z.pos a <= Int.max_unsigned
H0 : 0 <= Z.pos b <= Int.max_unsigned
H1 : posToValue a = posToValue b
Z.to_pos (Z.pos a) = Z.to_pos (Z.pos b)
rewrite <- Int.unsigned_repr at 1 ; try assumption .a, b : positive
H : 0 <= Z.pos a <= Int.max_unsigned
H0 : 0 <= Z.pos b <= Int.max_unsigned
H1 : posToValue a = posToValue b
Z.to_pos (Int.unsigned (Int.repr (Z.pos a))) =
Z.to_pos (Z.pos b)
symmetry .a, b : positive
H : 0 <= Z.pos a <= Int.max_unsigned
H0 : 0 <= Z.pos b <= Int.max_unsigned
H1 : posToValue a = posToValue b
Z.to_pos (Z.pos b) =
Z.to_pos (Int.unsigned (Int.repr (Z.pos a)))
rewrite <- Int.unsigned_repr at 1 ; try assumption .a, b : positive
H : 0 <= Z.pos a <= Int.max_unsigned
H0 : 0 <= Z.pos b <= Int.max_unsigned
H1 : posToValue a = posToValue b
Z.to_pos (Int.unsigned (Int.repr (Z.pos b))) =
Z.to_pos (Int.unsigned (Int.repr (Z.pos a)))
unfold posToValue in *.a, b : positive
H : 0 <= Z.pos a <= Int.max_unsigned
H0 : 0 <= Z.pos b <= Int.max_unsigned
H1 : Int.repr (Z.pos a) = Int.repr (Z.pos b)
Z.to_pos (Int.unsigned (Int.repr (Z.pos b))) =
Z.to_pos (Int.unsigned (Int.repr (Z.pos a)))
rewrite H1; auto .
Qed .
Lemma valueToPos_inj :
forall a b ,
0 < Int.unsigned a ->
0 < Int.unsigned b ->
valueToPos a = valueToPos b ->
a = b.forall a b : int,
0 < Int.unsigned a ->
0 < Int.unsigned b ->
valueToPos a = valueToPos b -> a = b
Proof .forall a b : int,
0 < Int.unsigned a ->
0 < Int.unsigned b ->
valueToPos a = valueToPos b -> a = b
intros .a, b : int
H : 0 < Int.unsigned a
H0 : 0 < Int.unsigned b
H1 : valueToPos a = valueToPos b
a = b
unfold valueToPos in *.a, b : int
H : 0 < Int.unsigned a
H0 : 0 < Int.unsigned b
H1 : Z.to_pos (Int.unsigned a) =
Z.to_pos (Int.unsigned b)
a = b
rewrite <- Int.repr_unsigned at 1 .a, b : int
H : 0 < Int.unsigned a
H0 : 0 < Int.unsigned b
H1 : Z.to_pos (Int.unsigned a) =
Z.to_pos (Int.unsigned b)
Int.repr (Int.unsigned a) = b
rewrite <- Int.repr_unsigned.a, b : int
H : 0 < Int.unsigned a
H0 : 0 < Int.unsigned b
H1 : Z.to_pos (Int.unsigned a) =
Z.to_pos (Int.unsigned b)
Int.repr (Int.unsigned a) = Int.repr (Int.unsigned b)
apply Pos2Z.inj_iff in H1.a, b : int
H : 0 < Int.unsigned a
H0 : 0 < Int.unsigned b
H1 : Z.pos (Z.to_pos (Int.unsigned a)) =
Z.pos (Z.to_pos (Int.unsigned b))
Int.repr (Int.unsigned a) = Int.repr (Int.unsigned b)
rewrite Z2Pos.id in H1; auto .a, b : int
H : 0 < Int.unsigned a
H0 : 0 < Int.unsigned b
H1 : Int.unsigned a =
Z.pos (Z.to_pos (Int.unsigned b))
Int.repr (Int.unsigned a) = Int.repr (Int.unsigned b)
rewrite Z2Pos.id in H1; auto .a, b : int
H : 0 < Int.unsigned a
H0 : 0 < Int.unsigned b
H1 : Int.unsigned a = Int.unsigned b
Int.repr (Int.unsigned a) = Int.repr (Int.unsigned b)
rewrite H1.a, b : int
H : 0 < Int.unsigned a
H0 : 0 < Int.unsigned b
H1 : Int.unsigned a = Int.unsigned b
Int.repr (Int.unsigned b) = Int.repr (Int.unsigned b)
auto .
Qed .
Lemma unsigned_posToValue_le :
forall p ,
Z.pos p <= Int.max_unsigned ->
0 < Int.unsigned (posToValue p).forall p : positive,
Z.pos p <= Int.max_unsigned ->
0 < Int.unsigned (posToValue p)
Proof .forall p : positive,
Z.pos p <= Int.max_unsigned ->
0 < Int.unsigned (posToValue p)
intros .p : positive
H : Z.pos p <= Int.max_unsigned
0 < Int.unsigned (posToValue p)
unfold posToValue.p : positive
H : Z.pos p <= Int.max_unsigned
0 < Int.unsigned (Int.repr (Z.pos p))
rewrite Int.unsigned_repr; lia .
Qed .
Lemma transl_list_fun_fst :
forall p1 p2 a b ,
0 <= Z.pos p1 <= Int.max_unsigned ->
0 <= Z.pos p2 <= Int.max_unsigned ->
transl_list_fun (p1, a) = transl_list_fun (p2, b) ->
(p1, a) = (p2, b).forall (p1 p2 : positive) (a b : stmnt),
0 <= Z.pos p1 <= Int.max_unsigned ->
0 <= Z.pos p2 <= Int.max_unsigned ->
transl_list_fun (p1, a) = transl_list_fun (p2, b) ->
(p1, a) = (p2, b)
Proof .forall (p1 p2 : positive) (a b : stmnt),
0 <= Z.pos p1 <= Int.max_unsigned ->
0 <= Z.pos p2 <= Int.max_unsigned ->
transl_list_fun (p1, a) = transl_list_fun (p2, b) ->
(p1, a) = (p2, b)
intros .p1, p2 : positive
a, b : stmnt
H : 0 <= Z.pos p1 <= Int.max_unsigned
H0 : 0 <= Z.pos p2 <= Int.max_unsigned
H1 : transl_list_fun (p1, a) = transl_list_fun (p2, b)
(p1, a) = (p2, b)
unfold transl_list_fun in H1.p1, p2 : positive
a, b : stmnt
H : 0 <= Z.pos p1 <= Int.max_unsigned
H0 : 0 <= Z.pos p2 <= Int.max_unsigned
H1 : (Vlit (posToValue p1), a) =
(Vlit (posToValue p2), b)
(p1, a) = (p2, b)
apply pair_equal_spec in H1.p1, p2 : positive
a, b : stmnt
H : 0 <= Z.pos p1 <= Int.max_unsigned
H0 : 0 <= Z.pos p2 <= Int.max_unsigned
H1 : Vlit (posToValue p1) = Vlit (posToValue p2) /\
a = b
(p1, a) = (p2, b)
destruct H1.p1, p2 : positive
a, b : stmnt
H : 0 <= Z.pos p1 <= Int.max_unsigned
H0 : 0 <= Z.pos p2 <= Int.max_unsigned
H1 : Vlit (posToValue p1) = Vlit (posToValue p2)
H2 : a = b
(p1, a) = (p2, b)
rewrite H2.p1, p2 : positive
a, b : stmnt
H : 0 <= Z.pos p1 <= Int.max_unsigned
H0 : 0 <= Z.pos p2 <= Int.max_unsigned
H1 : Vlit (posToValue p1) = Vlit (posToValue p2)
H2 : a = b
(p1, b) = (p2, b)
apply Vlit_inj in H1.p1, p2 : positive
a, b : stmnt
H : 0 <= Z.pos p1 <= Int.max_unsigned
H0 : 0 <= Z.pos p2 <= Int.max_unsigned
H1 : posToValue p1 = posToValue p2
H2 : a = b
(p1, b) = (p2, b)
apply posToValue_inj in H1; try assumption .p1, p2 : positive
a, b : stmnt
H : 0 <= Z.pos p1 <= Int.max_unsigned
H0 : 0 <= Z.pos p2 <= Int.max_unsigned
H1 : p1 = p2
H2 : a = b
(p1, b) = (p2, b)
rewrite H1; auto .
Qed .
Lemma Zle_relax :
forall p q r ,
p < q <= r ->
p <= q <= r.forall p q r : Z, p < q <= r -> p <= q <= r
Proof .forall p q r : Z, p < q <= r -> p <= q <= r
lia . Qed .
Hint Resolve Zle_relax : verilogproof.
Lemma transl_in :
forall l p ,
0 <= Z.pos p <= Int.max_unsigned ->
(forall p0 , In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) ->
In p (map fst l).forall (l : list (positive * stmnt)) (p : positive),
0 <= Z.pos p <= Int.max_unsigned ->
(forall p0 : positive,
In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
In (Vlit (posToValue p))
(map fst (map transl_list_fun l)) ->
In p (map fst l)
Proof .forall (l : list (positive * stmnt)) (p : positive),
0 <= Z.pos p <= Int.max_unsigned ->
(forall p0 : positive,
In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
In (Vlit (posToValue p))
(map fst (map transl_list_fun l)) ->
In p (map fst l)
induction l.forall p : positive,
0 <= Z.pos p <= Int.max_unsigned ->
(forall p0 : positive,
In p0 (map fst nil) ->
0 < Z.pos p0 <= Int.max_unsigned) ->
In (Vlit (posToValue p))
(map fst (map transl_list_fun nil)) ->
In p (map fst nil)
- forall p : positive,
0 <= Z.pos p <= Int.max_unsigned ->
(forall p0 : positive,
In p0 (map fst nil) ->
0 < Z.pos p0 <= Int.max_unsigned) ->
In (Vlit (posToValue p))
(map fst (map transl_list_fun nil)) ->
In p (map fst nil)
simplify. p : positive
H0 : forall p0 : positive,
False -> 0 < Z.pos p0 <= 4294967295
H1 : False
H2 : 0 <= Z.pos p
H3 : Z.pos p <= 4294967295
False
auto .
- a : (positive * stmnt)%type
l : list (positive * stmnt)
IHl : forall p : positive,
0 <= Z.pos p <= Int.max_unsigned ->
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) ->
In p (map fst l)
forall p : positive,
0 <= Z.pos p <= Int.max_unsigned ->
(forall p0 : positive,
In p0 (map fst (a :: l)) ->
0 < Z.pos p0 <= Int.max_unsigned) ->
In (Vlit (posToValue p))
(map fst (map transl_list_fun (a :: l))) ->
In p (map fst (a :: l))
intros .a : (positive * stmnt)%type
l : list (positive * stmnt)
IHl : forall p : positive,
0 <= Z.pos p <= Int.max_unsigned ->
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) ->
In p (map fst l)
p : positive
H : 0 <= Z.pos p <= Int.max_unsigned
H0 : forall p0 : positive,
In p0 (map fst (a :: l)) ->
0 < Z.pos p0 <= Int.max_unsigned
H1 : In (Vlit (posToValue p))
(map fst (map transl_list_fun (a :: l)))
In p (map fst (a :: l))
destruct a.p0 : positive
s : stmnt
l : list (positive * stmnt)
IHl : forall p : positive,
0 <= Z.pos p <= Int.max_unsigned ->
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) ->
In p (map fst l)
p : positive
H : 0 <= Z.pos p <= Int.max_unsigned
H0 : forall p1 : positive,
In p1 (map fst ((p0, s) :: l)) ->
0 < Z.pos p1 <= Int.max_unsigned
H1 : In (Vlit (posToValue p))
(map fst (map transl_list_fun ((p0, s) :: l)))
In p (map fst ((p0, s) :: l))
simplify. p0 : positive
s : stmnt
l : list (positive * stmnt)
IHl : forall p : positive,
0 <= Z.pos p <= 4294967295 ->
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) ->
In p (map fst l)
p : positive
H0 : forall p1 : positive,
p0 = p1 \/ In p1 (map fst l) ->
0 < Z.pos p1 <= 4294967295
H1 : Vlit (posToValue p0) = Vlit (posToValue p) \/
In (Vlit (posToValue p))
(map fst (map transl_list_fun l))
H2 : 0 <= Z.pos p
H3 : Z.pos p <= 4294967295
p0 = p \/ In p (map fst l)
destruct (peq p0 p); auto .p0 : positive
s : stmnt
l : list (positive * stmnt)
IHl : forall p : positive,
0 <= Z.pos p <= 4294967295 ->
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) ->
In p (map fst l)
p : positive
H0 : forall p1 : positive,
p0 = p1 \/ In p1 (map fst l) ->
0 < Z.pos p1 <= 4294967295
H1 : Vlit (posToValue p0) = Vlit (posToValue p) \/
In (Vlit (posToValue p))
(map fst (map transl_list_fun l))
H2 : 0 <= Z.pos p
H3 : Z.pos p <= 4294967295
n : p0 <> p
p0 = p \/ In p (map fst l)
right .p0 : positive
s : stmnt
l : list (positive * stmnt)
IHl : forall p : positive,
0 <= Z.pos p <= 4294967295 ->
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) ->
In p (map fst l)
p : positive
H0 : forall p1 : positive,
p0 = p1 \/ In p1 (map fst l) ->
0 < Z.pos p1 <= 4294967295
H1 : Vlit (posToValue p0) = Vlit (posToValue p) \/
In (Vlit (posToValue p))
(map fst (map transl_list_fun l))
H2 : 0 <= Z.pos p
H3 : Z.pos p <= 4294967295
n : p0 <> p
In p (map fst l)
inv H1. p0 : positive
s : stmnt
l : list (positive * stmnt)
IHl : forall p : positive,
0 <= Z.pos p <= 4294967295 ->
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) ->
In p (map fst l)
p : positive
H0 : forall p1 : positive,
p0 = p1 \/ In p1 (map fst l) ->
0 < Z.pos p1 <= 4294967295
H2 : 0 <= Z.pos p
H3 : Z.pos p <= 4294967295
n : p0 <> p
H : Vlit (posToValue p0) = Vlit (posToValue p)
In p (map fst l)
apply Vlit_inj in H.p0 : positive
s : stmnt
l : list (positive * stmnt)
IHl : forall p : positive,
0 <= Z.pos p <= 4294967295 ->
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) ->
In p (map fst l)
p : positive
H0 : forall p1 : positive,
p0 = p1 \/ In p1 (map fst l) ->
0 < Z.pos p1 <= 4294967295
H2 : 0 <= Z.pos p
H3 : Z.pos p <= 4294967295
n : p0 <> p
H : posToValue p0 = posToValue p
In p (map fst l)
apply posToValue_inj in H; auto .p0 : positive
s : stmnt
l : list (positive * stmnt)
IHl : forall p : positive,
0 <= Z.pos p <= 4294967295 ->
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) ->
In p (map fst l)
p : positive
H0 : forall p1 : positive,
p0 = p1 \/ In p1 (map fst l) ->
0 < Z.pos p1 <= 4294967295
H2 : 0 <= Z.pos p
H3 : Z.pos p <= 4294967295
n : p0 <> p
H : p0 = p
In p (map fst l)
contradiction .p0 : positive
s : stmnt
l : list (positive * stmnt)
IHl : forall p : positive,
0 <= Z.pos p <= 4294967295 ->
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) ->
In p (map fst l)
p : positive
H0 : forall p1 : positive,
p0 = p1 \/ In p1 (map fst l) ->
0 < Z.pos p1 <= 4294967295
H2 : 0 <= Z.pos p
H3 : Z.pos p <= 4294967295
n : p0 <> p
H : posToValue p0 = posToValue p
0 <= Z.pos p0 <= Int.max_unsigned
auto with verilogproof.p0 : positive
s : stmnt
l : list (positive * stmnt)
IHl : forall p : positive,
0 <= Z.pos p <= 4294967295 ->
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) ->
In p (map fst l)
p : positive
H0 : forall p1 : positive,
p0 = p1 \/ In p1 (map fst l) ->
0 < Z.pos p1 <= 4294967295
H2 : 0 <= Z.pos p
H3 : Z.pos p <= 4294967295
n : p0 <> p
H : In (Vlit (posToValue p))
(map fst (map transl_list_fun l))
In p (map fst l)
apply IHl; auto .
Qed .
Lemma transl_notin :
forall l p ,
0 <= Z.pos p <= Int.max_unsigned ->
(forall p0 , In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
~ In p (List.map fst l) -> ~ In (Vlit (posToValue p)) (List.map fst (transl_list l)).forall (l : list (positive * stmnt)) (p : positive),
0 <= Z.pos p <= Int.max_unsigned ->
(forall p0 : positive,
In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
~ In p (map fst l) ->
~ In (Vlit (posToValue p)) (map fst (transl_list l))
Proof .forall (l : list (positive * stmnt)) (p : positive),
0 <= Z.pos p <= Int.max_unsigned ->
(forall p0 : positive,
In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
~ In p (map fst l) ->
~ In (Vlit (posToValue p)) (map fst (transl_list l))
induction l; auto .a : (positive * stmnt)%type
l : list (positive * stmnt)
IHl : forall p : positive,
0 <= Z.pos p <= Int.max_unsigned ->
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
~ In p (map fst l) -> ~ In (Vlit (posToValue p)) (map fst (transl_list l))
forall p : positive,
0 <= Z.pos p <= Int.max_unsigned ->
(forall p0 : positive,
In p0 (map fst (a :: l)) ->
0 < Z.pos p0 <= Int.max_unsigned) ->
~ In p (map fst (a :: l)) ->
~
In (Vlit (posToValue p))
(map fst (transl_list (a :: l)))
intros .a : (positive * stmnt)%type
l : list (positive * stmnt)
IHl : forall p : positive,
0 <= Z.pos p <= Int.max_unsigned ->
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
~ In p (map fst l) -> ~ In (Vlit (posToValue p)) (map fst (transl_list l))
p : positive
H : 0 <= Z.pos p <= Int.max_unsigned
H0 : forall p0 : positive,
In p0 (map fst (a :: l)) ->
0 < Z.pos p0 <= Int.max_unsigned
H1 : ~ In p (map fst (a :: l))
~
In (Vlit (posToValue p))
(map fst (transl_list (a :: l)))
destruct a.p0 : positive
s : stmnt
l : list (positive * stmnt)
IHl : forall p : positive,
0 <= Z.pos p <= Int.max_unsigned ->
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
~ In p (map fst l) -> ~ In (Vlit (posToValue p)) (map fst (transl_list l))
p : positive
H : 0 <= Z.pos p <= Int.max_unsigned
H0 : forall p1 : positive,
In p1 (map fst ((p0, s) :: l)) ->
0 < Z.pos p1 <= Int.max_unsigned
H1 : ~ In p (map fst ((p0, s) :: l))
~
In (Vlit (posToValue p))
(map fst (transl_list ((p0, s) :: l)))
unfold not in *.p0 : positive
s : stmnt
l : list (positive * stmnt)
IHl : forall p : positive,
0 <= Z.pos p <= Int.max_unsigned ->
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
(In p (map fst l) -> False ) ->
In (Vlit (posToValue p)) (map fst (transl_list l)) -> False
p : positive
H : 0 <= Z.pos p <= Int.max_unsigned
H0 : forall p1 : positive,
In p1 (map fst ((p0, s) :: l)) ->
0 < Z.pos p1 <= Int.max_unsigned
H1 : In p (map fst ((p0, s) :: l)) -> False
In (Vlit (posToValue p))
(map fst (transl_list ((p0, s) :: l))) -> False
intros .p0 : positive
s : stmnt
l : list (positive * stmnt)
IHl : forall p : positive,
0 <= Z.pos p <= Int.max_unsigned ->
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
(In p (map fst l) -> False ) ->
In (Vlit (posToValue p)) (map fst (transl_list l)) -> False
p : positive
H : 0 <= Z.pos p <= Int.max_unsigned
H0 : forall p1 : positive,
In p1 (map fst ((p0, s) :: l)) ->
0 < Z.pos p1 <= Int.max_unsigned
H1 : In p (map fst ((p0, s) :: l)) -> False
H2 : In (Vlit (posToValue p))
(map fst (transl_list ((p0, s) :: l)))
False
simplify. p0 : positive
s : stmnt
l : list (positive * stmnt)
IHl : forall p : positive,
0 <= Z.pos p <= 4294967295 ->
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
(In p (map fst l) -> False ) ->
In (Vlit (posToValue p)) (map fst (transl_list l)) -> False
p : positive
H0 : forall p1 : positive,
p0 = p1 \/ In p1 (map fst l) ->
0 < Z.pos p1 <= 4294967295
H1 : p0 = p \/ In p (map fst l) -> False
H2 : Vlit (posToValue p0) = Vlit (posToValue p) \/
In (Vlit (posToValue p))
(map fst (transl_list l))
H3 : 0 <= Z.pos p
H4 : Z.pos p <= 4294967295
False
destruct (peq p0 p).p0 : positive
s : stmnt
l : list (positive * stmnt)
IHl : forall p : positive,
0 <= Z.pos p <= 4294967295 ->
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
(In p (map fst l) -> False ) ->
In (Vlit (posToValue p)) (map fst (transl_list l)) -> False
p : positive
H0 : forall p1 : positive,
p0 = p1 \/ In p1 (map fst l) ->
0 < Z.pos p1 <= 4294967295
H1 : p0 = p \/ In p (map fst l) -> False
H2 : Vlit (posToValue p0) = Vlit (posToValue p) \/
In (Vlit (posToValue p))
(map fst (transl_list l))
H3 : 0 <= Z.pos p
H4 : Z.pos p <= 4294967295
e : p0 = p
False
apply H1.p0 : positive
s : stmnt
l : list (positive * stmnt)
IHl : forall p : positive,
0 <= Z.pos p <= 4294967295 ->
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
(In p (map fst l) -> False ) ->
In (Vlit (posToValue p)) (map fst (transl_list l)) -> False
p : positive
H0 : forall p1 : positive,
p0 = p1 \/ In p1 (map fst l) ->
0 < Z.pos p1 <= 4294967295
H1 : p0 = p \/ In p (map fst l) -> False
H2 : Vlit (posToValue p0) = Vlit (posToValue p) \/
In (Vlit (posToValue p))
(map fst (transl_list l))
H3 : 0 <= Z.pos p
H4 : Z.pos p <= 4294967295
e : p0 = p
p0 = p \/ In p (map fst l)
auto .p0 : positive
s : stmnt
l : list (positive * stmnt)
IHl : forall p : positive,
0 <= Z.pos p <= 4294967295 ->
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
(In p (map fst l) -> False ) ->
In (Vlit (posToValue p)) (map fst (transl_list l)) -> False
p : positive
H0 : forall p1 : positive,
p0 = p1 \/ In p1 (map fst l) ->
0 < Z.pos p1 <= 4294967295
H1 : p0 = p \/ In p (map fst l) -> False
H2 : Vlit (posToValue p0) = Vlit (posToValue p) \/
In (Vlit (posToValue p))
(map fst (transl_list l))
H3 : 0 <= Z.pos p
H4 : Z.pos p <= 4294967295
n : p0 <> p
False
apply H1.p0 : positive
s : stmnt
l : list (positive * stmnt)
IHl : forall p : positive,
0 <= Z.pos p <= 4294967295 ->
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
(In p (map fst l) -> False ) ->
In (Vlit (posToValue p)) (map fst (transl_list l)) -> False
p : positive
H0 : forall p1 : positive,
p0 = p1 \/ In p1 (map fst l) ->
0 < Z.pos p1 <= 4294967295
H1 : p0 = p \/ In p (map fst l) -> False
H2 : Vlit (posToValue p0) = Vlit (posToValue p) \/
In (Vlit (posToValue p))
(map fst (transl_list l))
H3 : 0 <= Z.pos p
H4 : Z.pos p <= 4294967295
n : p0 <> p
p0 = p \/ In p (map fst l)
unfold transl_list in *.p0 : positive
s : stmnt
l : list (positive * stmnt)
IHl : forall p : positive,
0 <= Z.pos p <= 4294967295 ->
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
(In p (map fst l) -> False ) ->
In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> False
p : positive
H0 : forall p1 : positive,
p0 = p1 \/ In p1 (map fst l) ->
0 < Z.pos p1 <= 4294967295
H1 : p0 = p \/ In p (map fst l) -> False
H2 : Vlit (posToValue p0) = Vlit (posToValue p) \/
In (Vlit (posToValue p))
(map fst (map transl_list_fun l))
H3 : 0 <= Z.pos p
H4 : Z.pos p <= 4294967295
n : p0 <> p
p0 = p \/ In p (map fst l)
inv H2. p0 : positive
s : stmnt
l : list (positive * stmnt)
IHl : forall p : positive,
0 <= Z.pos p <= 4294967295 ->
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
(In p (map fst l) -> False ) ->
In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> False
p : positive
H0 : forall p1 : positive,
p0 = p1 \/ In p1 (map fst l) ->
0 < Z.pos p1 <= 4294967295
H1 : p0 = p \/ In p (map fst l) -> False
H3 : 0 <= Z.pos p
H4 : Z.pos p <= 4294967295
n : p0 <> p
H : Vlit (posToValue p0) = Vlit (posToValue p)
p0 = p \/ In p (map fst l)
apply Vlit_inj in H.p0 : positive
s : stmnt
l : list (positive * stmnt)
IHl : forall p : positive,
0 <= Z.pos p <= 4294967295 ->
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
(In p (map fst l) -> False ) ->
In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> False
p : positive
H0 : forall p1 : positive,
p0 = p1 \/ In p1 (map fst l) ->
0 < Z.pos p1 <= 4294967295
H1 : p0 = p \/ In p (map fst l) -> False
H3 : 0 <= Z.pos p
H4 : Z.pos p <= 4294967295
n : p0 <> p
H : posToValue p0 = posToValue p
p0 = p \/ In p (map fst l)
apply posToValue_inj in H.p0 : positive
s : stmnt
l : list (positive * stmnt)
IHl : forall p : positive,
0 <= Z.pos p <= 4294967295 ->
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
(In p (map fst l) -> False ) ->
In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> False
p : positive
H0 : forall p1 : positive,
p0 = p1 \/ In p1 (map fst l) ->
0 < Z.pos p1 <= 4294967295
H1 : p0 = p \/ In p (map fst l) -> False
H3 : 0 <= Z.pos p
H4 : Z.pos p <= 4294967295
n : p0 <> p
H : p0 = p
p0 = p \/ In p (map fst l)
contradiction .p0 : positive
s : stmnt
l : list (positive * stmnt)
IHl : forall p : positive,
0 <= Z.pos p <= 4294967295 ->
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
(In p (map fst l) -> False ) ->
In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> False
p : positive
H0 : forall p1 : positive,
p0 = p1 \/ In p1 (map fst l) ->
0 < Z.pos p1 <= 4294967295
H1 : p0 = p \/ In p (map fst l) -> False
H3 : 0 <= Z.pos p
H4 : Z.pos p <= 4294967295
n : p0 <> p
H : posToValue p0 = posToValue p
0 <= Z.pos p0 <= Int.max_unsigned
auto with verilogproof.p0 : positive
s : stmnt
l : list (positive * stmnt)
IHl : forall p : positive,
0 <= Z.pos p <= 4294967295 ->
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
(In p (map fst l) -> False ) ->
In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> False
p : positive
H0 : forall p1 : positive,
p0 = p1 \/ In p1 (map fst l) ->
0 < Z.pos p1 <= 4294967295
H1 : p0 = p \/ In p (map fst l) -> False
H3 : 0 <= Z.pos p
H4 : Z.pos p <= 4294967295
n : p0 <> p
H : posToValue p0 = posToValue p
0 <= Z.pos p <= Int.max_unsigned
auto .p0 : positive
s : stmnt
l : list (positive * stmnt)
IHl : forall p : positive,
0 <= Z.pos p <= 4294967295 ->
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
(In p (map fst l) -> False ) ->
In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> False
p : positive
H0 : forall p1 : positive,
p0 = p1 \/ In p1 (map fst l) ->
0 < Z.pos p1 <= 4294967295
H1 : p0 = p \/ In p (map fst l) -> False
H3 : 0 <= Z.pos p
H4 : Z.pos p <= 4294967295
n : p0 <> p
H : In (Vlit (posToValue p))
(map fst (map transl_list_fun l))
p0 = p \/ In p (map fst l)
right .p0 : positive
s : stmnt
l : list (positive * stmnt)
IHl : forall p : positive,
0 <= Z.pos p <= 4294967295 ->
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
(In p (map fst l) -> False ) ->
In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> False
p : positive
H0 : forall p1 : positive,
p0 = p1 \/ In p1 (map fst l) ->
0 < Z.pos p1 <= 4294967295
H1 : p0 = p \/ In p (map fst l) -> False
H3 : 0 <= Z.pos p
H4 : Z.pos p <= 4294967295
n : p0 <> p
H : In (Vlit (posToValue p))
(map fst (map transl_list_fun l))
In p (map fst l)
apply transl_in; auto .
Qed .
Lemma transl_norepet :
forall l ,
(forall p0 , In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
list_norepet (List.map fst l) -> list_norepet (List.map fst (transl_list l)).forall l : list (positive * stmnt),
(forall p0 : positive,
In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
list_norepet (map fst l) ->
list_norepet (map fst (transl_list l))
Proof .forall l : list (positive * stmnt),
(forall p0 : positive,
In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
list_norepet (map fst l) ->
list_norepet (map fst (transl_list l))
induction l.(forall p0 : positive,
In p0 (map fst nil) ->
0 < Z.pos p0 <= Int.max_unsigned) ->
list_norepet (map fst nil) ->
list_norepet (map fst (transl_list nil))
- (forall p0 : positive,
In p0 (map fst nil) ->
0 < Z.pos p0 <= Int.max_unsigned) ->
list_norepet (map fst nil) ->
list_norepet (map fst (transl_list nil))
intros .H : forall p0 : positive,
In p0 (map fst nil) ->
0 < Z.pos p0 <= Int.max_unsigned
H0 : list_norepet (map fst nil)
list_norepet (map fst (transl_list nil))
simpl .H : forall p0 : positive,
In p0 (map fst nil) ->
0 < Z.pos p0 <= Int.max_unsigned
H0 : list_norepet (map fst nil)
list_norepet nil
apply list_norepet_nil.
- a : (positive * stmnt)%type
l : list (positive * stmnt)
IHl : (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
(forall p0 : positive,
In p0 (map fst (a :: l)) ->
0 < Z.pos p0 <= Int.max_unsigned) ->
list_norepet (map fst (a :: l)) ->
list_norepet (map fst (transl_list (a :: l)))
destruct a.p : positive
s : stmnt
l : list (positive * stmnt)
IHl : (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
(forall p0 : positive,
In p0 (map fst ((p, s) :: l)) ->
0 < Z.pos p0 <= Int.max_unsigned) ->
list_norepet (map fst ((p, s) :: l)) ->
list_norepet (map fst (transl_list ((p, s) :: l)))
intros .p : positive
s : stmnt
l : list (positive * stmnt)
IHl : (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H : forall p0 : positive,
In p0 (map fst ((p, s) :: l)) ->
0 < Z.pos p0 <= Int.max_unsigned
H0 : list_norepet (map fst ((p, s) :: l))
list_norepet (map fst (transl_list ((p, s) :: l)))
simpl .p : positive
s : stmnt
l : list (positive * stmnt)
IHl : (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H : forall p0 : positive,
In p0 (map fst ((p, s) :: l)) ->
0 < Z.pos p0 <= Int.max_unsigned
H0 : list_norepet (map fst ((p, s) :: l))
list_norepet
(Vlit (posToValue p) :: map fst (transl_list l))
apply list_norepet_cons.p : positive
s : stmnt
l : list (positive * stmnt)
IHl : (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H : forall p0 : positive,
In p0 (map fst ((p, s) :: l)) ->
0 < Z.pos p0 <= Int.max_unsigned
H0 : list_norepet (map fst ((p, s) :: l))
~ In (Vlit (posToValue p)) (map fst (transl_list l))
inv H0. p : positive
s : stmnt
l : list (positive * stmnt)
IHl : (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H : forall p0 : positive,
In p0 (map fst ((p, s) :: l)) ->
0 < Z.pos p0 <= Int.max_unsigned
H3 : ~ In p (map fst l)
H4 : list_norepet (map fst l)
~ In (Vlit (posToValue p)) (map fst (transl_list l))
apply transl_notin.p : positive
s : stmnt
l : list (positive * stmnt)
IHl : (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H : forall p0 : positive,
In p0 (map fst ((p, s) :: l)) ->
0 < Z.pos p0 <= Int.max_unsigned
H3 : ~ In p (map fst l)
H4 : list_norepet (map fst l)
0 <= Z.pos p <= Int.max_unsigned
apply Zle_relax.p : positive
s : stmnt
l : list (positive * stmnt)
IHl : (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H : forall p0 : positive,
In p0 (map fst ((p, s) :: l)) ->
0 < Z.pos p0 <= Int.max_unsigned
H3 : ~ In p (map fst l)
H4 : list_norepet (map fst l)
0 < Z.pos p <= Int.max_unsigned
apply H.p : positive
s : stmnt
l : list (positive * stmnt)
IHl : (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H : forall p0 : positive,
In p0 (map fst ((p, s) :: l)) ->
0 < Z.pos p0 <= Int.max_unsigned
H3 : ~ In p (map fst l)
H4 : list_norepet (map fst l)
In p (map fst ((p, s) :: l))
simplify; auto . p : positive
s : stmnt
l : list (positive * stmnt)
IHl : (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H : forall p0 : positive,
In p0 (map fst ((p, s) :: l)) ->
0 < Z.pos p0 <= Int.max_unsigned
H3 : ~ In p (map fst l)
H4 : list_norepet (map fst l)
forall p0 : positive,
In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned
intros .p : positive
s : stmnt
l : list (positive * stmnt)
IHl : (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H : forall p0 : positive,
In p0 (map fst ((p, s) :: l)) ->
0 < Z.pos p0 <= Int.max_unsigned
H3 : ~ In p (map fst l)
H4 : list_norepet (map fst l)
p0 : positive
H0 : In p0 (map fst l)
0 < Z.pos p0 <= Int.max_unsigned
apply H.p : positive
s : stmnt
l : list (positive * stmnt)
IHl : (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H : forall p0 : positive,
In p0 (map fst ((p, s) :: l)) ->
0 < Z.pos p0 <= Int.max_unsigned
H3 : ~ In p (map fst l)
H4 : list_norepet (map fst l)
p0 : positive
H0 : In p0 (map fst l)
In p0 (map fst ((p, s) :: l))
destruct (peq p0 p); subst ; simplify; auto .p : positive
s : stmnt
l : list (positive * stmnt)
IHl : (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H : forall p0 : positive,
In p0 (map fst ((p, s) :: l)) ->
0 < Z.pos p0 <= Int.max_unsigned
H3 : ~ In p (map fst l)
H4 : list_norepet (map fst l)
~ In p (map fst l)
assumption .p : positive
s : stmnt
l : list (positive * stmnt)
IHl : (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H : forall p0 : positive,
In p0 (map fst ((p, s) :: l)) ->
0 < Z.pos p0 <= Int.max_unsigned
H0 : list_norepet (map fst ((p, s) :: l))
list_norepet (map fst (transl_list l))
apply IHl.p : positive
s : stmnt
l : list (positive * stmnt)
IHl : (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H : forall p0 : positive,
In p0 (map fst ((p, s) :: l)) ->
0 < Z.pos p0 <= Int.max_unsigned
H0 : list_norepet (map fst ((p, s) :: l))
forall p0 : positive,
In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned
intros .p : positive
s : stmnt
l : list (positive * stmnt)
IHl : (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H : forall p0 : positive,
In p0 (map fst ((p, s) :: l)) ->
0 < Z.pos p0 <= Int.max_unsigned
H0 : list_norepet (map fst ((p, s) :: l))
p0 : positive
H1 : In p0 (map fst l)
0 < Z.pos p0 <= Int.max_unsigned
apply H.p : positive
s : stmnt
l : list (positive * stmnt)
IHl : (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H : forall p0 : positive,
In p0 (map fst ((p, s) :: l)) ->
0 < Z.pos p0 <= Int.max_unsigned
H0 : list_norepet (map fst ((p, s) :: l))
p0 : positive
H1 : In p0 (map fst l)
In p0 (map fst ((p, s) :: l))
destruct (peq p0 p); subst ; simplify; auto .p : positive
s : stmnt
l : list (positive * stmnt)
IHl : (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H : forall p0 : positive,
In p0 (map fst ((p, s) :: l)) ->
0 < Z.pos p0 <= Int.max_unsigned
H0 : list_norepet (map fst ((p, s) :: l))
list_norepet (map fst l)
simplify. p : positive
s : stmnt
l : list (positive * stmnt)
IHl : (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H : forall p0 : positive,
p = p0 \/ In p0 (map fst l) ->
0 < Z.pos p0 <= 4294967295
H0 : list_norepet (p :: map fst l)
list_norepet (map fst l)
inv H0. p : positive
s : stmnt
l : list (positive * stmnt)
IHl : (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H : forall p0 : positive,
p = p0 \/ In p0 (map fst l) ->
0 < Z.pos p0 <= 4294967295
H3 : ~ In p (map fst l)
H4 : list_norepet (map fst l)
list_norepet (map fst l)
assumption .
Qed .
Lemma transl_list_correct :
forall l v ev f asr asa asrn asan asr' asa' asrn' asan' ,
(forall p0 , In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
list_norepet (List.map fst l) ->
asr!ev = Some v ->
(forall p s ,
In (p, s) l ->
v = posToValue p ->
stmnt_runp f
{| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |}
s
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
stmnt_runp f
{| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list l) (Some Vskip))
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |}).forall (l : list (positive * stmnt)) (v : value)
(ev : positive) (f : fext) (asr : AssocMap.t value)
(asa : AssocMap.t arr) (asrn : AssocMap.t value)
(asan : AssocMap.t arr) (asr' : AssocMap.t value)
(asa' : AssocMap.t arr) (asrn' : AssocMap.t value)
(asan' : AssocMap.t arr),
(forall p0 : positive,
In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
list_norepet (map fst l) ->
asr ! ev = Some v ->
forall (p : positive) (s : stmnt),
In (p, s) l ->
v = posToValue p ->
stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |} ->
stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list l) (Some Vskip))
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
Proof .forall (l : list (positive * stmnt)) (v : value)
(ev : positive) (f : fext) (asr : AssocMap.t value)
(asa : AssocMap.t arr) (asrn : AssocMap.t value)
(asan : AssocMap.t arr) (asr' : AssocMap.t value)
(asa' : AssocMap.t arr) (asrn' : AssocMap.t value)
(asan' : AssocMap.t arr),
(forall p0 : positive,
In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
list_norepet (map fst l) ->
asr ! ev = Some v ->
forall (p : positive) (s : stmnt),
In (p, s) l ->
v = posToValue p ->
stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |} ->
stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list l) (Some Vskip))
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
induction l as [| a l IHl].forall (v : value) (ev : positive) (f : fext)
(asr : AssocMap.t value) (asa : AssocMap.t arr)
(asrn : AssocMap.t value) (asan : AssocMap.t arr)
(asr' : AssocMap.t value) (asa' : AssocMap.t arr)
(asrn' : AssocMap.t value) (asan' : AssocMap.t arr),
(forall p0 : positive,
In p0 (map fst nil) ->
0 < Z.pos p0 <= Int.max_unsigned) ->
list_norepet (map fst nil) ->
asr ! ev = Some v ->
forall (p : positive) (s : stmnt),
In (p, s) nil ->
v = posToValue p ->
stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |} ->
stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list nil) (Some Vskip))
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
- forall (v : value) (ev : positive) (f : fext)
(asr : AssocMap.t value) (asa : AssocMap.t arr)
(asrn : AssocMap.t value) (asan : AssocMap.t arr)
(asr' : AssocMap.t value) (asa' : AssocMap.t arr)
(asrn' : AssocMap.t value) (asan' : AssocMap.t arr),
(forall p0 : positive,
In p0 (map fst nil) ->
0 < Z.pos p0 <= Int.max_unsigned) ->
list_norepet (map fst nil) ->
asr ! ev = Some v ->
forall (p : positive) (s : stmnt),
In (p, s) nil ->
v = posToValue p ->
stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |} ->
stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list nil) (Some Vskip))
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
contradiction .
- a : (positive * stmnt)%type
l : list (positive * stmnt)
IHl : forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value)
(asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr)
(asr' : AssocMap.t value) (asa' : AssocMap.t arr)
(asrn' : AssocMap.t value) (asan' : AssocMap.t arr),
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
list_norepet (map fst l) ->
asr ! ev = Some v ->
forall (p : positive) (s : stmnt),
In (p, s) l ->
v = posToValue p ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |} s
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list l) (Some Vskip))
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |}
forall (v : value) (ev : positive) (f : fext)
(asr : AssocMap.t value) (asa : AssocMap.t arr)
(asrn : AssocMap.t value) (asan : AssocMap.t arr)
(asr' : AssocMap.t value) (asa' : AssocMap.t arr)
(asrn' : AssocMap.t value) (asan' : AssocMap.t arr),
(forall p0 : positive,
In p0 (map fst (a :: l)) ->
0 < Z.pos p0 <= Int.max_unsigned) ->
list_norepet (map fst (a :: l)) ->
asr ! ev = Some v ->
forall (p : positive) (s : stmnt),
In (p, s) (a :: l) ->
v = posToValue p ->
stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |} ->
stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list (a :: l)) (Some Vskip))
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
intros v ev f asr asa asrn asan asr' asa' asrn' asan' BOUND NOREP ASSOC p s IN EQ SRUN.a : (positive * stmnt)%type
l : list (positive * stmnt)
IHl : forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value)
(asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr)
(asr' : AssocMap.t value) (asa' : AssocMap.t arr)
(asrn' : AssocMap.t value) (asan' : AssocMap.t arr),
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
list_norepet (map fst l) ->
asr ! ev = Some v ->
forall (p : positive) (s : stmnt),
In (p, s) l ->
v = posToValue p ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |} s
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list l) (Some Vskip))
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |}
v : value
ev : positive
f : fext
asr : AssocMap.t value
asa : AssocMap.t arr
asrn : AssocMap.t value
asan : AssocMap.t arr
asr' : AssocMap.t value
asa' : AssocMap.t arr
asrn' : AssocMap.t value
asan' : AssocMap.t arr
BOUND : forall p0 : positive,
In p0 (map fst (a :: l)) ->
0 < Z.pos p0 <= Int.max_unsigned
NOREP : list_norepet (map fst (a :: l))
ASSOC : asr ! ev = Some v
p : positive
s : stmnt
IN : In (p, s) (a :: l)
EQ : v = posToValue p
SRUN : stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list (a :: l)) (Some Vskip))
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
destruct a as [p' s'].p' : positive
s' : stmnt
l : list (positive * stmnt)
IHl : forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value)
(asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr)
(asr' : AssocMap.t value) (asa' : AssocMap.t arr)
(asrn' : AssocMap.t value) (asan' : AssocMap.t arr),
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
list_norepet (map fst l) ->
asr ! ev = Some v ->
forall (p : positive) (s : stmnt),
In (p, s) l ->
v = posToValue p ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |} s
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list l) (Some Vskip))
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |}
v : value
ev : positive
f : fext
asr : AssocMap.t value
asa : AssocMap.t arr
asrn : AssocMap.t value
asan : AssocMap.t arr
asr' : AssocMap.t value
asa' : AssocMap.t arr
asrn' : AssocMap.t value
asan' : AssocMap.t arr
BOUND : forall p0 : positive,
In p0 (map fst ((p', s') :: l)) ->
0 < Z.pos p0 <= Int.max_unsigned
NOREP : list_norepet (map fst ((p', s') :: l))
ASSOC : asr ! ev = Some v
p : positive
s : stmnt
IN : In (p, s) ((p', s') :: l)
EQ : v = posToValue p
SRUN : stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list ((p', s') :: l))
(Some Vskip))
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
simplify. p' : positive
s' : stmnt
l : list (positive * stmnt)
IHl : forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value)
(asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr)
(asr' : AssocMap.t value) (asa' : AssocMap.t arr)
(asrn' : AssocMap.t value) (asan' : AssocMap.t arr),
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
list_norepet (map fst l) ->
asr ! ev = Some v ->
forall (p : positive) (s : stmnt),
In (p, s) l ->
v = posToValue p ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |} s
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list l) (Some Vskip))
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |}
v : value
ev : positive
f : fext
asr : AssocMap.t value
asa : AssocMap.t arr
asrn : AssocMap.t value
asan : AssocMap.t arr
asr' : AssocMap.t value
asa' : AssocMap.t arr
asrn' : AssocMap.t value
asan' : AssocMap.t arr
BOUND : forall p0 : positive,
p' = p0 \/ In p0 (map fst l) ->
0 < Z.pos p0 <= 4294967295
NOREP : list_norepet (p' :: map fst l)
ASSOC : asr ! ev = Some v
p : positive
s : stmnt
IN : (p', s') = (p, s) \/ In (p, s) l
EQ : v = posToValue p
SRUN : stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |}
(Vcase (Vvar ev)
((Vlit (posToValue p'), s') :: transl_list l)
(Some Vskip))
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
destruct (peq p p'); subst .p' : positive
s' : stmnt
l : list (positive * stmnt)
IHl : forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value)
(asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr)
(asr' : AssocMap.t value) (asa' : AssocMap.t arr)
(asrn' : AssocMap.t value) (asan' : AssocMap.t arr),
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
list_norepet (map fst l) ->
asr ! ev = Some v ->
forall (p : positive) (s : stmnt),
In (p, s) l ->
v = posToValue p ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |} s
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list l) (Some Vskip))
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev : positive
f : fext
asr : AssocMap.t value
asa : AssocMap.t arr
asrn : AssocMap.t value
asan : AssocMap.t arr
asr' : AssocMap.t value
asa' : AssocMap.t arr
asrn' : AssocMap.t value
asan' : AssocMap.t arr
BOUND : forall p0 : positive,
p' = p0 \/ In p0 (map fst l) ->
0 < Z.pos p0 <= 4294967295
NOREP : list_norepet (p' :: map fst l)
ASSOC : asr ! ev = Some (posToValue p')
s : stmnt
IN : (p', s') = (p', s) \/ In (p', s) l
SRUN : stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |}
(Vcase (Vvar ev)
((Vlit (posToValue p'), s') :: transl_list l)
(Some Vskip))
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
eapply stmnt_runp_Vcase_match.
constructor . simplify. unfold AssocMap.find_assocmap, AssocMapExt.get_default.
rewrite ASSOC. trivial . constructor .p' : positive
s' : stmnt
l : list (positive * stmnt)
IHl : forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value)
(asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr)
(asr' : AssocMap.t value) (asa' : AssocMap.t arr)
(asrn' : AssocMap.t value) (asan' : AssocMap.t arr),
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
list_norepet (map fst l) ->
asr ! ev = Some v ->
forall (p : positive) (s : stmnt),
In (p, s) l ->
v = posToValue p ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |} s
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list l) (Some Vskip))
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev : positive
f : fext
asr : AssocMap.t value
asa : AssocMap.t arr
asrn : AssocMap.t value
asan : AssocMap.t arr
asr' : AssocMap.t value
asa' : AssocMap.t arr
asrn' : AssocMap.t value
asan' : AssocMap.t arr
BOUND : forall p0 : positive,
p' = p0 \/ In p0 (map fst l) ->
0 < Z.pos p0 <= 4294967295
NOREP : list_norepet (p' :: map fst l)
ASSOC : asr ! ev = Some (posToValue p')
s : stmnt
IN : (p', s') = (p', s) \/ In (p', s) l
SRUN : stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
posToValue p' = posToValue p'
auto .p' : positive
s' : stmnt
l : list (positive * stmnt)
IHl : forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value)
(asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr)
(asr' : AssocMap.t value) (asa' : AssocMap.t arr)
(asrn' : AssocMap.t value) (asan' : AssocMap.t arr),
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
list_norepet (map fst l) ->
asr ! ev = Some v ->
forall (p : positive) (s : stmnt),
In (p, s) l ->
v = posToValue p ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |} s
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list l) (Some Vskip))
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev : positive
f : fext
asr : AssocMap.t value
asa : AssocMap.t arr
asrn : AssocMap.t value
asan : AssocMap.t arr
asr' : AssocMap.t value
asa' : AssocMap.t arr
asrn' : AssocMap.t value
asan' : AssocMap.t arr
BOUND : forall p0 : positive,
p' = p0 \/ In p0 (map fst l) ->
0 < Z.pos p0 <= 4294967295
NOREP : list_norepet (p' :: map fst l)
ASSOC : asr ! ev = Some (posToValue p')
s : stmnt
IN : (p', s') = (p', s) \/ In (p', s) l
SRUN : stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s'
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
inversion IN as [INV | INV].p' : positive
s' : stmnt
l : list (positive * stmnt)
IHl : forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value)
(asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr)
(asr' : AssocMap.t value) (asa' : AssocMap.t arr)
(asrn' : AssocMap.t value) (asan' : AssocMap.t arr),
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
list_norepet (map fst l) ->
asr ! ev = Some v ->
forall (p : positive) (s : stmnt),
In (p, s) l ->
v = posToValue p ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |} s
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list l) (Some Vskip))
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev : positive
f : fext
asr : AssocMap.t value
asa : AssocMap.t arr
asrn : AssocMap.t value
asan : AssocMap.t arr
asr' : AssocMap.t value
asa' : AssocMap.t arr
asrn' : AssocMap.t value
asan' : AssocMap.t arr
BOUND : forall p0 : positive,
p' = p0 \/ In p0 (map fst l) ->
0 < Z.pos p0 <= 4294967295
NOREP : list_norepet (p' :: map fst l)
ASSOC : asr ! ev = Some (posToValue p')
s : stmnt
IN : (p', s') = (p', s) \/ In (p', s) l
SRUN : stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
INV : (p', s') = (p', s)
stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s'
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
inversion INV as [INV2]; subst .p' : positive
l : list (positive * stmnt)
IHl : forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value)
(asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr)
(asr' : AssocMap.t value) (asa' : AssocMap.t arr)
(asrn' : AssocMap.t value) (asan' : AssocMap.t arr),
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
list_norepet (map fst l) ->
asr ! ev = Some v ->
forall (p : positive) (s : stmnt),
In (p, s) l ->
v = posToValue p ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |} s
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list l) (Some Vskip))
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev : positive
f : fext
asr : AssocMap.t value
asa : AssocMap.t arr
asrn : AssocMap.t value
asan : AssocMap.t arr
asr' : AssocMap.t value
asa' : AssocMap.t arr
asrn' : AssocMap.t value
asan' : AssocMap.t arr
BOUND : forall p0 : positive,
p' = p0 \/ In p0 (map fst l) ->
0 < Z.pos p0 <= 4294967295
NOREP : list_norepet (p' :: map fst l)
ASSOC : asr ! ev = Some (posToValue p')
s : stmnt
IN : (p', s) = (p', s) \/ In (p', s) l
SRUN : stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
INV : (p', s) = (p', s)
stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
assumption .p' : positive
s' : stmnt
l : list (positive * stmnt)
IHl : forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value)
(asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr)
(asr' : AssocMap.t value) (asa' : AssocMap.t arr)
(asrn' : AssocMap.t value) (asan' : AssocMap.t arr),
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
list_norepet (map fst l) ->
asr ! ev = Some v ->
forall (p : positive) (s : stmnt),
In (p, s) l ->
v = posToValue p ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |} s
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list l) (Some Vskip))
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev : positive
f : fext
asr : AssocMap.t value
asa : AssocMap.t arr
asrn : AssocMap.t value
asan : AssocMap.t arr
asr' : AssocMap.t value
asa' : AssocMap.t arr
asrn' : AssocMap.t value
asan' : AssocMap.t arr
BOUND : forall p0 : positive,
p' = p0 \/ In p0 (map fst l) ->
0 < Z.pos p0 <= 4294967295
NOREP : list_norepet (p' :: map fst l)
ASSOC : asr ! ev = Some (posToValue p')
s : stmnt
IN : (p', s') = (p', s) \/ In (p', s) l
SRUN : stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
INV : In (p', s) l
stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s'
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
inv NOREP. p' : positive
s' : stmnt
l : list (positive * stmnt)
IHl : forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value)
(asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr)
(asr' : AssocMap.t value) (asa' : AssocMap.t arr)
(asrn' : AssocMap.t value) (asan' : AssocMap.t arr),
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
list_norepet (map fst l) ->
asr ! ev = Some v ->
forall (p : positive) (s : stmnt),
In (p, s) l ->
v = posToValue p ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |} s
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list l) (Some Vskip))
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev : positive
f : fext
asr : AssocMap.t value
asa : AssocMap.t arr
asrn : AssocMap.t value
asan : AssocMap.t arr
asr' : AssocMap.t value
asa' : AssocMap.t arr
asrn' : AssocMap.t value
asan' : AssocMap.t arr
BOUND : forall p0 : positive,
p' = p0 \/ In p0 (map fst l) ->
0 < Z.pos p0 <= 4294967295
ASSOC : asr ! ev = Some (posToValue p')
s : stmnt
IN : (p', s') = (p', s) \/ In (p', s) l
SRUN : stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
INV : In (p', s) l
H1 : ~ In p' (map fst l)
H2 : list_norepet (map fst l)
stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s'
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
eapply in_map with (f := fst) in INV.p' : positive
s' : stmnt
l : list (positive * stmnt)
IHl : forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value)
(asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr)
(asr' : AssocMap.t value) (asa' : AssocMap.t arr)
(asrn' : AssocMap.t value) (asan' : AssocMap.t arr),
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
list_norepet (map fst l) ->
asr ! ev = Some v ->
forall (p : positive) (s : stmnt),
In (p, s) l ->
v = posToValue p ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |} s
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list l) (Some Vskip))
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev : positive
f : fext
asr : AssocMap.t value
asa : AssocMap.t arr
asrn : AssocMap.t value
asan : AssocMap.t arr
asr' : AssocMap.t value
asa' : AssocMap.t arr
asrn' : AssocMap.t value
asan' : AssocMap.t arr
BOUND : forall p0 : positive,
p' = p0 \/ In p0 (map fst l) ->
0 < Z.pos p0 <= 4294967295
ASSOC : asr ! ev = Some (posToValue p')
s : stmnt
IN : (p', s') = (p', s) \/ In (p', s) l
SRUN : stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
INV : In (fst (p', s)) (map fst l)
H1 : ~ In p' (map fst l)
H2 : list_norepet (map fst l)
stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s'
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
contradiction .p' : positive
s' : stmnt
l : list (positive * stmnt)
IHl : forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value)
(asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr)
(asr' : AssocMap.t value) (asa' : AssocMap.t arr)
(asrn' : AssocMap.t value) (asan' : AssocMap.t arr),
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
list_norepet (map fst l) ->
asr ! ev = Some v ->
forall (p : positive) (s : stmnt),
In (p, s) l ->
v = posToValue p ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |} s
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list l) (Some Vskip))
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev : positive
f : fext
asr : AssocMap.t value
asa : AssocMap.t arr
asrn : AssocMap.t value
asan : AssocMap.t arr
asr' : AssocMap.t value
asa' : AssocMap.t arr
asrn' : AssocMap.t value
asan' : AssocMap.t arr
BOUND : forall p0 : positive,
p' = p0 \/ In p0 (map fst l) ->
0 < Z.pos p0 <= 4294967295
NOREP : list_norepet (p' :: map fst l)
p : positive
ASSOC : asr ! ev = Some (posToValue p)
s : stmnt
IN : (p', s') = (p, s) \/ In (p, s) l
SRUN : stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
n : p <> p'
stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |}
(Vcase (Vvar ev)
((Vlit (posToValue p'), s') :: transl_list l)
(Some Vskip))
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
eapply stmnt_runp_Vcase_nomatch. constructor . simplify.
unfold AssocMap.find_assocmap, AssocMapExt.get_default. rewrite ASSOC.
trivial . constructor .p' : positive
s' : stmnt
l : list (positive * stmnt)
IHl : forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value)
(asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr)
(asr' : AssocMap.t value) (asa' : AssocMap.t arr)
(asrn' : AssocMap.t value) (asan' : AssocMap.t arr),
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
list_norepet (map fst l) ->
asr ! ev = Some v ->
forall (p : positive) (s : stmnt),
In (p, s) l ->
v = posToValue p ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |} s
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list l) (Some Vskip))
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev : positive
f : fext
asr : AssocMap.t value
asa : AssocMap.t arr
asrn : AssocMap.t value
asan : AssocMap.t arr
asr' : AssocMap.t value
asa' : AssocMap.t arr
asrn' : AssocMap.t value
asan' : AssocMap.t arr
BOUND : forall p0 : positive,
p' = p0 \/ In p0 (map fst l) ->
0 < Z.pos p0 <= 4294967295
NOREP : list_norepet (p' :: map fst l)
p : positive
ASSOC : asr ! ev = Some (posToValue p)
s : stmnt
IN : (p', s') = (p, s) \/ In (p, s) l
SRUN : stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
n : p <> p'
posToValue p' <> posToValue p
unfold not.p' : positive
s' : stmnt
l : list (positive * stmnt)
IHl : forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value)
(asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr)
(asr' : AssocMap.t value) (asa' : AssocMap.t arr)
(asrn' : AssocMap.t value) (asan' : AssocMap.t arr),
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
list_norepet (map fst l) ->
asr ! ev = Some v ->
forall (p : positive) (s : stmnt),
In (p, s) l ->
v = posToValue p ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |} s
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list l) (Some Vskip))
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev : positive
f : fext
asr : AssocMap.t value
asa : AssocMap.t arr
asrn : AssocMap.t value
asan : AssocMap.t arr
asr' : AssocMap.t value
asa' : AssocMap.t arr
asrn' : AssocMap.t value
asan' : AssocMap.t arr
BOUND : forall p0 : positive,
p' = p0 \/ In p0 (map fst l) ->
0 < Z.pos p0 <= 4294967295
NOREP : list_norepet (p' :: map fst l)
p : positive
ASSOC : asr ! ev = Some (posToValue p)
s : stmnt
IN : (p', s') = (p, s) \/ In (p, s) l
SRUN : stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
n : p <> p'
posToValue p' = posToValue p -> False
intros .p' : positive
s' : stmnt
l : list (positive * stmnt)
IHl : forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value)
(asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr)
(asr' : AssocMap.t value) (asa' : AssocMap.t arr)
(asrn' : AssocMap.t value) (asan' : AssocMap.t arr),
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
list_norepet (map fst l) ->
asr ! ev = Some v ->
forall (p : positive) (s : stmnt),
In (p, s) l ->
v = posToValue p ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |} s
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list l) (Some Vskip))
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev : positive
f : fext
asr : AssocMap.t value
asa : AssocMap.t arr
asrn : AssocMap.t value
asan : AssocMap.t arr
asr' : AssocMap.t value
asa' : AssocMap.t arr
asrn' : AssocMap.t value
asan' : AssocMap.t arr
BOUND : forall p0 : positive,
p' = p0 \/ In p0 (map fst l) ->
0 < Z.pos p0 <= 4294967295
NOREP : list_norepet (p' :: map fst l)
p : positive
ASSOC : asr ! ev = Some (posToValue p)
s : stmnt
IN : (p', s') = (p, s) \/ In (p, s) l
SRUN : stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
n : p <> p'
H : posToValue p' = posToValue p
False
apply n.p' : positive
s' : stmnt
l : list (positive * stmnt)
IHl : forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value)
(asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr)
(asr' : AssocMap.t value) (asa' : AssocMap.t arr)
(asrn' : AssocMap.t value) (asan' : AssocMap.t arr),
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
list_norepet (map fst l) ->
asr ! ev = Some v ->
forall (p : positive) (s : stmnt),
In (p, s) l ->
v = posToValue p ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |} s
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list l) (Some Vskip))
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev : positive
f : fext
asr : AssocMap.t value
asa : AssocMap.t arr
asrn : AssocMap.t value
asan : AssocMap.t arr
asr' : AssocMap.t value
asa' : AssocMap.t arr
asrn' : AssocMap.t value
asan' : AssocMap.t arr
BOUND : forall p0 : positive,
p' = p0 \/ In p0 (map fst l) ->
0 < Z.pos p0 <= 4294967295
NOREP : list_norepet (p' :: map fst l)
p : positive
ASSOC : asr ! ev = Some (posToValue p)
s : stmnt
IN : (p', s') = (p, s) \/ In (p, s) l
SRUN : stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
n : p <> p'
H : posToValue p' = posToValue p
p = p'
apply posToValue_inj.p' : positive
s' : stmnt
l : list (positive * stmnt)
IHl : forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value)
(asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr)
(asr' : AssocMap.t value) (asa' : AssocMap.t arr)
(asrn' : AssocMap.t value) (asan' : AssocMap.t arr),
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
list_norepet (map fst l) ->
asr ! ev = Some v ->
forall (p : positive) (s : stmnt),
In (p, s) l ->
v = posToValue p ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |} s
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list l) (Some Vskip))
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev : positive
f : fext
asr : AssocMap.t value
asa : AssocMap.t arr
asrn : AssocMap.t value
asan : AssocMap.t arr
asr' : AssocMap.t value
asa' : AssocMap.t arr
asrn' : AssocMap.t value
asan' : AssocMap.t arr
BOUND : forall p0 : positive,
p' = p0 \/ In p0 (map fst l) ->
0 < Z.pos p0 <= 4294967295
NOREP : list_norepet (p' :: map fst l)
p : positive
ASSOC : asr ! ev = Some (posToValue p)
s : stmnt
IN : (p', s') = (p, s) \/ In (p, s) l
SRUN : stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
n : p <> p'
H : posToValue p' = posToValue p
0 <= Z.pos p <= Int.max_unsigned
apply Zle_relax.p' : positive
s' : stmnt
l : list (positive * stmnt)
IHl : forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value)
(asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr)
(asr' : AssocMap.t value) (asa' : AssocMap.t arr)
(asrn' : AssocMap.t value) (asan' : AssocMap.t arr),
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
list_norepet (map fst l) ->
asr ! ev = Some v ->
forall (p : positive) (s : stmnt),
In (p, s) l ->
v = posToValue p ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |} s
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list l) (Some Vskip))
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev : positive
f : fext
asr : AssocMap.t value
asa : AssocMap.t arr
asrn : AssocMap.t value
asan : AssocMap.t arr
asr' : AssocMap.t value
asa' : AssocMap.t arr
asrn' : AssocMap.t value
asan' : AssocMap.t arr
BOUND : forall p0 : positive,
p' = p0 \/ In p0 (map fst l) ->
0 < Z.pos p0 <= 4294967295
NOREP : list_norepet (p' :: map fst l)
p : positive
ASSOC : asr ! ev = Some (posToValue p)
s : stmnt
IN : (p', s') = (p, s) \/ In (p, s) l
SRUN : stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
n : p <> p'
H : posToValue p' = posToValue p
0 < Z.pos p <= Int.max_unsigned
apply BOUND.p' : positive
s' : stmnt
l : list (positive * stmnt)
IHl : forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value)
(asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr)
(asr' : AssocMap.t value) (asa' : AssocMap.t arr)
(asrn' : AssocMap.t value) (asan' : AssocMap.t arr),
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
list_norepet (map fst l) ->
asr ! ev = Some v ->
forall (p : positive) (s : stmnt),
In (p, s) l ->
v = posToValue p ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |} s
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list l) (Some Vskip))
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev : positive
f : fext
asr : AssocMap.t value
asa : AssocMap.t arr
asrn : AssocMap.t value
asan : AssocMap.t arr
asr' : AssocMap.t value
asa' : AssocMap.t arr
asrn' : AssocMap.t value
asan' : AssocMap.t arr
BOUND : forall p0 : positive,
p' = p0 \/ In p0 (map fst l) ->
0 < Z.pos p0 <= 4294967295
NOREP : list_norepet (p' :: map fst l)
p : positive
ASSOC : asr ! ev = Some (posToValue p)
s : stmnt
IN : (p', s') = (p, s) \/ In (p, s) l
SRUN : stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
n : p <> p'
H : posToValue p' = posToValue p
p' = p \/ In p (map fst l)
right .p' : positive
s' : stmnt
l : list (positive * stmnt)
IHl : forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value)
(asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr)
(asr' : AssocMap.t value) (asa' : AssocMap.t arr)
(asrn' : AssocMap.t value) (asan' : AssocMap.t arr),
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
list_norepet (map fst l) ->
asr ! ev = Some v ->
forall (p : positive) (s : stmnt),
In (p, s) l ->
v = posToValue p ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |} s
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list l) (Some Vskip))
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev : positive
f : fext
asr : AssocMap.t value
asa : AssocMap.t arr
asrn : AssocMap.t value
asan : AssocMap.t arr
asr' : AssocMap.t value
asa' : AssocMap.t arr
asrn' : AssocMap.t value
asan' : AssocMap.t arr
BOUND : forall p0 : positive,
p' = p0 \/ In p0 (map fst l) ->
0 < Z.pos p0 <= 4294967295
NOREP : list_norepet (p' :: map fst l)
p : positive
ASSOC : asr ! ev = Some (posToValue p)
s : stmnt
IN : (p', s') = (p, s) \/ In (p, s) l
SRUN : stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
n : p <> p'
H : posToValue p' = posToValue p
In p (map fst l)
inv IN. p' : positive
s' : stmnt
l : list (positive * stmnt)
IHl : forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value)
(asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr)
(asr' : AssocMap.t value) (asa' : AssocMap.t arr)
(asrn' : AssocMap.t value) (asan' : AssocMap.t arr),
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
list_norepet (map fst l) ->
asr ! ev = Some v ->
forall (p : positive) (s : stmnt),
In (p, s) l ->
v = posToValue p ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |} s
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list l) (Some Vskip))
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev : positive
f : fext
asr : AssocMap.t value
asa : AssocMap.t arr
asrn : AssocMap.t value
asan : AssocMap.t arr
asr' : AssocMap.t value
asa' : AssocMap.t arr
asrn' : AssocMap.t value
asan' : AssocMap.t arr
BOUND : forall p0 : positive,
p' = p0 \/ In p0 (map fst l) ->
0 < Z.pos p0 <= 4294967295
NOREP : list_norepet (p' :: map fst l)
p : positive
ASSOC : asr ! ev = Some (posToValue p)
s : stmnt
SRUN : stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
n : p <> p'
H : posToValue p' = posToValue p
H0 : (p', s') = (p, s)
In p (map fst l)
inv H0; contradiction . p' : positive
s' : stmnt
l : list (positive * stmnt)
IHl : forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value)
(asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr)
(asr' : AssocMap.t value) (asa' : AssocMap.t arr)
(asrn' : AssocMap.t value) (asan' : AssocMap.t arr),
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
list_norepet (map fst l) ->
asr ! ev = Some v ->
forall (p : positive) (s : stmnt),
In (p, s) l ->
v = posToValue p ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |} s
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list l) (Some Vskip))
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev : positive
f : fext
asr : AssocMap.t value
asa : AssocMap.t arr
asrn : AssocMap.t value
asan : AssocMap.t arr
asr' : AssocMap.t value
asa' : AssocMap.t arr
asrn' : AssocMap.t value
asan' : AssocMap.t arr
BOUND : forall p0 : positive,
p' = p0 \/ In p0 (map fst l) ->
0 < Z.pos p0 <= 4294967295
NOREP : list_norepet (p' :: map fst l)
p : positive
ASSOC : asr ! ev = Some (posToValue p)
s : stmnt
SRUN : stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
n : p <> p'
H : posToValue p' = posToValue p
H0 : In (p, s) l
In p (map fst l)
eapply in_map with (f := fst) in H0.p' : positive
s' : stmnt
l : list (positive * stmnt)
IHl : forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value)
(asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr)
(asr' : AssocMap.t value) (asa' : AssocMap.t arr)
(asrn' : AssocMap.t value) (asan' : AssocMap.t arr),
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
list_norepet (map fst l) ->
asr ! ev = Some v ->
forall (p : positive) (s : stmnt),
In (p, s) l ->
v = posToValue p ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |} s
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list l) (Some Vskip))
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev : positive
f : fext
asr : AssocMap.t value
asa : AssocMap.t arr
asrn : AssocMap.t value
asan : AssocMap.t arr
asr' : AssocMap.t value
asa' : AssocMap.t arr
asrn' : AssocMap.t value
asan' : AssocMap.t arr
BOUND : forall p0 : positive,
p' = p0 \/ In p0 (map fst l) ->
0 < Z.pos p0 <= 4294967295
NOREP : list_norepet (p' :: map fst l)
p : positive
ASSOC : asr ! ev = Some (posToValue p)
s : stmnt
SRUN : stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
n : p <> p'
H : posToValue p' = posToValue p
H0 : In (fst (p, s)) (map fst l)
In p (map fst l)
auto .p' : positive
s' : stmnt
l : list (positive * stmnt)
IHl : forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value)
(asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr)
(asr' : AssocMap.t value) (asa' : AssocMap.t arr)
(asrn' : AssocMap.t value) (asan' : AssocMap.t arr),
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
list_norepet (map fst l) ->
asr ! ev = Some v ->
forall (p : positive) (s : stmnt),
In (p, s) l ->
v = posToValue p ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |} s
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list l) (Some Vskip))
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev : positive
f : fext
asr : AssocMap.t value
asa : AssocMap.t arr
asrn : AssocMap.t value
asan : AssocMap.t arr
asr' : AssocMap.t value
asa' : AssocMap.t arr
asrn' : AssocMap.t value
asan' : AssocMap.t arr
BOUND : forall p0 : positive,
p' = p0 \/ In p0 (map fst l) ->
0 < Z.pos p0 <= 4294967295
NOREP : list_norepet (p' :: map fst l)
p : positive
ASSOC : asr ! ev = Some (posToValue p)
s : stmnt
IN : (p', s') = (p, s) \/ In (p, s) l
SRUN : stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
n : p <> p'
H : posToValue p' = posToValue p
0 <= Z.pos p' <= Int.max_unsigned
apply Zle_relax.p' : positive
s' : stmnt
l : list (positive * stmnt)
IHl : forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value)
(asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr)
(asr' : AssocMap.t value) (asa' : AssocMap.t arr)
(asrn' : AssocMap.t value) (asan' : AssocMap.t arr),
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
list_norepet (map fst l) ->
asr ! ev = Some v ->
forall (p : positive) (s : stmnt),
In (p, s) l ->
v = posToValue p ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |} s
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list l) (Some Vskip))
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev : positive
f : fext
asr : AssocMap.t value
asa : AssocMap.t arr
asrn : AssocMap.t value
asan : AssocMap.t arr
asr' : AssocMap.t value
asa' : AssocMap.t arr
asrn' : AssocMap.t value
asan' : AssocMap.t arr
BOUND : forall p0 : positive,
p' = p0 \/ In p0 (map fst l) ->
0 < Z.pos p0 <= 4294967295
NOREP : list_norepet (p' :: map fst l)
p : positive
ASSOC : asr ! ev = Some (posToValue p)
s : stmnt
IN : (p', s') = (p, s) \/ In (p, s) l
SRUN : stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
n : p <> p'
H : posToValue p' = posToValue p
0 < Z.pos p' <= Int.max_unsigned
apply BOUND; auto .p' : positive
s' : stmnt
l : list (positive * stmnt)
IHl : forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value)
(asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr)
(asr' : AssocMap.t value) (asa' : AssocMap.t arr)
(asrn' : AssocMap.t value) (asan' : AssocMap.t arr),
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
list_norepet (map fst l) ->
asr ! ev = Some v ->
forall (p : positive) (s : stmnt),
In (p, s) l ->
v = posToValue p ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |} s
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list l) (Some Vskip))
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev : positive
f : fext
asr : AssocMap.t value
asa : AssocMap.t arr
asrn : AssocMap.t value
asan : AssocMap.t arr
asr' : AssocMap.t value
asa' : AssocMap.t arr
asrn' : AssocMap.t value
asan' : AssocMap.t arr
BOUND : forall p0 : positive,
p' = p0 \/ In p0 (map fst l) ->
0 < Z.pos p0 <= 4294967295
NOREP : list_norepet (p' :: map fst l)
p : positive
ASSOC : asr ! ev = Some (posToValue p)
s : stmnt
IN : (p', s') = (p, s) \/ In (p, s) l
SRUN : stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
n : p <> p'
H : posToValue p' = posToValue p
posToValue p = posToValue p'
auto .p' : positive
s' : stmnt
l : list (positive * stmnt)
IHl : forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value)
(asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr)
(asr' : AssocMap.t value) (asa' : AssocMap.t arr)
(asrn' : AssocMap.t value) (asan' : AssocMap.t arr),
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
list_norepet (map fst l) ->
asr ! ev = Some v ->
forall (p : positive) (s : stmnt),
In (p, s) l ->
v = posToValue p ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |} s
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list l) (Some Vskip))
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev : positive
f : fext
asr : AssocMap.t value
asa : AssocMap.t arr
asrn : AssocMap.t value
asan : AssocMap.t arr
asr' : AssocMap.t value
asa' : AssocMap.t arr
asrn' : AssocMap.t value
asan' : AssocMap.t arr
BOUND : forall p0 : positive,
p' = p0 \/ In p0 (map fst l) ->
0 < Z.pos p0 <= 4294967295
NOREP : list_norepet (p' :: map fst l)
p : positive
ASSOC : asr ! ev = Some (posToValue p)
s : stmnt
IN : (p', s') = (p, s) \/ In (p, s) l
SRUN : stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
n : p <> p'
stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list l) (Some Vskip))
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
eapply IHl. auto . inv NOREP. auto . eassumption . inv IN. inv H. contradiction . apply H.p' : positive
s' : stmnt
l : list (positive * stmnt)
IHl : forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value)
(asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr)
(asr' : AssocMap.t value) (asa' : AssocMap.t arr)
(asrn' : AssocMap.t value) (asan' : AssocMap.t arr),
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
list_norepet (map fst l) ->
asr ! ev = Some v ->
forall (p : positive) (s : stmnt),
In (p, s) l ->
v = posToValue p ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |} s
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list l) (Some Vskip))
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev : positive
f : fext
asr : AssocMap.t value
asa : AssocMap.t arr
asrn : AssocMap.t value
asan : AssocMap.t arr
asr' : AssocMap.t value
asa' : AssocMap.t arr
asrn' : AssocMap.t value
asan' : AssocMap.t arr
BOUND : forall p0 : positive,
p' = p0 \/ In p0 (map fst l) ->
0 < Z.pos p0 <= 4294967295
NOREP : list_norepet (p' :: map fst l)
p : positive
ASSOC : asr ! ev = Some (posToValue p)
s : stmnt
IN : (p', s') = (p, s) \/ In (p, s) l
SRUN : stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
n : p <> p'
posToValue p = posToValue p
trivial .p' : positive
s' : stmnt
l : list (positive * stmnt)
IHl : forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value)
(asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr)
(asr' : AssocMap.t value) (asa' : AssocMap.t arr)
(asrn' : AssocMap.t value) (asan' : AssocMap.t arr),
(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295 ) ->
list_norepet (map fst l) ->
asr ! ev = Some v ->
forall (p : positive) (s : stmnt),
In (p, s) l ->
v = posToValue p ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |} s
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |}
{| assoc_blocking := asa; assoc_nonblocking := asan |}
(Vcase (Vvar ev) (transl_list l) (Some Vskip))
{| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
{| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev : positive
f : fext
asr : AssocMap.t value
asa : AssocMap.t arr
asrn : AssocMap.t value
asan : AssocMap.t arr
asr' : AssocMap.t value
asa' : AssocMap.t arr
asrn' : AssocMap.t value
asan' : AssocMap.t arr
BOUND : forall p0 : positive,
p' = p0 \/ In p0 (map fst l) ->
0 < Z.pos p0 <= 4294967295
NOREP : list_norepet (p' :: map fst l)
p : positive
ASSOC : asr ! ev = Some (posToValue p)
s : stmnt
IN : (p', s') = (p, s) \/ In (p, s) l
SRUN : stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
n : p <> p'
stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := asrn |}
{|
assoc_blocking := asa;
assoc_nonblocking := asan |} s
{|
assoc_blocking := asr';
assoc_nonblocking := asrn' |}
{|
assoc_blocking := asa';
assoc_nonblocking := asan' |}
assumption .
Qed .
Hint Resolve transl_list_correct : verilogproof.
Lemma pc_wf :
forall A m p v ,
(forall p0 , In p0 (List.map fst (@AssocMap.elements A m)) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
m!p = Some v ->
0 <= Z.pos p <= Int.max_unsigned.forall (A : Type ) (m : AssocMap.t A) (p : positive)
(v : A),
(forall p0 : positive,
In p0 (map fst (AssocMap.elements m)) ->
0 < Z.pos p0 <= Int.max_unsigned) ->
m ! p = Some v -> 0 <= Z.pos p <= Int.max_unsigned
Proof .forall (A : Type ) (m : AssocMap.t A) (p : positive)
(v : A),
(forall p0 : positive,
In p0 (map fst (AssocMap.elements m)) ->
0 < Z.pos p0 <= Int.max_unsigned) ->
m ! p = Some v -> 0 <= Z.pos p <= Int.max_unsigned
intros A m p v LT S.A : Type
m : AssocMap.t A
p : positive
v : A
LT : forall p0 : positive,
In p0 (map fst (AssocMap.elements m)) ->
0 < Z.pos p0 <= Int.max_unsigned
S : m ! p = Some v
0 <= Z.pos p <= Int.max_unsigned
apply Zle_relax.A : Type
m : AssocMap.t A
p : positive
v : A
LT : forall p0 : positive,
In p0 (map fst (AssocMap.elements m)) ->
0 < Z.pos p0 <= Int.max_unsigned
S : m ! p = Some v
0 < Z.pos p <= Int.max_unsigned
apply LT.A : Type
m : AssocMap.t A
p : positive
v : A
LT : forall p0 : positive,
In p0 (map fst (AssocMap.elements m)) ->
0 < Z.pos p0 <= Int.max_unsigned
S : m ! p = Some v
In p (map fst (AssocMap.elements m))
apply AssocMap.elements_correct in S.A : Type
m : AssocMap.t A
p : positive
v : A
LT : forall p0 : positive,
In p0 (map fst (AssocMap.elements m)) ->
0 < Z.pos p0 <= Int.max_unsigned
S : In (p, v) (AssocMap.elements m)
In p (map fst (AssocMap.elements m))
remember (p, v) as x.A : Type
m : AssocMap.t A
p : positive
v : A
LT : forall p0 : positive,
In p0 (map fst (AssocMap.elements m)) ->
0 < Z.pos p0 <= Int.max_unsigned
x : (positive * A)%type
Heqx : x = (p, v)
S : In x (AssocMap.elements m)
In p (map fst (AssocMap.elements m))
exploit in_map. apply S. instantiate (1 := fst).A : Type
m : AssocMap.t A
p : positive
v : A
LT : forall p0 : positive,
In p0 (map fst (AssocMap.elements m)) ->
0 < Z.pos p0 <= Int.max_unsigned
x : (positive * A)%type
Heqx : x = (p, v)
S : In x (AssocMap.elements m)
In (fst x) (map fst (AssocMap.elements m)) ->
In p (map fst (AssocMap.elements m))
subst .A : Type
m : AssocMap.t A
p : positive
v : A
LT : forall p0 : positive,
In p0 (map fst (AssocMap.elements m)) ->
0 < Z.pos p0 <= Int.max_unsigned
S : In (p, v) (AssocMap.elements m)
In (fst (p, v)) (map fst (AssocMap.elements m)) ->
In p (map fst (AssocMap.elements m))
simplify. A : Type
m : AssocMap.t A
p : positive
v : A
LT : forall p0 : positive,
In p0 (map fst (AssocMap.elements m)) ->
0 < Z.pos p0 <= 4294967295
S : In (p, v) (AssocMap.elements m)
H : In p (map fst (AssocMap.elements m))
In p (map fst (AssocMap.elements m))
auto .
Qed .
Lemma mis_stepp_decl :
forall l asr asa f ,
mis_stepp f asr asa (map Vdeclaration l) asr asa.forall (l : list declaration) (asr : reg_associations)
(asa : arr_associations) (f : fext),
mis_stepp f asr asa (map Vdeclaration l) asr asa
Proof .forall (l : list declaration) (asr : reg_associations)
(asa : arr_associations) (f : fext),
mis_stepp f asr asa (map Vdeclaration l) asr asa
induction l.forall (asr : reg_associations)
(asa : arr_associations) (f : fext),
mis_stepp f asr asa (map Vdeclaration nil) asr asa
- forall (asr : reg_associations)
(asa : arr_associations) (f : fext),
mis_stepp f asr asa (map Vdeclaration nil) asr asa
intros .asr : reg_associations
asa : arr_associations
f : fext
mis_stepp f asr asa (map Vdeclaration nil) asr asa
constructor .
- a : declaration
l : list declaration
IHl : forall (asr : reg_associations) (asa : arr_associations) (f : fext),
mis_stepp f asr asa (map Vdeclaration l) asr asa
forall (asr : reg_associations)
(asa : arr_associations) (f : fext),
mis_stepp f asr asa (map Vdeclaration (a :: l)) asr
asa
intros .a : declaration
l : list declaration
IHl : forall (asr : reg_associations) (asa : arr_associations) (f : fext),
mis_stepp f asr asa (map Vdeclaration l) asr asa
asr : reg_associations
asa : arr_associations
f : fext
mis_stepp f asr asa (map Vdeclaration (a :: l)) asr
asa
simplify. a : declaration
l : list declaration
IHl : forall (asr : reg_associations) (asa : arr_associations) (f : fext),
mis_stepp f asr asa (map Vdeclaration l) asr asa
asr : reg_associations
asa : arr_associations
f : fext
mis_stepp f asr asa
(Vdeclaration a :: map Vdeclaration l) asr asa
econstructor . constructor .a : declaration
l : list declaration
IHl : forall (asr : reg_associations) (asa : arr_associations) (f : fext),
mis_stepp f asr asa (map Vdeclaration l) asr asa
asr : reg_associations
asa : arr_associations
f : fext
mis_stepp f asr asa (map Vdeclaration l) asr asa
auto .
Qed .
Hint Resolve mis_stepp_decl : verilogproof.
Section CORRECTNESS .
Variable prog : HTL.program.
Variable tprog : program.
Hypothesis TRANSL : match_prog prog tprog.
Let ge : HTL.genv := Globalenvs.Genv.globalenv prog.
Let tge : genv := Globalenvs.Genv.globalenv tprog.
Lemma symbols_preserved :
forall (s : AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s.prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
ge := Genv.globalenv prog : HTL.genv
tge := Genv.globalenv tprog : genv
forall s : AST.ident ,
Genv.find_symbol tge s = Genv.find_symbol ge s
Proof .prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
ge := Genv.globalenv prog : HTL.genv
tge := Genv.globalenv tprog : genv
forall s : AST.ident ,
Genv.find_symbol tge s = Genv.find_symbol ge s
intros .prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
ge := Genv.globalenv prog : HTL.genv
tge := Genv.globalenv tprog : genv
s : AST.ident
Genv.find_symbol tge s = Genv.find_symbol ge s
eapply (Genv.find_symbol_match TRANSL). Qed .
Hint Resolve symbols_preserved : verilogproof.
Lemma function_ptr_translated :
forall (b : Values.block) (f : HTL.fundef),
Genv.find_funct_ptr ge b = Some f ->
exists tf ,
Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = tf.prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
ge := Genv.globalenv prog : HTL.genv
tge := Genv.globalenv tprog : genv
forall (b : Values.block) (f : HTL.fundef),
Genv.find_funct_ptr ge b = Some f ->
exists tf : fundef,
Genv.find_funct_ptr tge b = Some tf /\
transl_fundef f = tf
Proof .prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
ge := Genv.globalenv prog : HTL.genv
tge := Genv.globalenv tprog : genv
forall (b : Values.block) (f : HTL.fundef),
Genv.find_funct_ptr ge b = Some f ->
exists tf : fundef,
Genv.find_funct_ptr tge b = Some tf /\
transl_fundef f = tf
intros .prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
ge := Genv.globalenv prog : HTL.genv
tge := Genv.globalenv tprog : genv
b : Values.block
f : HTL.fundef
H : Genv.find_funct_ptr ge b = Some f
exists tf : fundef,
Genv.find_funct_ptr tge b = Some tf /\
transl_fundef f = tf
exploit (Genv.find_funct_ptr_match TRANSL); eauto . prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
ge := Genv.globalenv prog : HTL.genv
tge := Genv.globalenv tprog : genv
b : Values.block
f : HTL.fundef
H : Genv.find_funct_ptr ge b = Some f
(exists
(cunit : AST.program (AST.fundef HTL.module) unit)
(tf : AST.fundef module),
Genv.find_funct_ptr (Genv.globalenv tprog) b =
Some tf /\
tf = transl_fundef f /\ linkorder cunit prog) ->
exists tf : fundef,
Genv.find_funct_ptr tge b = Some tf /\
transl_fundef f = tf
intros (cu & tf & P & Q & R); exists tf ; auto .
Qed .
Hint Resolve function_ptr_translated : verilogproof.
Lemma functions_translated :
forall (v : Values.val) (f : HTL.fundef),
Genv.find_funct ge v = Some f ->
exists tf ,
Genv.find_funct tge v = Some tf /\ transl_fundef f = tf.prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
ge := Genv.globalenv prog : HTL.genv
tge := Genv.globalenv tprog : genv
forall (v : Values.val) (f : HTL.fundef),
Genv.find_funct ge v = Some f ->
exists tf : fundef,
Genv.find_funct tge v = Some tf /\
transl_fundef f = tf
Proof .prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
ge := Genv.globalenv prog : HTL.genv
tge := Genv.globalenv tprog : genv
forall (v : Values.val) (f : HTL.fundef),
Genv.find_funct ge v = Some f ->
exists tf : fundef,
Genv.find_funct tge v = Some tf /\
transl_fundef f = tf
intros .prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
ge := Genv.globalenv prog : HTL.genv
tge := Genv.globalenv tprog : genv
v : Values.val
f : HTL.fundef
H : Genv.find_funct ge v = Some f
exists tf : fundef,
Genv.find_funct tge v = Some tf /\
transl_fundef f = tf
exploit (Genv.find_funct_match TRANSL); eauto . prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
ge := Genv.globalenv prog : HTL.genv
tge := Genv.globalenv tprog : genv
v : Values.val
f : HTL.fundef
H : Genv.find_funct ge v = Some f
(exists
(cunit : AST.program (AST.fundef HTL.module) unit)
(tf : AST.fundef module),
Genv.find_funct (Genv.globalenv tprog) v = Some tf /\
tf = transl_fundef f /\ linkorder cunit prog) ->
exists tf : fundef,
Genv.find_funct tge v = Some tf /\
transl_fundef f = tf
intros (cu & tf & P & Q & R); exists tf ; auto .
Qed .
Hint Resolve functions_translated : verilogproof.
Lemma senv_preserved :
Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge).prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
ge := Genv.globalenv prog : HTL.genv
tge := Genv.globalenv tprog : genv
Senv.equiv ge tge
Proof .prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
ge := Genv.globalenv prog : HTL.genv
tge := Genv.globalenv tprog : genv
Senv.equiv ge tge
intros .prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
ge := Genv.globalenv prog : HTL.genv
tge := Genv.globalenv tprog : genv
Senv.equiv ge tge
eapply (Genv.senv_match TRANSL).
Qed .
Hint Resolve senv_preserved : verilogproof.
Theorem transl_step_correct :
forall (S1 : HTL.state) t S2 ,
HTL.step ge S1 t S2 ->
forall (R1 : state),
match_states S1 R1 ->
exists R2 , Smallstep.plus step tge R1 t R2 /\ match_states S2 R2.prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
ge := Genv.globalenv prog : HTL.genv
tge := Genv.globalenv tprog : genv
forall (S1 : HTL.state) (t : Events.trace)
(S2 : HTL.state),
HTL.step ge S1 t S2 ->
forall R1 : state,
match_states S1 R1 ->
exists R2 : state,
plus step tge R1 t R2 /\ match_states S2 R2
Proof .prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
ge := Genv.globalenv prog : HTL.genv
tge := Genv.globalenv tprog : genv
forall (S1 : HTL.state) (t : Events.trace)
(S2 : HTL.state),
HTL.step ge S1 t S2 ->
forall R1 : state,
match_states S1 R1 ->
exists R2 : state,
plus step tge R1 t R2 /\ match_states S2 R2
induction 1 ; intros R1 MSTATE; inv MSTATE.prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
tge := Genv.globalenv tprog : genv
g : HTL.genv
m : HTL.module
st : positive
sf : list HTL.stackframe
ctrl, data : stmnt
asr : AssocMap.t value
asa : AssocMap.t arr
basr1 : AssocMap.t value
basa1 : AssocMap.t arr
nasr1 : AssocMap.t value
nasa1 : AssocMap.t arr
basr2 : AssocMap.t value
basa2 : AssocMap.t arr
nasr2 : AssocMap.t value
nasa2 : AssocMap.t arr
f : fext
pstval : positive
H : asr ! (HTL.mod_reset m) = Some (ZToValue 0 )
H0 : asr ! (HTL.mod_finish m) = Some (ZToValue 0 )
H1 : asr ! (HTL.mod_st m) = Some (posToValue st)
H2 : (HTL.mod_controllogic m) ! st = Some ctrl
H3 : (HTL.mod_datapath m) ! st = Some data
H4 : stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := empty_assocmap |}
{|
assoc_blocking := asa;
assoc_nonblocking := HTL.empty_stack m |} ctrl
{|
assoc_blocking := basr1;
assoc_nonblocking := nasr1 |}
{|
assoc_blocking := basa1;
assoc_nonblocking := nasa1 |}
H5 : basr1 ! (HTL.mod_st m) = Some (posToValue st)
H6 : stmnt_runp f
{|
assoc_blocking := basr1;
assoc_nonblocking := nasr1 |}
{|
assoc_blocking := basa1;
assoc_nonblocking := nasa1 |} data
{|
assoc_blocking := basr2;
assoc_nonblocking := nasr2 |}
{|
assoc_blocking := basa2;
assoc_nonblocking := nasa2 |}
H9 : (merge_regs nasr2 basr2) ! (HTL.mod_st m) =
Some (posToValue pstval)
H10 : Z.pos pstval <= Int.max_unsigned
vstk : list stackframe
H17 : match_stacks sf vstk
exists R2 : state,
plus step tge
(State vstk (transl_module m) st asr asa)
Events.E0 R2 /\
match_states
(HTL.State sf m pstval (merge_regs nasr2 basr2)
(merge_arrs nasa2 basa2)) R2
- prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
tge := Genv.globalenv tprog : genv
g : HTL.genv
m : HTL.module
st : positive
sf : list HTL.stackframe
ctrl, data : stmnt
asr : AssocMap.t value
asa : AssocMap.t arr
basr1 : AssocMap.t value
basa1 : AssocMap.t arr
nasr1 : AssocMap.t value
nasa1 : AssocMap.t arr
basr2 : AssocMap.t value
basa2 : AssocMap.t arr
nasr2 : AssocMap.t value
nasa2 : AssocMap.t arr
f : fext
pstval : positive
H : asr ! (HTL.mod_reset m) = Some (ZToValue 0 )
H0 : asr ! (HTL.mod_finish m) = Some (ZToValue 0 )
H1 : asr ! (HTL.mod_st m) = Some (posToValue st)
H2 : (HTL.mod_controllogic m) ! st = Some ctrl
H3 : (HTL.mod_datapath m) ! st = Some data
H4 : stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := empty_assocmap |}
{|
assoc_blocking := asa;
assoc_nonblocking := HTL.empty_stack m |} ctrl
{|
assoc_blocking := basr1;
assoc_nonblocking := nasr1 |}
{|
assoc_blocking := basa1;
assoc_nonblocking := nasa1 |}
H5 : basr1 ! (HTL.mod_st m) = Some (posToValue st)
H6 : stmnt_runp f
{|
assoc_blocking := basr1;
assoc_nonblocking := nasr1 |}
{|
assoc_blocking := basa1;
assoc_nonblocking := nasa1 |} data
{|
assoc_blocking := basr2;
assoc_nonblocking := nasr2 |}
{|
assoc_blocking := basa2;
assoc_nonblocking := nasa2 |}
H9 : (merge_regs nasr2 basr2) ! (HTL.mod_st m) =
Some (posToValue pstval)
H10 : Z.pos pstval <= Int.max_unsigned
vstk : list stackframe
H17 : match_stacks sf vstk
exists R2 : state,
plus step tge
(State vstk (transl_module m) st asr asa)
Events.E0 R2 /\
match_states
(HTL.State sf m pstval (merge_regs nasr2 basr2)
(merge_arrs nasa2 basa2)) R2
econstructor ; split . apply Smallstep.plus_one. econstructor .
assumption . assumption . eassumption . apply valueToPos_posToValue.
split . lia .
eapply pc_wf. intros . pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _].
split . lia . apply HP. eassumption . eassumption .
econstructor . econstructor . eapply stmnt_runp_Vcond_false. econstructor . econstructor .
simpl . unfold find_assocmap. unfold AssocMapExt.get_default.
rewrite H. trivial .
econstructor . simpl . auto . auto .
eapply transl_list_correct.
intros . split . lia . pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. auto .
apply Maps.PTree.elements_keys_norepet. eassumption .
2 : { apply valueToPos_inj. apply unsigned_posToValue_le.
eapply pc_wf. intros . pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _].
split . lia . apply HP. eassumption . eassumption .
apply unsigned_posToValue_le. eapply pc_wf. intros . pose proof (HTL.mod_wf m) as HP.
destruct HP as [HP _].
split . lia . apply HP. eassumption . eassumption . trivial .
}
apply Maps.PTree.elements_correct. eassumption . eassumption .
econstructor . econstructor .
eapply transl_list_correct.
intros . split . lia . pose proof (HTL.mod_wf m) as HP. destruct HP as [_ HP]. auto .
apply Maps.PTree.elements_keys_norepet. eassumption .
2 : { apply valueToPos_inj. apply unsigned_posToValue_le.
eapply pc_wf. intros . pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _].
split . lia . apply HP. eassumption . eassumption .
apply unsigned_posToValue_le. eapply pc_wf. intros . pose proof (HTL.mod_wf m) as HP.
destruct HP as [HP _].
split . lia . apply HP. eassumption . eassumption . trivial .
}
apply Maps.PTree.elements_correct. eassumption . eassumption .
apply mis_stepp_decl. trivial . trivial . simpl . eassumption . auto .prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
tge := Genv.globalenv tprog : genv
g : HTL.genv
m : HTL.module
st : positive
sf : list HTL.stackframe
ctrl, data : stmnt
asr : AssocMap.t value
asa : AssocMap.t arr
basr1 : AssocMap.t value
basa1 : AssocMap.t arr
nasr1 : AssocMap.t value
nasa1 : AssocMap.t arr
basr2 : AssocMap.t value
basa2 : AssocMap.t arr
nasr2 : AssocMap.t value
nasa2 : AssocMap.t arr
f : fext
pstval : positive
H : asr ! (HTL.mod_reset m) = Some (ZToValue 0 )
H0 : asr ! (HTL.mod_finish m) = Some (ZToValue 0 )
H1 : asr ! (HTL.mod_st m) = Some (posToValue st)
H2 : (HTL.mod_controllogic m) ! st = Some ctrl
H3 : (HTL.mod_datapath m) ! st = Some data
H4 : stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := empty_assocmap |}
{|
assoc_blocking := asa;
assoc_nonblocking := HTL.empty_stack m |} ctrl
{|
assoc_blocking := basr1;
assoc_nonblocking := nasr1 |}
{|
assoc_blocking := basa1;
assoc_nonblocking := nasa1 |}
H5 : basr1 ! (HTL.mod_st m) = Some (posToValue st)
H6 : stmnt_runp f
{|
assoc_blocking := basr1;
assoc_nonblocking := nasr1 |}
{|
assoc_blocking := basa1;
assoc_nonblocking := nasa1 |} data
{|
assoc_blocking := basr2;
assoc_nonblocking := nasr2 |}
{|
assoc_blocking := basa2;
assoc_nonblocking := nasa2 |}
H9 : (merge_regs nasr2 basr2) ! (HTL.mod_st m) =
Some (posToValue pstval)
H10 : Z.pos pstval <= Int.max_unsigned
vstk : list stackframe
H17 : match_stacks sf vstk
match_states
(HTL.State sf m pstval (merge_regs nasr2 basr2)
(merge_arrs nasa2 basa2))
(State vstk (transl_module m)
(valueToPos (posToValue pstval))
(merge_regs nasr2 basr2) (merge_arrs nasa2 basa2))
rewrite valueToPos_posToValue.prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
tge := Genv.globalenv tprog : genv
g : HTL.genv
m : HTL.module
st : positive
sf : list HTL.stackframe
ctrl, data : stmnt
asr : AssocMap.t value
asa : AssocMap.t arr
basr1 : AssocMap.t value
basa1 : AssocMap.t arr
nasr1 : AssocMap.t value
nasa1 : AssocMap.t arr
basr2 : AssocMap.t value
basa2 : AssocMap.t arr
nasr2 : AssocMap.t value
nasa2 : AssocMap.t arr
f : fext
pstval : positive
H : asr ! (HTL.mod_reset m) = Some (ZToValue 0 )
H0 : asr ! (HTL.mod_finish m) = Some (ZToValue 0 )
H1 : asr ! (HTL.mod_st m) = Some (posToValue st)
H2 : (HTL.mod_controllogic m) ! st = Some ctrl
H3 : (HTL.mod_datapath m) ! st = Some data
H4 : stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := empty_assocmap |}
{|
assoc_blocking := asa;
assoc_nonblocking := HTL.empty_stack m |} ctrl
{|
assoc_blocking := basr1;
assoc_nonblocking := nasr1 |}
{|
assoc_blocking := basa1;
assoc_nonblocking := nasa1 |}
H5 : basr1 ! (HTL.mod_st m) = Some (posToValue st)
H6 : stmnt_runp f
{|
assoc_blocking := basr1;
assoc_nonblocking := nasr1 |}
{|
assoc_blocking := basa1;
assoc_nonblocking := nasa1 |} data
{|
assoc_blocking := basr2;
assoc_nonblocking := nasr2 |}
{|
assoc_blocking := basa2;
assoc_nonblocking := nasa2 |}
H9 : (merge_regs nasr2 basr2) ! (HTL.mod_st m) =
Some (posToValue pstval)
H10 : Z.pos pstval <= Int.max_unsigned
vstk : list stackframe
H17 : match_stacks sf vstk
match_states
(HTL.State sf m pstval (merge_regs nasr2 basr2)
(merge_arrs nasa2 basa2))
(State vstk (transl_module m) pstval
(merge_regs nasr2 basr2) (merge_arrs nasa2 basa2))
constructor ; assumption .prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
tge := Genv.globalenv tprog : genv
g : HTL.genv
m : HTL.module
st : positive
sf : list HTL.stackframe
ctrl, data : stmnt
asr : AssocMap.t value
asa : AssocMap.t arr
basr1 : AssocMap.t value
basa1 : AssocMap.t arr
nasr1 : AssocMap.t value
nasa1 : AssocMap.t arr
basr2 : AssocMap.t value
basa2 : AssocMap.t arr
nasr2 : AssocMap.t value
nasa2 : AssocMap.t arr
f : fext
pstval : positive
H : asr ! (HTL.mod_reset m) = Some (ZToValue 0 )
H0 : asr ! (HTL.mod_finish m) = Some (ZToValue 0 )
H1 : asr ! (HTL.mod_st m) = Some (posToValue st)
H2 : (HTL.mod_controllogic m) ! st = Some ctrl
H3 : (HTL.mod_datapath m) ! st = Some data
H4 : stmnt_runp f
{|
assoc_blocking := asr;
assoc_nonblocking := empty_assocmap |}
{|
assoc_blocking := asa;
assoc_nonblocking := HTL.empty_stack m |} ctrl
{|
assoc_blocking := basr1;
assoc_nonblocking := nasr1 |}
{|
assoc_blocking := basa1;
assoc_nonblocking := nasa1 |}
H5 : basr1 ! (HTL.mod_st m) = Some (posToValue st)
H6 : stmnt_runp f
{|
assoc_blocking := basr1;
assoc_nonblocking := nasr1 |}
{|
assoc_blocking := basa1;
assoc_nonblocking := nasa1 |} data
{|
assoc_blocking := basr2;
assoc_nonblocking := nasr2 |}
{|
assoc_blocking := basa2;
assoc_nonblocking := nasa2 |}
H9 : (merge_regs nasr2 basr2) ! (HTL.mod_st m) =
Some (posToValue pstval)
H10 : Z.pos pstval <= Int.max_unsigned
vstk : list stackframe
H17 : match_stacks sf vstk
0 <= Z.pos pstval <= Int.max_unsigned
lia .
- prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
tge := Genv.globalenv tprog : genv
g : HTL.genv
m : HTL.module
st : HTL.node
asr : AssocMap.t value
asa : assocmap_arr
retval : value
sf : list HTL.stackframe
H : asr ! (HTL.mod_finish m) = Some (ZToValue 1 )
H0 : asr ! (HTL.mod_return m) = Some retval
vstk : list stackframe
H7 : match_stacks sf vstk
exists R2 : state,
plus step tge
(State vstk (transl_module m) st asr asa)
Events.E0 R2 /\
match_states (HTL.Returnstate sf retval) R2
econstructor ; split . apply Smallstep.plus_one. apply step_finish. assumption . eassumption .prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
tge := Genv.globalenv tprog : genv
g : HTL.genv
m : HTL.module
st : HTL.node
asr : AssocMap.t value
asa : assocmap_arr
retval : value
sf : list HTL.stackframe
H : asr ! (HTL.mod_finish m) = Some (ZToValue 1 )
H0 : asr ! (HTL.mod_return m) = Some retval
vstk : list stackframe
H7 : match_stacks sf vstk
match_states (HTL.Returnstate sf retval)
(Returnstate vstk retval)
constructor ; assumption .
- prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
tge := Genv.globalenv tprog : genv
g : HTL.genv
m : HTL.module
exists R2 : state,
plus step tge (Callstate nil (transl_module m) nil)
Events.E0 R2 /\
match_states
(HTL.State nil m (HTL.mod_entrypoint m)
(((HTL.init_regs nil (HTL.mod_params m))
# (HTL.mod_st m) <-
(posToValue (HTL.mod_entrypoint m)))
# (HTL.mod_finish m) <- (ZToValue 0 ))
# (HTL.mod_reset m) <- (ZToValue 0 )
(HTL.empty_stack m)) R2
econstructor ; split . apply Smallstep.plus_one. constructor .prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
tge := Genv.globalenv tprog : genv
g : HTL.genv
m : HTL.module
match_states
(HTL.State nil m (HTL.mod_entrypoint m)
(((HTL.init_regs nil (HTL.mod_params m))
# (HTL.mod_st m) <-
(posToValue (HTL.mod_entrypoint m)))
# (HTL.mod_finish m) <- (ZToValue 0 ))
# (HTL.mod_reset m) <- (ZToValue 0 )
(HTL.empty_stack m))
(State nil (transl_module m)
(mod_entrypoint (transl_module m))
(((init_params nil (mod_args (transl_module m)))
# (mod_st (transl_module m)) <-
(posToValue (mod_entrypoint (transl_module m))))
# (mod_finish (transl_module m)) <- (ZToValue 0 ))
# (mod_reset (transl_module m)) <- (ZToValue 0 )
(empty_stack (transl_module m)))
constructor .prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
tge := Genv.globalenv tprog : genv
g : HTL.genv
m : HTL.module
match_stacks nil nil
constructor .
- prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
tge := Genv.globalenv tprog : genv
g : HTL.genv
m : HTL.module
asr : assocmap_reg
asa : assocmap_arr
i : value
r : HTL.reg
sf : list HTL.stackframe
pc : HTL.node
vstk : list stackframe
H3 : match_stacks
(HTL.Stackframe r m pc asr asa :: sf) vstk
exists R2 : state,
plus step tge (Returnstate vstk i) Events.E0 R2 /\
match_states
(HTL.State sf m pc
(asr # (HTL.mod_st m) <- (posToValue pc))
# r <- i asa) R2
inv H3. prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
tge := Genv.globalenv tprog : genv
g : HTL.genv
m : HTL.module
asr : assocmap_reg
asa : assocmap_arr
i : value
r : HTL.reg
sf : list HTL.stackframe
pc : HTL.node
vstk0 : list stackframe
H7 : match_stacks sf vstk0
exists R2 : state,
plus step tge
(Returnstate
(Stackframe r (transl_module m) pc asr asa
:: vstk0) i) Events.E0 R2 /\
match_states
(HTL.State sf m pc
(asr # (HTL.mod_st m) <- (posToValue pc))
# r <- i asa) R2
econstructor ; split . apply Smallstep.plus_one. constructor . trivial .prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
tge := Genv.globalenv tprog : genv
g : HTL.genv
m : HTL.module
asr : assocmap_reg
asa : assocmap_arr
i : value
r : HTL.reg
sf : list HTL.stackframe
pc : HTL.node
vstk0 : list stackframe
H7 : match_stacks sf vstk0
match_states
(HTL.State sf m pc
(asr # (HTL.mod_st m) <- (posToValue pc)) # r <-
i asa)
(State vstk0 (transl_module m) pc
(asr # (mod_st (transl_module m)) <-
(posToValue pc)) # r <- i asa)
apply match_state.prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
tge := Genv.globalenv tprog : genv
g : HTL.genv
m : HTL.module
asr : assocmap_reg
asa : assocmap_arr
i : value
r : HTL.reg
sf : list HTL.stackframe
pc : HTL.node
vstk0 : list stackframe
H7 : match_stacks sf vstk0
match_stacks sf vstk0
assumption .
Qed .
Hint Resolve transl_step_correct : verilogproof.
Lemma transl_initial_states :
forall s1 : Smallstep.state (HTL.semantics prog),
Smallstep.initial_state (HTL.semantics prog) s1 ->
exists s2 : Smallstep.state (Verilog.semantics tprog),
Smallstep.initial_state (Verilog.semantics tprog) s2 /\ match_states s1 s2.prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
ge := Genv.globalenv prog : HTL.genv
tge := Genv.globalenv tprog : genv
forall s1 : Smallstep.state (HTL.semantics prog),
Smallstep.initial_state (HTL.semantics prog) s1 ->
exists s2 : Smallstep.state (semantics tprog),
Smallstep.initial_state (semantics tprog) s2 /\
match_states s1 s2
Proof .prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
ge := Genv.globalenv prog : HTL.genv
tge := Genv.globalenv tprog : genv
forall s1 : Smallstep.state (HTL.semantics prog),
Smallstep.initial_state (HTL.semantics prog) s1 ->
exists s2 : Smallstep.state (semantics tprog),
Smallstep.initial_state (semantics tprog) s2 /\
match_states s1 s2
induction 1 .prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
ge := Genv.globalenv prog : HTL.genv
tge := Genv.globalenv tprog : genv
b : Values.block
m0 : Memory.Mem.mem
m : HTL.module
ge0 := Genv.globalenv prog : Genv.t HTL.fundef unit
H : Genv.init_mem prog = Some m0
H0 : Genv.find_symbol ge0 (AST.prog_main prog) =
Some b
H1 : Genv.find_funct_ptr ge0 b = Some (AST.Internal m)
exists s2 : Smallstep.state (semantics tprog),
Smallstep.initial_state (semantics tprog) s2 /\
match_states (HTL.Callstate nil m nil) s2
econstructor ; split . econstructor .
apply (Genv.init_mem_transf TRANSL); eauto .
rewrite symbols_preserved.
replace (AST.prog_main tprog) with (AST.prog_main prog); eauto .
symmetry ; eapply Linking.match_program_main; eauto .
exploit function_ptr_translated; eauto . intros [tf [A B]].
inv B. eauto .prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
ge := Genv.globalenv prog : HTL.genv
tge := Genv.globalenv tprog : genv
b : Values.block
m0 : Memory.Mem.mem
m : HTL.module
ge0 := Genv.globalenv prog : Genv.t HTL.fundef unit
H : Genv.init_mem prog = Some m0
H0 : Genv.find_symbol ge0 (AST.prog_main prog) =
Some b
H1 : Genv.find_funct_ptr ge0 b = Some (AST.Internal m)
match_states (HTL.Callstate nil m nil)
(Callstate nil (transl_module m) nil)
constructor .
Qed .
Hint Resolve transl_initial_states : verilogproof.
Lemma transl_final_states :
forall (s1 : Smallstep.state (HTL.semantics prog))
(s2 : Smallstep.state (Verilog.semantics tprog))
(r : Integers.Int.int),
match_states s1 s2 ->
Smallstep.final_state (HTL.semantics prog) s1 r ->
Smallstep.final_state (Verilog.semantics tprog) s2 r.prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
ge := Genv.globalenv prog : HTL.genv
tge := Genv.globalenv tprog : genv
forall (s1 : Smallstep.state (HTL.semantics prog))
(s2 : Smallstep.state (semantics tprog)) (r : int),
match_states s1 s2 ->
Smallstep.final_state (HTL.semantics prog) s1 r ->
Smallstep.final_state (semantics tprog) s2 r
Proof .prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
ge := Genv.globalenv prog : HTL.genv
tge := Genv.globalenv tprog : genv
forall (s1 : Smallstep.state (HTL.semantics prog))
(s2 : Smallstep.state (semantics tprog)) (r : int),
match_states s1 s2 ->
Smallstep.final_state (HTL.semantics prog) s1 r ->
Smallstep.final_state (semantics tprog) s2 r
intros .prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
ge := Genv.globalenv prog : HTL.genv
tge := Genv.globalenv tprog : genv
s1 : Smallstep.state (HTL.semantics prog)
s2 : Smallstep.state (semantics tprog)
r : int
H : match_states s1 s2
H0 : Smallstep.final_state (HTL.semantics prog) s1 r
Smallstep.final_state (semantics tprog) s2 r
inv H0. prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
ge := Genv.globalenv prog : HTL.genv
tge := Genv.globalenv tprog : genv
s2 : Smallstep.state (semantics tprog)
retval : value
H : match_states (HTL.Returnstate nil retval) s2
Smallstep.final_state (semantics tprog) s2
(valueToInt retval)
inv H. prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
ge := Genv.globalenv prog : HTL.genv
tge := Genv.globalenv tprog : genv
retval : value
vstk : list stackframe
H3 : match_stacks nil vstk
Smallstep.final_state (semantics tprog)
(Returnstate vstk retval) (valueToInt retval)
inv H3. prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
ge := Genv.globalenv prog : HTL.genv
tge := Genv.globalenv tprog : genv
retval : value
Smallstep.final_state (semantics tprog)
(Returnstate nil retval) (valueToInt retval)
constructor .prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
ge := Genv.globalenv prog : HTL.genv
tge := Genv.globalenv tprog : genv
retval : value
valueToInt retval = valueToInt retval
reflexivity .
Qed .
Hint Resolve transl_final_states : verilogproof.
Theorem transf_program_correct :
forward_simulation (HTL.semantics prog) (Verilog.semantics tprog).prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
ge := Genv.globalenv prog : HTL.genv
tge := Genv.globalenv tprog : genv
forward_simulation (HTL.semantics prog)
(semantics tprog)
Proof .prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
ge := Genv.globalenv prog : HTL.genv
tge := Genv.globalenv tprog : genv
forward_simulation (HTL.semantics prog)
(semantics tprog)
eapply Smallstep.forward_simulation_plus; eauto with verilogproof.prog : HTL.program
tprog : program
TRANSL : match_prog prog tprog
ge := Genv.globalenv prog : HTL.genv
tge := Genv.globalenv tprog : genv
forall id : AST.ident ,
Senv.public_symbol (symbolenv (semantics tprog)) id =
Senv.public_symbol (symbolenv (HTL.semantics prog)) id
apply senv_preserved.
Qed .
End CORRECTNESS .