(* * 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 Maps.From compcert Require Errors Globalenvs Integers.From compcert Require Import AST RTL.From vericert Require Import Verilog HTL Vericertlib AssocMap ValueInt Statemonad.Hint Resolve AssocMap.gempty : htlh.Hint Resolve AssocMap.gso : htlh.Hint Resolve AssocMap.gss : htlh.Hint Resolve Ple_refl : htlh.Hint Resolve Ple_succ : htlh.Recordstate: Type := mkstate {
st_st : reg;
st_freshreg: reg;
st_freshstate: node;
st_scldecls: AssocMap.t (option io * scl_decl);
st_arrdecls: AssocMap.t (option io * arr_decl);
st_datapath: datapath;
st_controllogic: controllogic;
}.Definitioninit_state (st : reg) : state :=
mkstate st
1%positive
1%positive
(AssocMap.empty (option io * scl_decl))
(AssocMap.empty (option io * arr_decl))
(AssocMap.empty stmnt)
(AssocMap.empty stmnt).ModuleHTLState <: State.Definitionst := state.Inductivest_incr: state -> state -> Prop :=
state_incr_intro:
forall (s1s2: state),
st_st s1 = st_st s2 ->
Ple s1.(st_freshreg) s2.(st_freshreg) ->
Ple s1.(st_freshstate) s2.(st_freshstate) ->
(foralln,
s1.(st_datapath)!n = None \/ s2.(st_datapath)!n = s1.(st_datapath)!n) ->
(foralln,
s1.(st_controllogic)!n = None
\/ s2.(st_controllogic)!n = s1.(st_controllogic)!n) ->
st_incr s1 s2.Hint Constructors st_incr : htlh.Definitionst_prop := st_incr.Hint Unfold st_prop : htlh.
auto with htlh.Qed.Definitiondeclare_reg (i : option io) (r : reg) (sz : nat) : mon unit :=
funs => OK tt (mkstate
s.(st_st)
s.(st_freshreg)
s.(st_freshstate)
(AssocMap.set r (i, VScalar sz) s.(st_scldecls))
s.(st_arrdecls)
s.(st_datapath)
s.(st_controllogic))
(declare_reg_state_incr i s r sz).Definitionadd_instr (n : node) (n' : node) (st : stmnt) : mon unit :=
funs =>
match check_empty_node_datapath s n, check_empty_node_controllogic s n with
| left STM, left TRANS =>
OK tt (mkstate
s.(st_st)
s.(st_freshreg)
(st_freshstate s)
s.(st_scldecls)
s.(st_arrdecls)
(AssocMap.set n st s.(st_datapath))
(AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic)))
(add_instr_state_incr s n n' st STM TRANS)
| _, _ => Error (Errors.msg "HTL.add_instr")
end.
forall (s : state) (n : positive) (st : stmnt),
(st_datapath s) ! n = None ->
(st_controllogic s) ! n = None ->
st_incr s
{|
st_st := st_st s;
st_freshreg := st_freshreg s;
st_freshstate := st_freshstate s;
st_scldecls := st_scldecls s;
st_arrdecls := st_arrdecls s;
st_datapath := AssocMap.set n st (st_datapath s);
st_controllogic := AssocMap.set n Vskip
(st_controllogic s) |}
forall (s : state) (n : positive) (st : stmnt),
(st_datapath s) ! n = None ->
(st_controllogic s) ! n = None ->
st_incr s
{|
st_st := st_st s;
st_freshreg := st_freshreg s;
st_freshstate := st_freshstate s;
st_scldecls := st_scldecls s;
st_arrdecls := st_arrdecls s;
st_datapath := AssocMap.set n st (st_datapath s);
st_controllogic := AssocMap.set n Vskip
(st_controllogic s) |}
constructor; intros;
try (simpl; destruct (peq n n0); subst);
auto with htlh.Qed.Definitionadd_instr_skip (n : node) (st : stmnt) : mon unit :=
funs =>
match check_empty_node_datapath s n, check_empty_node_controllogic s n with
| left STM, left TRANS =>
OK tt (mkstate
s.(st_st)
s.(st_freshreg)
(st_freshstate s)
s.(st_scldecls)
s.(st_arrdecls)
(AssocMap.set n st s.(st_datapath))
(AssocMap.set n Vskip s.(st_controllogic)))
(add_instr_skip_state_incr s n st STM TRANS)
| _, _ => Error (Errors.msg "HTL.add_instr")
end.
forall (s : state) (n : positive) (st : stmnt),
(st_datapath s) ! n = None ->
(st_controllogic s) ! n = None ->
st_incr s
{|
st_st := st_st s;
st_freshreg := st_freshreg s;
st_freshstate := st_freshstate s;
st_scldecls := st_scldecls s;
st_arrdecls := st_arrdecls s;
st_datapath := AssocMap.set n Vskip (st_datapath s);
st_controllogic := AssocMap.set n st
(st_controllogic s) |}
forall (s : state) (n : positive) (st : stmnt),
(st_datapath s) ! n = None ->
(st_controllogic s) ! n = None ->
st_incr s
{|
st_st := st_st s;
st_freshreg := st_freshreg s;
st_freshstate := st_freshstate s;
st_scldecls := st_scldecls s;
st_arrdecls := st_arrdecls s;
st_datapath := AssocMap.set n Vskip (st_datapath s);
st_controllogic := AssocMap.set n st
(st_controllogic s) |}
constructor; intros;
try (simpl; destruct (peq n n0); subst);
auto with htlh.Qed.Definitionadd_node_skip (n : node) (st : stmnt) : mon unit :=
funs =>
match check_empty_node_datapath s n, check_empty_node_controllogic s n with
| left STM, left TRANS =>
OK tt (mkstate
s.(st_st)
s.(st_freshreg)
(st_freshstate s)
s.(st_scldecls)
s.(st_arrdecls)
(AssocMap.set n Vskip s.(st_datapath))
(AssocMap.set n st s.(st_controllogic)))
(add_node_skip_state_incr s n st STM TRANS)
| _, _ => Error (Errors.msg "HTL.add_instr")
end.Definitionnonblock (dst : reg) (e : expr) := Vnonblock (Vvar dst) e.Definitionblock (dst : reg) (e : expr) := Vblock (Vvar dst) e.Definitionbop (op : binop) (r1r2 : reg) : expr :=
Vbinop op (Vvar r1) (Vvar r2).Definitionboplit (op : binop) (r : reg) (l : Integers.int) : expr :=
Vbinop op (Vvar r) (Vlit (intToValue l)).Definitionboplitz (op: binop) (r: reg) (l: Z) : expr :=
Vbinop op (Vvar r) (Vlit (ZToValue l)).Definitiontranslate_comparison (c : Integers.comparison) (args : list reg) : mon expr :=
match c, args with
| Integers.Ceq, r1::r2::nil => ret (bop Veq r1 r2)
| Integers.Cne, r1::r2::nil => ret (bop Vne r1 r2)
| Integers.Clt, r1::r2::nil => ret (bop Vlt r1 r2)
| Integers.Cgt, r1::r2::nil => ret (bop Vgt r1 r2)
| Integers.Cle, r1::r2::nil => ret (bop Vle r1 r2)
| Integers.Cge, r1::r2::nil => ret (bop Vge r1 r2)
| _, _ => error (Errors.msg "Htlgen: comparison instruction not implemented: other")
end.Definitiontranslate_comparison_imm (c : Integers.comparison) (args : list reg) (i: Integers.int)
: mon expr :=
match c, args with
| Integers.Ceq, r1::nil => ret (boplit Veq r1 i)
| Integers.Cne, r1::nil => ret (boplit Vne r1 i)
| Integers.Clt, r1::nil => ret (boplit Vlt r1 i)
| Integers.Cgt, r1::nil => ret (boplit Vgt r1 i)
| Integers.Cle, r1::nil => ret (boplit Vle r1 i)
| Integers.Cge, r1::nil => ret (boplit Vge r1 i)
| _, _ => error (Errors.msg "Htlgen: comparison_imm instruction not implemented: other")
end.Definitiontranslate_comparisonu (c : Integers.comparison) (args : list reg) : mon expr :=
match c, args with
| Integers.Clt, r1::r2::nil => ret (bop Vltu r1 r2)
| Integers.Cgt, r1::r2::nil => ret (bop Vgtu r1 r2)
| Integers.Cle, r1::r2::nil => ret (bop Vleu r1 r2)
| Integers.Cge, r1::r2::nil => ret (bop Vgeu r1 r2)
| _, _ => error (Errors.msg "Htlgen: comparison instruction not implemented: other")
end.Definitiontranslate_comparison_immu (c : Integers.comparison) (args : list reg) (i: Integers.int)
: mon expr :=
match c, args with
| Integers.Clt, r1::nil => ret (boplit Vltu r1 i)
| Integers.Cgt, r1::nil => ret (boplit Vgtu r1 i)
| Integers.Cle, r1::nil => ret (boplit Vleu r1 i)
| Integers.Cge, r1::nil => ret (boplit Vgeu r1 i)
| _, _ => error (Errors.msg "Htlgen: comparison_imm instruction not implemented: other")
end.Definitiontranslate_condition (c : Op.condition) (args : list reg) : mon expr :=
match c, args with
| Op.Ccomp c, _ => translate_comparison c args
| Op.Ccompu c, _ => translate_comparisonu c args
| Op.Ccompimm c i, _ => translate_comparison_imm c args i
| Op.Ccompuimm c i, _ => translate_comparison_immu c args i
| Op.Cmaskzero n, _ => error (Errors.msg "Htlgen: condition instruction not implemented: Cmaskzero")
| Op.Cmasknotzero n, _ => error (Errors.msg "Htlgen: condition instruction not implemented: Cmasknotzero")
| _, _ => error (Errors.msg "Htlgen: condition instruction not implemented: other")
end.Definitioncheck_address_parameter_signed (p : Z) : bool :=
Z.leb Integers.Ptrofs.min_signed p
&& Z.leb p Integers.Ptrofs.max_signed.Definitioncheck_address_parameter_unsigned (p : Z) : bool :=
Z.leb p Integers.Ptrofs.max_unsigned.Definitiontranslate_eff_addressing (a: Op.addressing) (args: list reg) : mon expr :=
match a, args with(* TODO: We should be more methodical here; what are the possibilities?*)
| Op.Aindexed off, r1::nil =>
if (check_address_parameter_signed off)
then ret (boplitz Vadd r1 off)
else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed): address out of bounds")
| Op.Ascaled scale offset, r1::nil =>
if (check_address_parameter_signed scale) && (check_address_parameter_signed offset)
then ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue offset)))
else error (Errors.msg "Veriloggen: translate_eff_addressing (Ascaled): address out of bounds")
| Op.Aindexed2 offset, r1::r2::nil =>
if (check_address_parameter_signed offset)
then ret (Vbinop Vadd (bop Vadd r1 r2) (Vlit (ZToValue offset)))
else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2): address out of bounds")
| Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *)if (check_address_parameter_signed scale) && (check_address_parameter_signed offset)
then ret (Vbinop Vadd (Vvar r1) (Vbinop Vadd (boplitz Vmul r2 scale) (Vlit (ZToValue offset))))
else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2scaled): address out of bounds")
| Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)leta := Integers.Ptrofs.unsigned a inif (check_address_parameter_unsigned a)
then ret (Vlit (ZToValue a))
else error (Errors.msg "Veriloggen: translate_eff_addressing (Ainstack): address out of bounds")
| _, _ => error (Errors.msg "Veriloggen: translate_eff_addressing unsuported addressing")
end.(** Translate an instruction to a statement. FIX mulhs mulhu *)Definitiontranslate_instr (op : Op.operation) (args : list reg) : mon expr :=
match op, args with
| Op.Omove, r::nil => ret (Vvar r)
| Op.Ointconst n, _ => ret (Vlit (intToValue n))
| Op.Oneg, r::nil => ret (Vunop Vneg (Vvar r))
| Op.Osub, r1::r2::nil => ret (bop Vsub r1 r2)
| Op.Omul, r1::r2::nil => ret (bop Vmul r1 r2)
| Op.Omulimm n, r::nil => ret (boplit Vmul r n)
| Op.Omulhs, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: mulhs")
| Op.Omulhu, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: mulhu")
| Op.Odiv, r1::r2::nil => ret (bop Vdiv r1 r2)
| Op.Odivu, r1::r2::nil => ret (bop Vdivu r1 r2)
| Op.Omod, r1::r2::nil => ret (bop Vmod r1 r2)
| Op.Omodu, r1::r2::nil => ret (bop Vmodu r1 r2)
| Op.Oand, r1::r2::nil => ret (bop Vand r1 r2)
| Op.Oandimm n, r::nil => ret (boplit Vand r n)
| Op.Oor, r1::r2::nil => ret (bop Vor r1 r2)
| Op.Oorimm n, r::nil => ret (boplit Vor r n)
| Op.Oxor, r1::r2::nil => ret (bop Vxor r1 r2)
| Op.Oxorimm n, r::nil => ret (boplit Vxor r n)
| Op.Onot, r::nil => ret (Vunop Vnot (Vvar r))
| Op.Oshl, r1::r2::nil => ret (bop Vshl r1 r2)
| Op.Oshlimm n, r::nil => ret (boplit Vshl r n)
| Op.Oshr, r1::r2::nil => ret (bop Vshr r1 r2)
| Op.Oshrimm n, r::nil => ret (boplit Vshr r n)
| Op.Oshrximm n, r::nil =>
ret (Vternary (Vbinop Vlt (Vvar r) (Vlit (ZToValue 0)))
(Vunop Vneg (Vbinop Vshru (Vunop Vneg (Vvar r)) (Vlit n)))
(Vbinop Vshru (Vvar r) (Vlit n)))
| Op.Oshru, r1::r2::nil => ret (bop Vshru r1 r2)
| Op.Oshruimm n, r::nil => ret (boplit Vshru r n)
| Op.Ororimm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Ororimm")
(*ret (Vbinop Vor (boplit Vshru r (Integers.Int.modu n (Integers.Int.repr 32))) (boplit Vshl r (Integers.Int.sub (Integers.Int.repr 32) (Integers.Int.modu n (Integers.Int.repr 32)))))*)
| Op.Oshldimm n, r::nil => ret (Vbinop Vor (boplit Vshl r n) (boplit Vshr r (Integers.Int.sub (Integers.Int.repr 32) n)))
| Op.Ocmp c, _ => translate_condition c args
| Op.Osel c AST.Tint, r1::r2::rl =>
do tc <- translate_condition c rl;
ret (Vternary tc (Vvar r1) (Vvar r2))
| Op.Olea a, _ => translate_eff_addressing a args
| _, _ => error (Errors.msg "Htlgen: Instruction not implemented: other")
end.
forall (s : state) (e : expr) (n : positive)
(n1n2 : node),
(st_datapath s) ! n = None ->
(st_controllogic s) ! n = None ->
st_incr s
{|
st_st := st_st s;
st_freshreg := st_freshreg s;
st_freshstate := st_freshstate s;
st_scldecls := st_scldecls s;
st_arrdecls := st_arrdecls s;
st_datapath := AssocMap.set n Vskip (st_datapath s);
st_controllogic := AssocMap.set n
(state_cond (st_st s) e n1 n2)
(st_controllogic s) |}
forall (s : state) (e : expr) (n : positive)
(n1n2 : node),
(st_datapath s) ! n = None ->
(st_controllogic s) ! n = None ->
st_incr s
{|
st_st := st_st s;
st_freshreg := st_freshreg s;
st_freshstate := st_freshstate s;
st_scldecls := st_scldecls s;
st_arrdecls := st_arrdecls s;
st_datapath := AssocMap.set n Vskip (st_datapath s);
st_controllogic := AssocMap.set n
(state_cond (st_st s) e n1 n2)
(st_controllogic s) |}
apply state_incr_intro; simpl;
try (intros; destruct (peq n0 n); subst);
auto with htlh.Qed.Definitionadd_branch_instr (e: expr) (nn1n2: node) : mon unit :=
funs =>
match check_empty_node_datapath s n, check_empty_node_controllogic s n with
| left NSTM, left NTRANS =>
OK tt (mkstate
s.(st_st)
(st_freshreg s)
(st_freshstate s)
s.(st_scldecls)
s.(st_arrdecls)
(AssocMap.set n Vskip (st_datapath s))
(AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s)))
(add_branch_instr_state_incr s e n n1 n2 NSTM NTRANS)
| _, _ => Error (Errors.msg "Htlgen: add_branch_instr")
end.Definitiontranslate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing)
(args : list reg) (stack : reg) : mon expr :=
match mem, addr, args with(* TODO: We should be more methodical here; what are the possibilities?*)
| Mint32, Op.Aindexed off, r1::nil =>
if (check_address_parameter_signed off)
then ret (Vvari stack (Vbinop Vdivu (boplitz Vadd r1 off) (Vlit (ZToValue 4))))
else error (Errors.msg "HTLgen: translate_arr_access address out of bounds")
| Mint32, Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *)if (check_address_parameter_signed scale) && (check_address_parameter_signed offset)
then ret (Vvari stack
(Vbinop Vdivu
(Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale))
(Vlit (ZToValue 4))))
else error (Errors.msg "HTLgen: translate_arr_access address out of bounds")
| Mint32, Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)leta := Integers.Ptrofs.unsigned a inif (check_address_parameter_unsigned a)
then ret (Vvari stack (Vlit (ZToValue (a / 4))))
else error (Errors.msg "HTLgen: eff_addressing out of bounds stack offset")
| _, _, _ => error (Errors.msg "HTLgen: translate_arr_access unsuported addressing")
end.Fixpointenumerate (i : nat) (ns : list node) {structns} : list (nat * node) :=
match ns with
| n :: ns' => (i, n) :: enumerate (i+1) ns'
| nil => nil
end.Definitiontbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) :=
List.map (funa => match a with
(i, n) => (Vlit (natToValue i), Vnonblock (Vvar st) (Vlit (posToValue n)))
end)
(enumerate 0 ns).Definitiontransf_instr (finrtrnstack: reg) (ni: node * instruction) : mon unit :=
match ni with
(n, i) =>
match i with
| Inop n' =>
if Z.leb (Z.pos n') Integers.Int.max_unsigned then
add_instr n n' Vskip
else error (Errors.msg "State is larger than 2^32.")
| Iop op args dst n' =>
if Z.leb (Z.pos n') Integers.Int.max_unsigned thendo instr <- translate_instr op args;
do _ <- declare_reg None dst 32;
add_instr n n' (nonblock dst instr)
else error (Errors.msg "State is larger than 2^32.")
| Iload mem addr args dst n' =>
if Z.leb (Z.pos n') Integers.Int.max_unsigned thendo src <- translate_arr_access mem addr args stack;
do _ <- declare_reg None dst 32;
add_instr n n' (nonblock dst src)
else error (Errors.msg "State is larger than 2^32.")
| Istore mem addr args src n' =>
if Z.leb (Z.pos n') Integers.Int.max_unsigned thendo dst <- translate_arr_access mem addr args stack;
add_instr n n' (Vnonblock dst (Vvar src)) (* TODO: Could juse use add_instr? reg exists. *)else error (Errors.msg "State is larger than 2^32.")
| Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.")
| Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.")
| Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.")
| Icond cond args n1 n2 =>
if Z.leb (Z.pos n1) Integers.Int.max_unsigned && Z.leb (Z.pos n2) Integers.Int.max_unsigned thendo e <- translate_condition cond args;
add_branch_instr e n n1 n2
else error (Errors.msg "State is larger than 2^32.")
| Ijumptable r tbl =>
(*do s <- get; add_node_skip n (Vcase (Vvar r) (tbl_to_case_expr s.(st_st) tbl) (Some Vskip))*)
error (Errors.msg "Ijumptable: Case statement not supported.")
| Ireturn r =>
match r with
| Some r' =>
add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r')))
| None =>
add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vlit (ZToValue 0%Z))))
endendend.
forall (m : PTree.t stmnt) (pc : positive) (i : stmnt),
m ! pc = Some i -> Ple pc (max_pc_map m)
forall (m : PTree.t stmnt) (pc : positive) (i : stmnt),
m ! pc = Some i -> Ple pc (max_pc_map m)
m:PTree.t stmnt
pc:positive
i:stmnt
m ! pc = Some i -> Ple pc (max_pc_map m)
m:PTree.t stmnt
pc:positive
i:stmnt
m ! pc = Some i -> Ple pc (max_pc_map m)
m:PTree.t stmnt
pc:positive
i:stmnt
forall (mm' : PTree.t stmnt) (a : positive),
(forallx : PTree.elt, m ! x = m' ! x) ->
(m ! pc = Some i -> Ple pc a) ->
m' ! pc = Some i -> Ple pc a
m:PTree.t stmnt
pc:positive
i:stmnt
(PTree.empty stmnt) ! pc = Some i -> Ple pc 1
m:PTree.t stmnt
pc:positive
i:stmnt
forall (m0 : PTree.t stmnt) (a : positive)
(k : PTree.elt) (v : stmnt),
m0 ! k = None ->
m ! k = Some v ->
(m0 ! pc = Some i -> Ple pc a) ->
(PTree.set k v m0) ! pc = Some i ->
Ple pc (Pos.max a k)
(* extensionality *)
m:PTree.t stmnt
pc:positive
i:stmnt
m0, m':PTree.t stmnt
a:positive
H:forallx : PTree.elt, m0 ! x = m' ! x
H0:m0 ! pc = Some i -> Ple pc a
H1:m' ! pc = Some i
Ple pc a
m:PTree.t stmnt
pc:positive
i:stmnt
(PTree.empty stmnt) ! pc = Some i -> Ple pc 1
m:PTree.t stmnt
pc:positive
i:stmnt
forall (m0 : PTree.t stmnt) (a : positive)
(k : PTree.elt) (v : stmnt),
m0 ! k = None ->
m ! k = Some v ->
(m0 ! pc = Some i -> Ple pc a) ->
(PTree.set k v m0) ! pc = Some i ->
Ple pc (Pos.max a k)
m:PTree.t stmnt
pc:positive
i:stmnt
m0, m':PTree.t stmnt
a:positive
H:forallx : PTree.elt, m0 ! x = m' ! x
H0:m0 ! pc = Some i -> Ple pc a
H1:m' ! pc = Some i
m0 ! pc = Some i
m:PTree.t stmnt
pc:positive
i:stmnt
(PTree.empty stmnt) ! pc = Some i -> Ple pc 1
m:PTree.t stmnt
pc:positive
i:stmnt
forall (m0 : PTree.t stmnt) (a : positive)
(k : PTree.elt) (v : stmnt),
m0 ! k = None ->
m ! k = Some v ->
(m0 ! pc = Some i -> Ple pc a) ->
(PTree.set k v m0) ! pc = Some i ->
Ple pc (Pos.max a k)
m:PTree.t stmnt
pc:positive
i:stmnt
(PTree.empty stmnt) ! pc = Some i -> Ple pc 1
m:PTree.t stmnt
pc:positive
i:stmnt
forall (m0 : PTree.t stmnt) (a : positive)
(k : PTree.elt) (v : stmnt),
m0 ! k = None ->
m ! k = Some v ->
(m0 ! pc = Some i -> Ple pc a) ->
(PTree.set k v m0) ! pc = Some i ->
Ple pc (Pos.max a k)
(* base case *)
m:PTree.t stmnt
pc:positive
i:stmnt
None = Some i -> Ple pc 1
m:PTree.t stmnt
pc:positive
i:stmnt
forall (m0 : PTree.t stmnt) (a : positive)
(k : PTree.elt) (v : stmnt),
m0 ! k = None ->
m ! k = Some v ->
(m0 ! pc = Some i -> Ple pc a) ->
(PTree.set k v m0) ! pc = Some i ->
Ple pc (Pos.max a k)
m:PTree.t stmnt
pc:positive
i:stmnt
forall (m0 : PTree.t stmnt) (a : positive)
(k : PTree.elt) (v : stmnt),
m0 ! k = None ->
m ! k = Some v ->
(m0 ! pc = Some i -> Ple pc a) ->
(PTree.set k v m0) ! pc = Some i ->
Ple pc (Pos.max a k)
(* inductive case *)
m:PTree.t stmnt
pc:positive
i:stmnt
m0:PTree.t stmnt
a:positive
k:PTree.elt
v:stmnt
H:m0 ! k = None
H0:m ! k = Some v
H1:m0 ! pc = Some i -> Ple pc a
H2:(PTree.set k v m0) ! pc = Some i
Ple pc (Pos.max a k)
m:PTree.t stmnt
pc:positive
i:stmnt
m0:PTree.t stmnt
a:positive
k:PTree.elt
v:stmnt
H:m0 ! k = None
H0:m ! k = Some v
H1:m0 ! pc = Some i -> Ple pc a
H2:(if peq pc k then Some v else m0 ! pc) = Some i
Ple pc (Pos.max a k)
m:PTree.t stmnt
pc:positive
i:stmnt
m0:PTree.t stmnt
a:positive
k:PTree.elt
v:stmnt
H:m0 ! k = None
H0:m ! k = Some v
H1:m0 ! pc = Some i -> Ple pc a
e:pc = k
H2:Some v = Some i
Ple pc (Pos.max a k)
m:PTree.t stmnt
pc:positive
i:stmnt
m0:PTree.t stmnt
a:positive
k:PTree.elt
v:stmnt
H:m0 ! k = None
H0:m ! k = Some v
H1:m0 ! pc = Some i -> Ple pc a
n:pc <> k
H2:m0 ! pc = Some i
Ple pc (Pos.max a k)
m:PTree.t stmnt
i:stmnt
m0:PTree.t stmnt
a:positive
k:PTree.elt
H:m0 ! k = None
H0:m ! k = Some i
H1:m0 ! k = Some i -> Ple k a
Ple k (Pos.max a k)
m:PTree.t stmnt
pc:positive
i:stmnt
m0:PTree.t stmnt
a:positive
k:PTree.elt
v:stmnt
H:m0 ! k = None
H0:m ! k = Some v
H1:m0 ! pc = Some i -> Ple pc a
n:pc <> k
H2:m0 ! pc = Some i
Ple pc (Pos.max a k)
omegais deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
m:PTree.t stmnt
pc:positive
i:stmnt
m0:PTree.t stmnt
a:positive
k:PTree.elt
v:stmnt
H:m0 ! k = None
H0:m ! k = Some v
H1:m0 ! pc = Some i -> Ple pc a
n:pc <> k
H2:m0 ! pc = Some i
Ple pc (Pos.max a k)
m:PTree.t stmnt
pc:positive
i:stmnt
m0:PTree.t stmnt
a:positive
k:PTree.elt
v:stmnt
H:m0 ! k = None
H0:m ! k = Some v
H1:m0 ! pc = Some i -> Ple pc a
n:pc <> k
H2:m0 ! pc = Some i
Ple pc a
m:PTree.t stmnt
pc:positive
i:stmnt
m0:PTree.t stmnt
a:positive
k:PTree.elt
v:stmnt
H:m0 ! k = None
H0:m ! k = Some v
H1:m0 ! pc = Some i -> Ple pc a
n:pc <> k
H2:m0 ! pc = Some i
Ple a (Pos.max a k)
m:PTree.t stmnt
pc:positive
i:stmnt
m0:PTree.t stmnt
a:positive
k:PTree.elt
v:stmnt
H:m0 ! k = None
H0:m ! k = Some v
H1:m0 ! pc = Some i -> Ple pc a
n:pc <> k
H2:m0 ! pc = Some i
Ple a (Pos.max a k)
omegais deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
Qed.
forallm : PTree.t stmnt,
Z.pos (max_pc_map m) <= Integers.Int.max_unsigned ->
map_well_formed m
forallm : PTree.t stmnt,
Z.pos (max_pc_map m) <= Integers.Int.max_unsigned ->
map_well_formed m