diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-11-26 01:00:41 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-11-26 01:00:41 +0000 |
| commit | fa4b252945a870100305c159d20e264be18973ce (patch) | |
| tree | 435cbd07a2af45f3f08dc8ac892fa48044047eeb /docs/proof/HTLgen.html | |
| parent | 29bee524cccfe08c680f655b1969a4c421e0a969 (diff) | |
| download | vericert-fa4b252945a870100305c159d20e264be18973ce.tar.gz vericert-fa4b252945a870100305c159d20e264be18973ce.zip | |
Add proof documentation
Diffstat (limited to 'docs/proof/HTLgen.html')
| -rw-r--r-- | docs/proof/HTLgen.html | 970 |
1 files changed, 970 insertions, 0 deletions
diff --git a/docs/proof/HTLgen.html b/docs/proof/HTLgen.html new file mode 100644 index 0000000..a356f8c --- /dev/null +++ b/docs/proof/HTLgen.html @@ -0,0 +1,970 @@ +<?xml version="1.0" encoding="utf-8" ?> +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> +<html xmlns="http://www.w3.org/1999/xhtml" class="alectryon-standalone" xml:lang="en" lang="en"> +<head> +<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> +<meta name="generator" content="Docutils 0.16: http://docutils.sourceforge.net/" /> +<title>HTLgen.v</title> +<link rel="stylesheet" href="alectryon.css" type="text/css" /> +<link rel="stylesheet" href="docutils_basic.css" type="text/css" /> +<link rel="stylesheet" href="tango_subtle.css" type="text/css" /> +<link rel="stylesheet" href="tango_subtle.min.css" type="text/css" /> +<script type="text/javascript" src="alectryon.js"></script> +<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/IBM-type/0.5.4/css/ibm-type.min.css" integrity="sha512-sky5cf9Ts6FY1kstGOBHSybfKqdHR41M0Ldb0BjNiv3ifltoQIsg0zIaQ+wwdwgQ0w9vKFW7Js50lxH9vqNSSw==" crossorigin="anonymous" /> +<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/firacode/5.2.0/fira_code.min.css" integrity="sha512-MbysAYimH1hH2xYzkkMHB6MqxBqfP0megxsCLknbYqHVwXTCg9IqHbk+ZP/vnhO8UEW6PaXAkKe2vQ+SWACxxA==" crossorigin="anonymous" /> +</head> +<body> +<div class="alectryon-root alectryon-floating"><div class="document"> + + +<pre class="alectryon-io"><!-- Generator: Alectryon v1.0 --><span class="coq-wsp"><span class="highlight"><span class="c">(* </span> +<span class="c"> * Vericert: Verified high-level synthesis.</span> +<span class="c"> * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com></span> +<span class="c"> *</span> +<span class="c"> * This program is free software: you can redistribute it and/or modify</span> +<span class="c"> * it under the terms of the GNU General Public License as published by</span> +<span class="c"> * the Free Software Foundation, either version 3 of the License, or</span> +<span class="c"> * (at your option) any later version.</span> +<span class="c"> *</span> +<span class="c"> * This program is distributed in the hope that it will be useful,</span> +<span class="c"> * but WITHOUT ANY WARRANTY; without even the implied warranty of</span> +<span class="c"> * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the</span> +<span class="c"> * GNU General Public License for more details.</span> +<span class="c"> *</span> +<span class="c"> * You should have received a copy of the GNU General Public License</span> +<span class="c"> * along with this program. If not, see <https://www.gnu.org/licenses/>.</span> +<span class="c"> *)</span> + +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">From</span> compcert <span class="kn">Require Import</span> Maps.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">From</span> compcert <span class="kn">Require</span> Errors Globalenvs Integers.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">From</span> compcert <span class="kn">Require Import</span> AST RTL.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">From</span> vericert <span class="kn">Require Import</span> Verilog HTL Vericertlib AssocMap ValueInt Statemonad.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Hint Resolve</span> AssocMap.gempty : htlh.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Hint Resolve</span> AssocMap.gso : htlh.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Hint Resolve</span> AssocMap.gss : htlh.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Hint Resolve</span> Ple_refl : htlh.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Hint Resolve</span> Ple_succ : htlh.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Record</span> <span class="nf">state</span>: <span class="kt">Type</span> := 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; +}.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">init_state</span> (<span class="nv">st</span> : reg) : state := + mkstate st + <span class="mi">1</span>%positive + <span class="mi">1</span>%positive + (AssocMap.empty (option io * scl_decl)) + (AssocMap.empty (option io * arr_decl)) + (AssocMap.empty stmnt) + (AssocMap.empty stmnt).</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Module</span> <span class="nf">HTLState</span> <: State.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">st</span> := state.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Inductive</span> <span class="nf">st_incr</span>: state -> state -> <span class="kt">Prop</span> := + state_incr_intro: + <span class="kr">forall</span> (<span class="nv">s1</span> <span class="nv">s2</span>: state), + st_st s1 = st_st s2 -> + Ple s1.(st_freshreg) s2.(st_freshreg) -> + Ple s1.(st_freshstate) s2.(st_freshstate) -> + (<span class="kr">forall</span> <span class="nv">n</span>, + s1.(st_datapath)!n = None \/ s2.(st_datapath)!n = s1.(st_datapath)!n) -> + (<span class="kr">forall</span> <span class="nv">n</span>, + s1.(st_controllogic)!n = None + \/ s2.(st_controllogic)!n = s1.(st_controllogic)!n) -> + st_incr s1 s2.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Hint Constructors</span> st_incr : htlh.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">st_prop</span> := st_incr.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Hint Unfold</span> st_prop : htlh.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk0" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk0"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">st_refl</span> : <span class="kr">forall</span> <span class="nv">s</span>, st_prop s s.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> <span class="nv">s</span> : state, st_prop s s</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk1" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk1"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> <span class="nv">s</span> : state, st_prop s s</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="nb">auto with</span> htlh.</span></span><span class="coq-wsp"> </span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Qed</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk2" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk2"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">st_trans</span> : + <span class="kr">forall</span> <span class="nv">s1</span> <span class="nv">s2</span> <span class="nv">s3</span>, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> <span class="nv">s1</span> <span class="nv">s2</span> <span class="nv">s3</span> : state, +st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk3" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk3"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> <span class="nv">s1</span> <span class="nv">s2</span> <span class="nv">s3</span> : state, +st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk4" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk4"><span class="highlight"><span class="nb">intros</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">s1, s2, s3</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">state</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">st_prop s1 s2</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">st_prop s2 s3</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">st_prop s1 s3</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk5" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk5"><span class="highlight">inv H.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">s1, s2, s3</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">state</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">st_prop s2 s3</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H1</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">st_st s1 = st_st s2</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H2</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Ple (st_freshreg s1) (st_freshreg s2)</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H3</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Ple (st_freshstate s1) (st_freshstate s2)</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H4</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">n</span> : positive, +(st_datapath s1) ! n = None \/ +(st_datapath s2) ! n = (st_datapath s1) ! n</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H5</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">n</span> : positive, +(st_controllogic s1) ! n = None \/ +(st_controllogic s2) ! n = +(st_controllogic s1) ! n</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">st_prop s1 s3</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk6" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk6"><span class="highlight">inv H0.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">s1, s2, s3</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">state</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H1</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">st_st s1 = st_st s2</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H2</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Ple (st_freshreg s1) (st_freshreg s2)</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H3</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Ple (st_freshstate s1) (st_freshstate s2)</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H4</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">n</span> : positive, +(st_datapath s1) ! n = None \/ +(st_datapath s2) ! n = (st_datapath s1) ! n</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H5</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">n</span> : positive, +(st_controllogic s1) ! n = None \/ +(st_controllogic s2) ! n = +(st_controllogic s1) ! n</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">st_st s2 = st_st s3</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H6</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Ple (st_freshreg s2) (st_freshreg s3)</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H7</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Ple (st_freshstate s2) (st_freshstate s3)</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H8</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">n</span> : positive, +(st_datapath s2) ! n = None \/ +(st_datapath s3) ! n = (st_datapath s2) ! n</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H9</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">n</span> : positive, +(st_controllogic s2) ! n = None \/ +(st_controllogic s3) ! n = +(st_controllogic s2) ! n</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">st_prop s1 s3</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk7" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk7"><span class="highlight"><span class="nb">apply</span> state_incr_intro; <span class="nb">eauto using</span> Ple_trans; <span class="nb">intros</span>; <span class="kp">try</span> <span class="bp">congruence</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">s1, s2, s3</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">state</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H1</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">st_st s1 = st_st s2</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H2</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Ple (st_freshreg s1) (st_freshreg s2)</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H3</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Ple (st_freshstate s1) (st_freshstate s2)</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H4</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">n</span> : positive, +(st_datapath s1) ! n = None \/ +(st_datapath s2) ! n = (st_datapath s1) ! n</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H5</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">n</span> : positive, +(st_controllogic s1) ! n = None \/ +(st_controllogic s2) ! n = +(st_controllogic s1) ! n</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">st_st s2 = st_st s3</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H6</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Ple (st_freshreg s2) (st_freshreg s3)</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H7</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Ple (st_freshstate s2) (st_freshstate s3)</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H8</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">n</span> : positive, +(st_datapath s2) ! n = None \/ +(st_datapath s3) ! n = (st_datapath s2) ! n</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H9</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">n</span> : positive, +(st_controllogic s2) ! n = None \/ +(st_controllogic s3) ! n = +(st_controllogic s2) ! n</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">(st_datapath s1) ! n = None \/ +(st_datapath s3) ! n = (st_datapath s1) ! n</span></div></blockquote><div class="coq-extra-goals"><input class="coq-extra-goal-toggle" id="htlgen-v-chk8" style="display: none" type="checkbox"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">s1, s2, s3</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">state</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H1</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">st_st s1 = st_st s2</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H2</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Ple (st_freshreg s1) (st_freshreg s2)</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H3</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Ple (st_freshstate s1) (st_freshstate s2)</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H4</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">n</span> : positive, +(st_datapath s1) ! n = None \/ +(st_datapath s2) ! n = (st_datapath s1) ! n</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H5</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">n</span> : positive, +(st_controllogic s1) ! n = None \/ +(st_controllogic s2) ! n = +(st_controllogic s1) ! n</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">st_st s2 = st_st s3</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H6</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Ple (st_freshreg s2) (st_freshreg s3)</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H7</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Ple (st_freshstate s2) (st_freshstate s3)</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H8</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">n</span> : positive, +(st_datapath s2) ! n = None \/ +(st_datapath s3) ! n = (st_datapath s2) ! n</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H9</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">n</span> : positive, +(st_controllogic s2) ! n = None \/ +(st_controllogic s3) ! n = +(st_controllogic s2) ! n</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div></div><label class="goal-separator coq-extra-goal-label" for="htlgen-v-chk8"><hr></label><div class="goal-conclusion"><span class="highlight">(st_controllogic s1) ! n = None \/ +(st_controllogic s3) ! n = (st_controllogic s1) ! n</span></div></blockquote></div></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk9" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk9"><span class="highlight">-</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">s1, s2, s3</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">state</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H1</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">st_st s1 = st_st s2</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H2</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Ple (st_freshreg s1) (st_freshreg s2)</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H3</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Ple (st_freshstate s1) (st_freshstate s2)</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H4</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">n</span> : positive, +(st_datapath s1) ! n = None \/ +(st_datapath s2) ! n = (st_datapath s1) ! n</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H5</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">n</span> : positive, +(st_controllogic s1) ! n = None \/ +(st_controllogic s2) ! n = +(st_controllogic s1) ! n</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">st_st s2 = st_st s3</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H6</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Ple (st_freshreg s2) (st_freshreg s3)</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H7</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Ple (st_freshstate s2) (st_freshstate s3)</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H8</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">n</span> : positive, +(st_datapath s2) ! n = None \/ +(st_datapath s3) ! n = (st_datapath s2) ! n</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H9</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">n</span> : positive, +(st_controllogic s2) ! n = None \/ +(st_controllogic s3) ! n = +(st_controllogic s2) ! n</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">(st_datapath s1) ! n = None \/ +(st_datapath s3) ! n = (st_datapath s1) ! n</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="nb">destruct</span> H4 <span class="kr">with</span> n; <span class="nb">destruct</span> H8 <span class="kr">with</span> n; <span class="nb">intuition</span> <span class="bp">congruence</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chka" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chka"><span class="highlight">-</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">s1, s2, s3</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">state</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H1</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">st_st s1 = st_st s2</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H2</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Ple (st_freshreg s1) (st_freshreg s2)</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H3</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Ple (st_freshstate s1) (st_freshstate s2)</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H4</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">n</span> : positive, +(st_datapath s1) ! n = None \/ +(st_datapath s2) ! n = (st_datapath s1) ! n</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H5</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">n</span> : positive, +(st_controllogic s1) ! n = None \/ +(st_controllogic s2) ! n = +(st_controllogic s1) ! n</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">st_st s2 = st_st s3</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H6</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Ple (st_freshreg s2) (st_freshreg s3)</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H7</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Ple (st_freshstate s2) (st_freshstate s3)</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H8</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">n</span> : positive, +(st_datapath s2) ! n = None \/ +(st_datapath s3) ! n = (st_datapath s2) ! n</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H9</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">n</span> : positive, +(st_controllogic s2) ! n = None \/ +(st_controllogic s3) ! n = +(st_controllogic s2) ! n</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">(st_controllogic s1) ! n = None \/ +(st_controllogic s3) ! n = (st_controllogic s1) ! n</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="nb">destruct</span> H5 <span class="kr">with</span> n; <span class="nb">destruct</span> H9 <span class="kr">with</span> n; <span class="nb">intuition</span> <span class="bp">congruence</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Qed</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">End</span> <span class="nf">HTLState</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Export</span> HTLState.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Module</span> <span class="nf">HTLMonad</span> := Statemonad(HTLState).</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Export</span> HTLMonad.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Module</span> <span class="nf">HTLMonadExtra</span> := Monad.MonadExtra(HTLMonad).</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Import</span> HTLMonadExtra.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Export</span> MonadNotation.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">state_goto</span> (<span class="nv">st</span> : reg) (<span class="nv">n</span> : node) : stmnt := + Vnonblock (Vvar st) (Vlit (posToValue n)).</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">state_cond</span> (<span class="nv">st</span> : reg) (<span class="nv">c</span> : expr) (<span class="nv">n1</span> <span class="nv">n2</span> : node) : stmnt := + Vnonblock (Vvar st) (Vternary c (posToExpr n1) (posToExpr n2)).</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chkb" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chkb"><span class="highlight"><span class="kn">Definition</span> <span class="nf">check_empty_node_datapath</span>: + <span class="kr">forall</span> (<span class="nv">s</span>: state) (<span class="nv">n</span>: node), { s.(st_datapath)!n = None } + { <span class="kt">True</span> }.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">s</span> : state) (<span class="nv">n</span> : node), +{(st_datapath s) ! n = None} + {<span class="kt">True</span>}</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chkc" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chkc"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">s</span> : state) (<span class="nv">n</span> : node), +{(st_datapath s) ! n = None} + {<span class="kt">True</span>}</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chkd" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chkd"><span class="highlight"><span class="nb">intros</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">s</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">state</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">node</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">{(st_datapath s) ! n = None} + {<span class="kt">True</span>}</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="nb">case</span> (s.(st_datapath)!n); <span class="bp">tauto</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Defined</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chke" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chke"><span class="highlight"><span class="kn">Definition</span> <span class="nf">check_empty_node_controllogic</span>: + <span class="kr">forall</span> (<span class="nv">s</span>: state) (<span class="nv">n</span>: node), { s.(st_controllogic)!n = None } + { <span class="kt">True</span> }.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">s</span> : state) (<span class="nv">n</span> : node), +{(st_controllogic s) ! n = None} + {<span class="kt">True</span>}</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chkf" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chkf"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">s</span> : state) (<span class="nv">n</span> : node), +{(st_controllogic s) ! n = None} + {<span class="kt">True</span>}</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk10" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk10"><span class="highlight"><span class="nb">intros</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">s</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">state</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">node</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">{(st_controllogic s) ! n = None} + {<span class="kt">True</span>}</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="nb">case</span> (s.(st_controllogic)!n); <span class="bp">tauto</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Defined</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk11" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk11"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">add_instr_state_incr</span> : + <span class="kr">forall</span> <span class="nv">s</span> <span class="nv">n</span> <span class="nv">n'</span> <span class="nv">st</span>, + (st_datapath s)!n = None -> + (st_controllogic s)!n = None -> + st_incr s + (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.<span class="nb">set</span> n st s.(st_datapath)) + (AssocMap.<span class="nb">set</span> n (state_goto s.(st_st) n') s.(st_controllogic))).</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">s</span> : state) (<span class="nv">n</span> : positive) (<span class="nv">n'</span> : node) + (<span class="nv">st</span> : 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.<span class="nb">set</span> n st (st_datapath s); + st_controllogic := AssocMap.<span class="nb">set</span> n + (state_goto (st_st s) n') + (st_controllogic s) |}</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk12" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk12"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">s</span> : state) (<span class="nv">n</span> : positive) (<span class="nv">n'</span> : node) + (<span class="nv">st</span> : 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.<span class="nb">set</span> n st (st_datapath s); + st_controllogic := AssocMap.<span class="nb">set</span> n + (state_goto (st_st s) n') + (st_controllogic s) |}</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="nb">constructor</span>; <span class="nb">intros</span>; + <span class="kp">try</span> (<span class="nb">simpl</span>; <span class="nb">destruct</span> (peq n n0); <span class="nb">subst</span>); + <span class="nb">auto with</span> htlh.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Qed</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk13" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk13"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">declare_reg_state_incr</span> : + <span class="kr">forall</span> <span class="nv">i</span> <span class="nv">s</span> <span class="nv">r</span> <span class="nv">sz</span>, + st_incr s + (mkstate + s.(st_st) + s.(st_freshreg) + s.(st_freshstate) + (AssocMap.<span class="nb">set</span> r (i, VScalar sz) s.(st_scldecls)) + s.(st_arrdecls) + s.(st_datapath) + s.(st_controllogic)).</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">i</span> : option io) (<span class="nv">s</span> : state) (<span class="nv">r</span> : positive) + (<span class="nv">sz</span> : nat), +st_incr s + {| + st_st := st_st s; + st_freshreg := st_freshreg s; + st_freshstate := st_freshstate s; + st_scldecls := AssocMap.<span class="nb">set</span> r (i, VScalar sz) + (st_scldecls s); + st_arrdecls := st_arrdecls s; + st_datapath := st_datapath s; + st_controllogic := st_controllogic s |}</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk14" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk14"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">i</span> : option io) (<span class="nv">s</span> : state) (<span class="nv">r</span> : positive) + (<span class="nv">sz</span> : nat), +st_incr s + {| + st_st := st_st s; + st_freshreg := st_freshreg s; + st_freshstate := st_freshstate s; + st_scldecls := AssocMap.<span class="nb">set</span> r (i, VScalar sz) + (st_scldecls s); + st_arrdecls := st_arrdecls s; + st_datapath := st_datapath s; + st_controllogic := st_controllogic s |}</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="nb">auto with</span> htlh.</span></span><span class="coq-wsp"> </span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Qed</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">declare_reg</span> (<span class="nv">i</span> : option io) (<span class="nv">r</span> : reg) (<span class="nv">sz</span> : nat) : mon unit := + <span class="kr">fun</span> <span class="nv">s</span> => OK tt (mkstate + s.(st_st) + s.(st_freshreg) + s.(st_freshstate) + (AssocMap.<span class="nb">set</span> r (i, VScalar sz) s.(st_scldecls)) + s.(st_arrdecls) + s.(st_datapath) + s.(st_controllogic)) + (declare_reg_state_incr i s r sz).</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">add_instr</span> (<span class="nv">n</span> : node) (<span class="nv">n'</span> : node) (<span class="nv">st</span> : stmnt) : mon unit := + <span class="kr">fun</span> <span class="nv">s</span> => + <span class="kr">match</span> check_empty_node_datapath s n, check_empty_node_controllogic s n <span class="kr">with</span> + | <span class="nb">left</span> STM, <span class="nb">left</span> TRANS => + OK tt (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.<span class="nb">set</span> n st s.(st_datapath)) + (AssocMap.<span class="nb">set</span> n (state_goto s.(st_st) n') s.(st_controllogic))) + (add_instr_state_incr s n n' st STM TRANS) + | _, _ => Error (Errors.msg <span class="s2">"HTL.add_instr"</span>) + <span class="kr">end</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk15" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk15"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">add_instr_skip_state_incr</span> : + <span class="kr">forall</span> <span class="nv">s</span> <span class="nv">n</span> <span class="nv">st</span>, + (st_datapath s)!n = None -> + (st_controllogic s)!n = None -> + st_incr s + (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.<span class="nb">set</span> n st s.(st_datapath)) + (AssocMap.<span class="nb">set</span> n Vskip s.(st_controllogic))).</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">s</span> : state) (<span class="nv">n</span> : positive) (<span class="nv">st</span> : 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.<span class="nb">set</span> n st (st_datapath s); + st_controllogic := AssocMap.<span class="nb">set</span> n Vskip + (st_controllogic s) |}</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk16" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk16"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">s</span> : state) (<span class="nv">n</span> : positive) (<span class="nv">st</span> : 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.<span class="nb">set</span> n st (st_datapath s); + st_controllogic := AssocMap.<span class="nb">set</span> n Vskip + (st_controllogic s) |}</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="nb">constructor</span>; <span class="nb">intros</span>; + <span class="kp">try</span> (<span class="nb">simpl</span>; <span class="nb">destruct</span> (peq n n0); <span class="nb">subst</span>); + <span class="nb">auto with</span> htlh.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Qed</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">add_instr_skip</span> (<span class="nv">n</span> : node) (<span class="nv">st</span> : stmnt) : mon unit := + <span class="kr">fun</span> <span class="nv">s</span> => + <span class="kr">match</span> check_empty_node_datapath s n, check_empty_node_controllogic s n <span class="kr">with</span> + | <span class="nb">left</span> STM, <span class="nb">left</span> TRANS => + OK tt (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.<span class="nb">set</span> n st s.(st_datapath)) + (AssocMap.<span class="nb">set</span> n Vskip s.(st_controllogic))) + (add_instr_skip_state_incr s n st STM TRANS) + | _, _ => Error (Errors.msg <span class="s2">"HTL.add_instr"</span>) + <span class="kr">end</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk17" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk17"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">add_node_skip_state_incr</span> : + <span class="kr">forall</span> <span class="nv">s</span> <span class="nv">n</span> <span class="nv">st</span>, + (st_datapath s)!n = None -> + (st_controllogic s)!n = None -> + st_incr s + (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.<span class="nb">set</span> n Vskip s.(st_datapath)) + (AssocMap.<span class="nb">set</span> n st s.(st_controllogic))).</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">s</span> : state) (<span class="nv">n</span> : positive) (<span class="nv">st</span> : 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.<span class="nb">set</span> n Vskip (st_datapath s); + st_controllogic := AssocMap.<span class="nb">set</span> n st + (st_controllogic s) |}</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk18" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk18"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">s</span> : state) (<span class="nv">n</span> : positive) (<span class="nv">st</span> : 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.<span class="nb">set</span> n Vskip (st_datapath s); + st_controllogic := AssocMap.<span class="nb">set</span> n st + (st_controllogic s) |}</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="nb">constructor</span>; <span class="nb">intros</span>; + <span class="kp">try</span> (<span class="nb">simpl</span>; <span class="nb">destruct</span> (peq n n0); <span class="nb">subst</span>); + <span class="nb">auto with</span> htlh.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Qed</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">add_node_skip</span> (<span class="nv">n</span> : node) (<span class="nv">st</span> : stmnt) : mon unit := + <span class="kr">fun</span> <span class="nv">s</span> => + <span class="kr">match</span> check_empty_node_datapath s n, check_empty_node_controllogic s n <span class="kr">with</span> + | <span class="nb">left</span> STM, <span class="nb">left</span> TRANS => + OK tt (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.<span class="nb">set</span> n Vskip s.(st_datapath)) + (AssocMap.<span class="nb">set</span> n st s.(st_controllogic))) + (add_node_skip_state_incr s n st STM TRANS) + | _, _ => Error (Errors.msg <span class="s2">"HTL.add_instr"</span>) + <span class="kr">end</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">nonblock</span> (<span class="nv">dst</span> : reg) (<span class="nv">e</span> : expr) := Vnonblock (Vvar dst) e.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">block</span> (<span class="nv">dst</span> : reg) (<span class="nv">e</span> : expr) := Vblock (Vvar dst) e.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">bop</span> (<span class="nv">op</span> : binop) (<span class="nv">r1</span> <span class="nv">r2</span> : reg) : expr := + Vbinop op (Vvar r1) (Vvar r2).</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">boplit</span> (<span class="nv">op</span> : binop) (<span class="nv">r</span> : reg) (<span class="nv">l</span> : Integers.int) : expr := + Vbinop op (Vvar r) (Vlit (intToValue l)).</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">boplitz</span> (<span class="nv">op</span>: binop) (<span class="nv">r</span>: reg) (<span class="nv">l</span>: Z) : expr := + Vbinop op (Vvar r) (Vlit (ZToValue l)).</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">translate_comparison</span> (<span class="nv">c</span> : Integers.comparison) (<span class="nv">args</span> : list reg) : mon expr := + <span class="kr">match</span> c, args <span class="kr">with</span> + | 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 <span class="s2">"Htlgen: comparison instruction not implemented: other"</span>) + <span class="kr">end</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">translate_comparison_imm</span> (<span class="nv">c</span> : Integers.comparison) (<span class="nv">args</span> : list reg) (<span class="nv">i</span>: Integers.int) + : mon expr := + <span class="kr">match</span> c, args <span class="kr">with</span> + | 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 <span class="s2">"Htlgen: comparison_imm instruction not implemented: other"</span>) + <span class="kr">end</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">translate_comparisonu</span> (<span class="nv">c</span> : Integers.comparison) (<span class="nv">args</span> : list reg) : mon expr := + <span class="kr">match</span> c, args <span class="kr">with</span> + | 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 <span class="s2">"Htlgen: comparison instruction not implemented: other"</span>) + <span class="kr">end</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">translate_comparison_immu</span> (<span class="nv">c</span> : Integers.comparison) (<span class="nv">args</span> : list reg) (<span class="nv">i</span>: Integers.int) + : mon expr := + <span class="kr">match</span> c, args <span class="kr">with</span> + | 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 <span class="s2">"Htlgen: comparison_imm instruction not implemented: other"</span>) + <span class="kr">end</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">translate_condition</span> (<span class="nv">c</span> : Op.condition) (<span class="nv">args</span> : list reg) : mon expr := + <span class="kr">match</span> c, args <span class="kr">with</span> + | 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 <span class="s2">"Htlgen: condition instruction not implemented: Cmaskzero"</span>) + | Op.Cmasknotzero n, _ => error (Errors.msg <span class="s2">"Htlgen: condition instruction not implemented: Cmasknotzero"</span>) + | _, _ => error (Errors.msg <span class="s2">"Htlgen: condition instruction not implemented: other"</span>) + <span class="kr">end</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">check_address_parameter_signed</span> (<span class="nv">p</span> : Z) : bool := + Z.leb Integers.Ptrofs.min_signed p + && Z.leb p Integers.Ptrofs.max_signed.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">check_address_parameter_unsigned</span> (<span class="nv">p</span> : Z) : bool := + Z.leb p Integers.Ptrofs.max_unsigned.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">translate_eff_addressing</span> (<span class="nv">a</span>: Op.addressing) (<span class="nv">args</span>: list reg) : mon expr := + <span class="kr">match</span> a, args <span class="kr">with</span> <span class="c">(* TODO: We should be more methodical here; what are the possibilities?*)</span> + | Op.Aindexed off, r1::nil => + <span class="kr">if</span> (check_address_parameter_signed off) + <span class="kr">then</span> ret (boplitz Vadd r1 off) + <span class="kr">else</span> error (Errors.msg <span class="s2">"Veriloggen: translate_eff_addressing (Aindexed): address out of bounds"</span>) + | Op.Ascaled scale offset, r1::nil => + <span class="kr">if</span> (check_address_parameter_signed scale) && (check_address_parameter_signed offset) + <span class="kr">then</span> ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue offset))) + <span class="kr">else</span> error (Errors.msg <span class="s2">"Veriloggen: translate_eff_addressing (Ascaled): address out of bounds"</span>) + | Op.Aindexed2 offset, r1::r2::nil => + <span class="kr">if</span> (check_address_parameter_signed offset) + <span class="kr">then</span> ret (Vbinop Vadd (bop Vadd r1 r2) (Vlit (ZToValue offset))) + <span class="kr">else</span> error (Errors.msg <span class="s2">"Veriloggen: translate_eff_addressing (Aindexed2): address out of bounds"</span>) + | Op.Aindexed2scaled scale offset, r1::r2::nil => <span class="c">(* Typical for dynamic array addressing *)</span> + <span class="kr">if</span> (check_address_parameter_signed scale) && (check_address_parameter_signed offset) + <span class="kr">then</span> ret (Vbinop Vadd (Vvar r1) (Vbinop Vadd (boplitz Vmul r2 scale) (Vlit (ZToValue offset)))) + <span class="kr">else</span> error (Errors.msg <span class="s2">"Veriloggen: translate_eff_addressing (Aindexed2scaled): address out of bounds"</span>) + | Op.Ainstack a, nil => <span class="c">(* We need to be sure that the base address is aligned *)</span> + <span class="kr">let</span> <span class="nv">a</span> := Integers.Ptrofs.unsigned a <span class="kr">in</span> + <span class="kr">if</span> (check_address_parameter_unsigned a) + <span class="kr">then</span> ret (Vlit (ZToValue a)) + <span class="kr">else</span> error (Errors.msg <span class="s2">"Veriloggen: translate_eff_addressing (Ainstack): address out of bounds"</span>) + | _, _ => error (Errors.msg <span class="s2">"Veriloggen: translate_eff_addressing unsuported addressing"</span>) + <span class="kr">end</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +<span class="sd">(** Translate an instruction to a statement. FIX mulhs mulhu *)</span> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">translate_instr</span> (<span class="nv">op</span> : Op.operation) (<span class="nv">args</span> : list reg) : mon expr := + <span class="kr">match</span> op, args <span class="kr">with</span> + | 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 <span class="s2">"Htlgen: Instruction not implemented: mulhs"</span>) + | Op.Omulhu, r1::r2::nil => error (Errors.msg <span class="s2">"Htlgen: Instruction not implemented: mulhu"</span>) + | 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 <span class="mi">0</span>))) + (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 <span class="s2">"Htlgen: Instruction not implemented: Ororimm"</span>) + <span class="c">(*ret (Vbinop Vor (boplit Vshru r (Integers.Int.modu n (Integers.Int.repr 32)))</span> +<span class="c"> (boplit Vshl r (Integers.Int.sub (Integers.Int.repr 32) (Integers.Int.modu n (Integers.Int.repr 32)))))*)</span> + | Op.Oshldimm n, r::nil => ret (Vbinop Vor (boplit Vshl r n) (boplit Vshr r (Integers.Int.sub (Integers.Int.repr <span class="mi">32</span>) n))) + | Op.Ocmp c, _ => translate_condition c args + | Op.Osel c AST.Tint, r1::r2::rl => + <span class="kp">do</span> tc <- translate_condition c rl; + ret (Vternary tc (Vvar r1) (Vvar r2)) + | Op.Olea a, _ => translate_eff_addressing a args + | _, _ => error (Errors.msg <span class="s2">"Htlgen: Instruction not implemented: other"</span>) + <span class="kr">end</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk19" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk19"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">add_branch_instr_state_incr</span>: + <span class="kr">forall</span> <span class="nv">s</span> <span class="nv">e</span> <span class="nv">n</span> <span class="nv">n1</span> <span class="nv">n2</span>, + (st_datapath s) ! n = None -> + (st_controllogic s) ! n = None -> + st_incr s (mkstate + s.(st_st) + (st_freshreg s) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.<span class="nb">set</span> n Vskip (st_datapath s)) + (AssocMap.<span class="nb">set</span> n (state_cond s.(st_st) e n1 n2) (st_controllogic s))).</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">s</span> : state) (<span class="nv">e</span> : expr) (<span class="nv">n</span> : positive) + (<span class="nv">n1</span> <span class="nv">n2</span> : 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.<span class="nb">set</span> n Vskip (st_datapath s); + st_controllogic := AssocMap.<span class="nb">set</span> n + (state_cond (st_st s) e n1 n2) + (st_controllogic s) |}</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk1a" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk1a"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">s</span> : state) (<span class="nv">e</span> : expr) (<span class="nv">n</span> : positive) + (<span class="nv">n1</span> <span class="nv">n2</span> : 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.<span class="nb">set</span> n Vskip (st_datapath s); + st_controllogic := AssocMap.<span class="nb">set</span> n + (state_cond (st_st s) e n1 n2) + (st_controllogic s) |}</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk1b" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk1b"><span class="highlight"><span class="nb">intros</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">s</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">state</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">e</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">expr</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n1, n2</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">node</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">(st_datapath s) ! n = None</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">(st_controllogic s) ! n = None</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">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.<span class="nb">set</span> n Vskip (st_datapath s); + st_controllogic := AssocMap.<span class="nb">set</span> n + (state_cond (st_st s) e n1 n2) + (st_controllogic s) |}</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="nb">apply</span> state_incr_intro; <span class="nb">simpl</span>; + <span class="kp">try</span> (<span class="nb">intros</span>; <span class="nb">destruct</span> (peq n0 n); <span class="nb">subst</span>); + <span class="nb">auto with</span> htlh.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Qed</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">add_branch_instr</span> (<span class="nv">e</span>: expr) (<span class="nv">n</span> <span class="nv">n1</span> <span class="nv">n2</span>: node) : mon unit := + <span class="kr">fun</span> <span class="nv">s</span> => + <span class="kr">match</span> check_empty_node_datapath s n, check_empty_node_controllogic s n <span class="kr">with</span> + | <span class="nb">left</span> NSTM, <span class="nb">left</span> NTRANS => + OK tt (mkstate + s.(st_st) + (st_freshreg s) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.<span class="nb">set</span> n Vskip (st_datapath s)) + (AssocMap.<span class="nb">set</span> 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 <span class="s2">"Htlgen: add_branch_instr"</span>) + <span class="kr">end</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">translate_arr_access</span> (<span class="nv">mem</span> : AST.memory_chunk) (<span class="nv">addr</span> : Op.addressing) + (<span class="nv">args</span> : list reg) (<span class="nv">stack</span> : reg) : mon expr := + <span class="kr">match</span> mem, addr, args <span class="kr">with</span> <span class="c">(* TODO: We should be more methodical here; what are the possibilities?*)</span> + | Mint32, Op.Aindexed off, r1::nil => + <span class="kr">if</span> (check_address_parameter_signed off) + <span class="kr">then</span> ret (Vvari stack (Vbinop Vdivu (boplitz Vadd r1 off) (Vlit (ZToValue <span class="mi">4</span>)))) + <span class="kr">else</span> error (Errors.msg <span class="s2">"HTLgen: translate_arr_access address out of bounds"</span>) + | Mint32, Op.Aindexed2scaled scale offset, r1::r2::nil => <span class="c">(* Typical for dynamic array addressing *)</span> + <span class="kr">if</span> (check_address_parameter_signed scale) && (check_address_parameter_signed offset) + <span class="kr">then</span> ret (Vvari stack + (Vbinop Vdivu + (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) + (Vlit (ZToValue <span class="mi">4</span>)))) + <span class="kr">else</span> error (Errors.msg <span class="s2">"HTLgen: translate_arr_access address out of bounds"</span>) + | Mint32, Op.Ainstack a, nil => <span class="c">(* We need to be sure that the base address is aligned *)</span> + <span class="kr">let</span> <span class="nv">a</span> := Integers.Ptrofs.unsigned a <span class="kr">in</span> + <span class="kr">if</span> (check_address_parameter_unsigned a) + <span class="kr">then</span> ret (Vvari stack (Vlit (ZToValue (a / <span class="mi">4</span>)))) + <span class="kr">else</span> error (Errors.msg <span class="s2">"HTLgen: eff_addressing out of bounds stack offset"</span>) + | _, _, _ => error (Errors.msg <span class="s2">"HTLgen: translate_arr_access unsuported addressing"</span>) + <span class="kr">end</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Fixpoint</span> <span class="nf">enumerate</span> (<span class="nv">i</span> : nat) (<span class="nv">ns</span> : list node) {<span class="nv">struct</span> <span class="nv">ns</span>} : list (nat * node) := + <span class="kr">match</span> ns <span class="kr">with</span> + | n :: ns' => (i, n) :: enumerate (i+<span class="mi">1</span>) ns' + | nil => nil + <span class="kr">end</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">tbl_to_case_expr</span> (<span class="nv">st</span> : reg) (<span class="nv">ns</span> : list node) : list (expr * stmnt) := + List.map (<span class="kr">fun</span> <span class="nv">a</span> => <span class="kr">match</span> a <span class="kr">with</span> + (i, n) => (Vlit (natToValue i), Vnonblock (Vvar st) (Vlit (posToValue n))) + <span class="kr">end</span>) + (enumerate <span class="mi">0</span> ns).</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">transf_instr</span> (<span class="nv">fin</span> <span class="nv">rtrn</span> <span class="nv">stack</span>: reg) (<span class="nv">ni</span>: node * instruction) : mon unit := + <span class="kr">match</span> ni <span class="kr">with</span> + (n, i) => + <span class="kr">match</span> i <span class="kr">with</span> + | Inop n' => + <span class="kr">if</span> Z.leb (Z.pos n') Integers.Int.max_unsigned <span class="kr">then</span> + add_instr n n' Vskip + <span class="kr">else</span> error (Errors.msg <span class="s2">"State is larger than 2^32."</span>) + | Iop op args dst n' => + <span class="kr">if</span> Z.leb (Z.pos n') Integers.Int.max_unsigned <span class="kr">then</span> + <span class="kp">do</span> instr <- translate_instr op args; + <span class="kp">do</span> _ <- declare_reg None dst <span class="mi">32</span>; + add_instr n n' (nonblock dst instr) + <span class="kr">else</span> error (Errors.msg <span class="s2">"State is larger than 2^32."</span>) + | Iload mem addr args dst n' => + <span class="kr">if</span> Z.leb (Z.pos n') Integers.Int.max_unsigned <span class="kr">then</span> + <span class="kp">do</span> src <- translate_arr_access mem addr args stack; + <span class="kp">do</span> _ <- declare_reg None dst <span class="mi">32</span>; + add_instr n n' (nonblock dst src) + <span class="kr">else</span> error (Errors.msg <span class="s2">"State is larger than 2^32."</span>) + | Istore mem addr args src n' => + <span class="kr">if</span> Z.leb (Z.pos n') Integers.Int.max_unsigned <span class="kr">then</span> + <span class="kp">do</span> dst <- translate_arr_access mem addr args stack; + add_instr n n' (Vnonblock dst (Vvar src)) <span class="c">(* TODO: Could juse use add_instr? reg exists. *)</span> + <span class="kr">else</span> error (Errors.msg <span class="s2">"State is larger than 2^32."</span>) + | Icall _ _ _ _ _ => error (Errors.msg <span class="s2">"Calls are not implemented."</span>) + | Itailcall _ _ _ => error (Errors.msg <span class="s2">"Tailcalls are not implemented."</span>) + | Ibuiltin _ _ _ _ => error (Errors.msg <span class="s2">"Builtin functions not implemented."</span>) + | Icond cond args n1 n2 => + <span class="kr">if</span> Z.leb (Z.pos n1) Integers.Int.max_unsigned && Z.leb (Z.pos n2) Integers.Int.max_unsigned <span class="kr">then</span> + <span class="kp">do</span> e <- translate_condition cond args; + add_branch_instr e n n1 n2 + <span class="kr">else</span> error (Errors.msg <span class="s2">"State is larger than 2^32."</span>) + | Ijumptable r tbl => + <span class="c">(*do s <- get;</span> +<span class="c"> add_node_skip n (Vcase (Vvar r) (tbl_to_case_expr s.(st_st) tbl) (Some Vskip))*)</span> + error (Errors.msg <span class="s2">"Ijumptable: Case statement not supported."</span>) + | Ireturn r => + <span class="kr">match</span> r <span class="kr">with</span> + | Some r' => + add_instr_skip n (Vseq (block fin (Vlit (ZToValue <span class="mi">1</span>%Z))) (block rtrn (Vvar r'))) + | None => + add_instr_skip n (Vseq (block fin (Vlit (ZToValue <span class="mi">1</span>%Z))) (block rtrn (Vlit (ZToValue <span class="mi">0</span>%Z)))) + <span class="kr">end</span> + <span class="kr">end</span> + <span class="kr">end</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk1c" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk1c"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">create_reg_state_incr</span>: + <span class="kr">forall</span> <span class="nv">s</span> <span class="nv">sz</span> <span class="nv">i</span>, + st_incr s (mkstate + s.(st_st) + (Pos.succ (st_freshreg s)) + (st_freshstate s) + (AssocMap.<span class="nb">set</span> s.(st_freshreg) (i, VScalar sz) s.(st_scldecls)) + s.(st_arrdecls) + (st_datapath s) + (st_controllogic s)).</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">s</span> : state) (<span class="nv">sz</span> : nat) (<span class="nv">i</span> : option io), +st_incr s + {| + st_st := st_st s; + st_freshreg := Pos.succ (st_freshreg s); + st_freshstate := st_freshstate s; + st_scldecls := AssocMap.<span class="nb">set</span> (st_freshreg s) + (i, VScalar sz) (st_scldecls s); + st_arrdecls := st_arrdecls s; + st_datapath := st_datapath s; + st_controllogic := st_controllogic s |}</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk1d" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk1d"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">s</span> : state) (<span class="nv">sz</span> : nat) (<span class="nv">i</span> : option io), +st_incr s + {| + st_st := st_st s; + st_freshreg := Pos.succ (st_freshreg s); + st_freshstate := st_freshstate s; + st_scldecls := AssocMap.<span class="nb">set</span> (st_freshreg s) + (i, VScalar sz) (st_scldecls s); + st_arrdecls := st_arrdecls s; + st_datapath := st_datapath s; + st_controllogic := st_controllogic s |}</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="nb">constructor</span>; <span class="nb">simpl</span>; <span class="nb">auto with</span> htlh.</span></span><span class="coq-wsp"> </span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Qed</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">create_reg</span> (<span class="nv">i</span> : option io) (<span class="nv">sz</span> : nat) : mon reg := + <span class="kr">fun</span> <span class="nv">s</span> => <span class="kr">let</span> <span class="nv">r</span> := s.(st_freshreg) <span class="kr">in</span> + OK r (mkstate + s.(st_st) + (Pos.succ r) + (st_freshstate s) + (AssocMap.<span class="nb">set</span> s.(st_freshreg) (i, VScalar sz) s.(st_scldecls)) + (st_arrdecls s) + (st_datapath s) + (st_controllogic s)) + (create_reg_state_incr s sz i).</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk1e" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk1e"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">create_arr_state_incr</span>: + <span class="kr">forall</span> <span class="nv">s</span> <span class="nv">sz</span> <span class="nv">ln</span> <span class="nv">i</span>, + st_incr s (mkstate + s.(st_st) + (Pos.succ (st_freshreg s)) + (st_freshstate s) + s.(st_scldecls) + (AssocMap.<span class="nb">set</span> s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls)) + (st_datapath s) + (st_controllogic s)).</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">s</span> : state) (<span class="nv">sz</span> <span class="nv">ln</span> : nat) (<span class="nv">i</span> : option io), +st_incr s + {| + st_st := st_st s; + st_freshreg := Pos.succ (st_freshreg s); + st_freshstate := st_freshstate s; + st_scldecls := st_scldecls s; + st_arrdecls := AssocMap.<span class="nb">set</span> (st_freshreg s) + (i, VArray sz ln) (st_arrdecls s); + st_datapath := st_datapath s; + st_controllogic := st_controllogic s |}</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk1f" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk1f"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">s</span> : state) (<span class="nv">sz</span> <span class="nv">ln</span> : nat) (<span class="nv">i</span> : option io), +st_incr s + {| + st_st := st_st s; + st_freshreg := Pos.succ (st_freshreg s); + st_freshstate := st_freshstate s; + st_scldecls := st_scldecls s; + st_arrdecls := AssocMap.<span class="nb">set</span> (st_freshreg s) + (i, VArray sz ln) (st_arrdecls s); + st_datapath := st_datapath s; + st_controllogic := st_controllogic s |}</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="nb">constructor</span>; <span class="nb">simpl</span>; <span class="nb">auto with</span> htlh.</span></span><span class="coq-wsp"> </span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Qed</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">create_arr</span> (<span class="nv">i</span> : option io) (<span class="nv">sz</span> : nat) (<span class="nv">ln</span> : nat) : mon (reg * nat) := + <span class="kr">fun</span> <span class="nv">s</span> => <span class="kr">let</span> <span class="nv">r</span> := s.(st_freshreg) <span class="kr">in</span> + OK (r, ln) (mkstate + s.(st_st) + (Pos.succ r) + (st_freshstate s) + s.(st_scldecls) + (AssocMap.<span class="nb">set</span> s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls)) + (st_datapath s) + (st_controllogic s)) + (create_arr_state_incr s sz ln i).</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">stack_correct</span> (<span class="nv">sz</span> : Z) : bool := + (<span class="mi">0</span> <=? sz) && (sz <? Integers.Ptrofs.modulus) && (Z.modulo sz <span class="mi">4</span> =? <span class="mi">0</span>).</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">max_pc_map</span> (<span class="nv">m</span> : Maps.PTree.t stmnt) := + PTree.<span class="nb">fold</span> (<span class="kr">fun</span> <span class="nv">m</span> <span class="nv">pc</span> <span class="nv">i</span> => Pos.max m pc) m <span class="mi">1</span>%positive.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk20" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk20"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">max_pc_map_sound</span>: + <span class="kr">forall</span> <span class="nv">m</span> <span class="nv">pc</span> <span class="nv">i</span>, m!pc = Some i -> Ple pc (max_pc_map m).</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">m</span> : PTree.t stmnt) (<span class="nv">pc</span> : positive) (<span class="nv">i</span> : stmnt), +m ! pc = Some i -> Ple pc (max_pc_map m)</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk21" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk21"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">m</span> : PTree.t stmnt) (<span class="nv">pc</span> : positive) (<span class="nv">i</span> : stmnt), +m ! pc = Some i -> Ple pc (max_pc_map m)</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk22" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk22"><span class="highlight"><span class="nb">intros until</span> i.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">m</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">pc</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">m ! pc = Some i -> Ple pc (max_pc_map m)</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk23" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk23"><span class="highlight"><span class="nb">unfold</span> max_pc_function.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">m</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">pc</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">m ! pc = Some i -> Ple pc (max_pc_map m)</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk24" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk24"><span class="highlight"><span class="nb">apply</span> PTree_Properties.fold_rec <span class="kr">with</span> (P := <span class="kr">fun</span> <span class="nv">c</span> <span class="nv">m</span> => c!pc = Some i -> Ple pc m).</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">m</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">pc</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">m</span> <span class="nv">m'</span> : PTree.t stmnt) (<span class="nv">a</span> : positive), +(<span class="kr">forall</span> <span class="nv">x</span> : PTree.elt, m ! x = m' ! x) -> +(m ! pc = Some i -> Ple pc a) -> +m' ! pc = Some i -> Ple pc a</span></div></blockquote><div class="coq-extra-goals"><input class="coq-extra-goal-toggle" id="htlgen-v-chk25" style="display: none" type="checkbox"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">m</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">pc</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div></div><label class="goal-separator coq-extra-goal-label" for="htlgen-v-chk25"><hr></label><div class="goal-conclusion"><span class="highlight">(PTree.empty stmnt) ! pc = Some i -> Ple pc <span class="mi">1</span></span></div></blockquote><input class="coq-extra-goal-toggle" id="htlgen-v-chk26" style="display: none" type="checkbox"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">m</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">pc</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div></div><label class="goal-separator coq-extra-goal-label" for="htlgen-v-chk26"><hr></label><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">m0</span> : PTree.t stmnt) (<span class="nv">a</span> : positive) + (<span class="nv">k</span> : PTree.elt) (<span class="nv">v</span> : stmnt), +m0 ! k = None -> +m ! k = Some v -> +(m0 ! pc = Some i -> Ple pc a) -> +(PTree.<span class="nb">set</span> k v m0) ! pc = Some i -> +Ple pc (Pos.max a k)</span></div></blockquote></div></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> <span class="c">(* extensionality *)</span> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk27" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk27"><span class="highlight"><span class="nb">intros</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">m</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">pc</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">m0, m'</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">x</span> : PTree.elt, m0 ! x = m' ! x</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m0 ! pc = Some i -> Ple pc a</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H1</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m' ! pc = Some i</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">Ple pc a</span></div></blockquote><div class="coq-extra-goals"><input class="coq-extra-goal-toggle" id="htlgen-v-chk28" style="display: none" type="checkbox"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">m</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">pc</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div></div><label class="goal-separator coq-extra-goal-label" for="htlgen-v-chk28"><hr></label><div class="goal-conclusion"><span class="highlight">(PTree.empty stmnt) ! pc = Some i -> Ple pc <span class="mi">1</span></span></div></blockquote><input class="coq-extra-goal-toggle" id="htlgen-v-chk29" style="display: none" type="checkbox"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">m</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">pc</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div></div><label class="goal-separator coq-extra-goal-label" for="htlgen-v-chk29"><hr></label><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">m0</span> : PTree.t stmnt) (<span class="nv">a</span> : positive) + (<span class="nv">k</span> : PTree.elt) (<span class="nv">v</span> : stmnt), +m0 ! k = None -> +m ! k = Some v -> +(m0 ! pc = Some i -> Ple pc a) -> +(PTree.<span class="nb">set</span> k v m0) ! pc = Some i -> +Ple pc (Pos.max a k)</span></div></blockquote></div></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk2a" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk2a"><span class="highlight"><span class="nb">apply</span> H0.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">m</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">pc</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">m0, m'</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">x</span> : PTree.elt, m0 ! x = m' ! x</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m0 ! pc = Some i -> Ple pc a</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H1</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m' ! pc = Some i</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">m0 ! pc = Some i</span></div></blockquote><div class="coq-extra-goals"><input class="coq-extra-goal-toggle" id="htlgen-v-chk2b" style="display: none" type="checkbox"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">m</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">pc</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div></div><label class="goal-separator coq-extra-goal-label" for="htlgen-v-chk2b"><hr></label><div class="goal-conclusion"><span class="highlight">(PTree.empty stmnt) ! pc = Some i -> Ple pc <span class="mi">1</span></span></div></blockquote><input class="coq-extra-goal-toggle" id="htlgen-v-chk2c" style="display: none" type="checkbox"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">m</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">pc</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div></div><label class="goal-separator coq-extra-goal-label" for="htlgen-v-chk2c"><hr></label><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">m0</span> : PTree.t stmnt) (<span class="nv">a</span> : positive) + (<span class="nv">k</span> : PTree.elt) (<span class="nv">v</span> : stmnt), +m0 ! k = None -> +m ! k = Some v -> +(m0 ! pc = Some i -> Ple pc a) -> +(PTree.<span class="nb">set</span> k v m0) ! pc = Some i -> +Ple pc (Pos.max a k)</span></div></blockquote></div></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk2d" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk2d"><span class="highlight"><span class="nb">rewrite</span> H; <span class="nb">auto</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">m</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">pc</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">(PTree.empty stmnt) ! pc = Some i -> Ple pc <span class="mi">1</span></span></div></blockquote><div class="coq-extra-goals"><input class="coq-extra-goal-toggle" id="htlgen-v-chk2e" style="display: none" type="checkbox"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">m</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">pc</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div></div><label class="goal-separator coq-extra-goal-label" for="htlgen-v-chk2e"><hr></label><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">m0</span> : PTree.t stmnt) (<span class="nv">a</span> : positive) + (<span class="nv">k</span> : PTree.elt) (<span class="nv">v</span> : stmnt), +m0 ! k = None -> +m ! k = Some v -> +(m0 ! pc = Some i -> Ple pc a) -> +(PTree.<span class="nb">set</span> k v m0) ! pc = Some i -> +Ple pc (Pos.max a k)</span></div></blockquote></div></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> <span class="c">(* base case *)</span> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk2f" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk2f"><span class="highlight"><span class="nb">rewrite</span> PTree.gempty.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">m</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">pc</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">None = Some i -> Ple pc <span class="mi">1</span></span></div></blockquote><div class="coq-extra-goals"><input class="coq-extra-goal-toggle" id="htlgen-v-chk30" style="display: none" type="checkbox"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">m</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">pc</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div></div><label class="goal-separator coq-extra-goal-label" for="htlgen-v-chk30"><hr></label><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">m0</span> : PTree.t stmnt) (<span class="nv">a</span> : positive) + (<span class="nv">k</span> : PTree.elt) (<span class="nv">v</span> : stmnt), +m0 ! k = None -> +m ! k = Some v -> +(m0 ! pc = Some i -> Ple pc a) -> +(PTree.<span class="nb">set</span> k v m0) ! pc = Some i -> +Ple pc (Pos.max a k)</span></div></blockquote></div></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk31" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk31"><span class="highlight"><span class="bp">congruence</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">m</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">pc</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">m0</span> : PTree.t stmnt) (<span class="nv">a</span> : positive) + (<span class="nv">k</span> : PTree.elt) (<span class="nv">v</span> : stmnt), +m0 ! k = None -> +m ! k = Some v -> +(m0 ! pc = Some i -> Ple pc a) -> +(PTree.<span class="nb">set</span> k v m0) ! pc = Some i -> +Ple pc (Pos.max a k)</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> <span class="c">(* inductive case *)</span> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk32" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk32"><span class="highlight"><span class="nb">intros</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">m</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">pc</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">m0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">k</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.elt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">v</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m0 ! k = None</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m ! k = Some v</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H1</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m0 ! pc = Some i -> Ple pc a</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H2</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">(PTree.<span class="nb">set</span> k v m0) ! pc = Some i</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">Ple pc (Pos.max a k)</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk33" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk33"><span class="highlight"><span class="nb">rewrite</span> PTree.gsspec <span class="kr">in</span> H2.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">m</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">pc</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">m0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">k</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.elt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">v</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m0 ! k = None</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m ! k = Some v</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H1</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m0 ! pc = Some i -> Ple pc a</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H2</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">(<span class="kr">if</span> peq pc k <span class="kr">then</span> Some v <span class="kr">else</span> m0 ! pc) = Some i</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">Ple pc (Pos.max a k)</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk34" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk34"><span class="highlight"><span class="nb">destruct</span> (peq pc k).</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">m</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">pc</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">m0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">k</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.elt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">v</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m0 ! k = None</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m ! k = Some v</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H1</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m0 ! pc = Some i -> Ple pc a</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">e</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">pc = k</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H2</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Some v = Some i</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">Ple pc (Pos.max a k)</span></div></blockquote><div class="coq-extra-goals"><input class="coq-extra-goal-toggle" id="htlgen-v-chk35" style="display: none" type="checkbox"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">m</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">pc</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">m0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">k</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.elt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">v</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m0 ! k = None</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m ! k = Some v</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H1</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m0 ! pc = Some i -> Ple pc a</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">pc <> k</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H2</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m0 ! pc = Some i</span></span></span></span></div></div><label class="goal-separator coq-extra-goal-label" for="htlgen-v-chk35"><hr></label><div class="goal-conclusion"><span class="highlight">Ple pc (Pos.max a k)</span></div></blockquote></div></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk36" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk36"><span class="highlight">inv H2.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">m</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">m0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">k</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.elt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m0 ! k = None</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m ! k = Some i</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H1</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m0 ! k = Some i -> Ple k a</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">Ple k (Pos.max a k)</span></div></blockquote><div class="coq-extra-goals"><input class="coq-extra-goal-toggle" id="htlgen-v-chk37" style="display: none" type="checkbox"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">m</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">pc</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">m0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">k</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.elt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">v</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m0 ! k = None</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m ! k = Some v</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H1</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m0 ! pc = Some i -> Ple pc a</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">pc <> k</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H2</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m0 ! pc = Some i</span></span></span></span></div></div><label class="goal-separator coq-extra-goal-label" for="htlgen-v-chk37"><hr></label><div class="goal-conclusion"><span class="highlight">Ple pc (Pos.max a k)</span></div></blockquote></div></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk38" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk38"><span class="highlight">xomega.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-messages"><blockquote class="coq-message"><span class="highlight"><span class="bp">omega</span> <span class="kr">is</span> deprecated since <span class="mi">8</span>.<span class="mi">12</span>; use “<span class="bp">lia</span>” instead. +[<span class="bp">omega</span>-<span class="kr">is</span>-deprecated,deprecated]</span></blockquote></div><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">m</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">pc</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">m0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">k</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.elt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">v</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m0 ! k = None</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m ! k = Some v</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H1</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m0 ! pc = Some i -> Ple pc a</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">pc <> k</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H2</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m0 ! pc = Some i</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">Ple pc (Pos.max a k)</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk39" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk39"><span class="highlight"><span class="nb">apply</span> Ple_trans <span class="kr">with</span> a.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">m</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">pc</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">m0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">k</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.elt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">v</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m0 ! k = None</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m ! k = Some v</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H1</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m0 ! pc = Some i -> Ple pc a</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">pc <> k</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H2</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m0 ! pc = Some i</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">Ple pc a</span></div></blockquote><div class="coq-extra-goals"><input class="coq-extra-goal-toggle" id="htlgen-v-chk3a" style="display: none" type="checkbox"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">m</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">pc</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">m0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">k</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.elt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">v</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m0 ! k = None</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m ! k = Some v</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H1</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m0 ! pc = Some i -> Ple pc a</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">pc <> k</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H2</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m0 ! pc = Some i</span></span></span></span></div></div><label class="goal-separator coq-extra-goal-label" for="htlgen-v-chk3a"><hr></label><div class="goal-conclusion"><span class="highlight">Ple a (Pos.max a k)</span></div></blockquote></div></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk3b" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk3b"><span class="highlight"><span class="nb">auto</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">m</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">pc</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">m0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">k</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.elt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">v</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m0 ! k = None</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m ! k = Some v</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H1</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m0 ! pc = Some i -> Ple pc a</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">pc <> k</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H2</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m0 ! pc = Some i</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">Ple a (Pos.max a k)</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk3c" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk3c"><span class="highlight">xomega.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-messages"><blockquote class="coq-message"><span class="highlight"><span class="bp">omega</span> <span class="kr">is</span> deprecated since <span class="mi">8</span>.<span class="mi">12</span>; use “<span class="bp">lia</span>” instead. +[<span class="bp">omega</span>-<span class="kr">is</span>-deprecated,deprecated]</span></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Qed</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk3d" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk3d"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">max_pc_wf</span> : + <span class="kr">forall</span> <span class="nv">m</span>, Z.pos (max_pc_map m) <= Integers.Int.max_unsigned -> + map_well_formed m.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> <span class="nv">m</span> : PTree.t stmnt, +Z.pos (max_pc_map m) <= Integers.Int.max_unsigned -> +map_well_formed m</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk3e" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk3e"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> <span class="nv">m</span> : PTree.t stmnt, +Z.pos (max_pc_map m) <= Integers.Int.max_unsigned -> +map_well_formed m</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk3f" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk3f"><span class="highlight"><span class="nb">unfold</span> map_well_formed.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> <span class="nv">m</span> : PTree.t stmnt, +Z.pos (max_pc_map m) <= Integers.Int.max_unsigned -> +<span class="kr">forall</span> <span class="nv">p0</span> : positive, +In p0 (map fst (PTree.elements m)) -> +Z.pos p0 <= Integers.Int.max_unsigned</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk40" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk40"><span class="highlight"><span class="nb">intros</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">m</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Z.pos (max_pc_map m) <= Integers.Int.max_unsigned</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">p0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">In p0 (map fst (PTree.elements m))</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">Z.pos p0 <= Integers.Int.max_unsigned</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><span class="coq-input"><span class="highlight">exploit list_in_map_inv.</span></span><span class="coq-wsp"> </span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk41" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk41"><span class="highlight"><span class="bp">eassumption</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">m</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Z.pos (max_pc_map m) <= Integers.Int.max_unsigned</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">p0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">In p0 (map fst (PTree.elements m))</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">(<span class="kr">exists</span> <span class="nv">x</span> : positive * stmnt, + p0 = fst x /\ In x (PTree.elements m)) -> +Z.pos p0 <= Integers.Int.max_unsigned</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk42" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk42"><span class="highlight"><span class="nb">intros</span> [x [A B]].</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">m</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Z.pos (max_pc_map m) <= Integers.Int.max_unsigned</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">p0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">In p0 (map fst (PTree.elements m))</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">x</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">(positive * stmnt)%type</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">p0 = fst x</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">B</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">In x (PTree.elements m)</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">Z.pos p0 <= Integers.Int.max_unsigned</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk43" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk43"><span class="highlight"><span class="nb">destruct</span> x.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">m</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Z.pos (max_pc_map m) <= Integers.Int.max_unsigned</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">p0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">In p0 (map fst (PTree.elements m))</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">p</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">s</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">p0 = fst (p, s)</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">B</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">In (p, s) (PTree.elements m)</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">Z.pos p0 <= Integers.Int.max_unsigned</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk44" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk44"><span class="highlight"><span class="nb">apply</span> Maps.PTree.elements_complete <span class="kr">in</span> B.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">m</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Z.pos (max_pc_map m) <= Integers.Int.max_unsigned</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">p0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">In p0 (map fst (PTree.elements m))</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">p</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">s</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">p0 = fst (p, s)</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">B</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">m ! p = Some s</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">Z.pos p0 <= Integers.Int.max_unsigned</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk45" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk45"><span class="highlight"><span class="nb">apply</span> max_pc_map_sound <span class="kr">in</span> B.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">m</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Z.pos (max_pc_map m) <= Integers.Int.max_unsigned</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">p0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">In p0 (map fst (PTree.elements m))</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">p</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">s</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">p0 = fst (p, s)</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">B</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Ple p (max_pc_map m)</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">Z.pos p0 <= Integers.Int.max_unsigned</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk46" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk46"><span class="highlight"><span class="nb">unfold</span> Ple <span class="kr">in</span> B.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">m</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Z.pos (max_pc_map m) <= Integers.Int.max_unsigned</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">p0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">In p0 (map fst (PTree.elements m))</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">p</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">s</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">p0 = fst (p, s)</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">B</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">(p <= max_pc_map m)%positive</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">Z.pos p0 <= Integers.Int.max_unsigned</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk47" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk47"><span class="highlight"><span class="nb">apply</span> Pos2Z.pos_le_pos <span class="kr">in</span> B.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">m</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Z.pos (max_pc_map m) <= Integers.Int.max_unsigned</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">p0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">In p0 (map fst (PTree.elements m))</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">p</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">s</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">p0 = fst (p, s)</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">B</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Z.pos p <= Z.pos (max_pc_map m)</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">Z.pos p0 <= Integers.Int.max_unsigned</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk48" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk48"><span class="highlight"><span class="nb">subst</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">m</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Z.pos (max_pc_map m) <= Integers.Int.max_unsigned</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">p</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">s</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">In (fst (p, s)) (map fst (PTree.elements m))</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">B</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Z.pos p <= Z.pos (max_pc_map m)</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">Z.pos (fst (p, s)) <= Integers.Int.max_unsigned</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="htlgen-v-chk49" style="display: none" type="checkbox"><label class="coq-input" for="htlgen-v-chk49"><span class="highlight">simplify.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">m</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">PTree.t stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Z.pos (max_pc_map m) <= <span class="mi">4294967295</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">p</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">positive</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">s</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">stmnt</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">In p (map fst (PTree.elements m))</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">B</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Z.pos p <= Z.pos (max_pc_map m)</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">Z.pos p <= <span class="mi">4294967295</span></span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="nb">transitivity</span> (Z.pos (max_pc_map m)); <span class="nb">eauto</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Qed</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">transf_module</span> (<span class="nv">f</span>: function) : mon module := + <span class="kr">if</span> stack_correct f.(fn_stacksize) <span class="kr">then</span> + <span class="kp">do</span> fin <- create_reg (Some Voutput) <span class="mi">1</span>; + <span class="kp">do</span> rtrn <- create_reg (Some Voutput) <span class="mi">32</span>; + <span class="kp">do</span> (stack, stack_len) <- create_arr None <span class="mi">32</span> (Z.to_nat (f.(fn_stacksize) / <span class="mi">4</span>)); + <span class="kp">do</span> _ <- collectlist (transf_instr fin rtrn stack) (Maps.PTree.elements f.(RTL.fn_code)); + <span class="kp">do</span> _ <- collectlist (<span class="kr">fun</span> <span class="nv">r</span> => declare_reg (Some Vinput) r <span class="mi">32</span>) f.(RTL.fn_params); + <span class="kp">do</span> start <- create_reg (Some Vinput) <span class="mi">1</span>; + <span class="kp">do</span> rst <- create_reg (Some Vinput) <span class="mi">1</span>; + <span class="kp">do</span> clk <- create_reg (Some Vinput) <span class="mi">1</span>; + <span class="kp">do</span> current_state <- get; + <span class="kr">match</span> zle (Z.pos (max_pc_map current_state.(st_datapath))) Integers.Int.max_unsigned, + zle (Z.pos (max_pc_map current_state.(st_controllogic))) Integers.Int.max_unsigned <span class="kr">with</span> + | <span class="nb">left</span> LEDATA, <span class="nb">left</span> LECTRL => + ret (mkmodule + f.(RTL.fn_params) + current_state.(st_datapath) + current_state.(st_controllogic) + f.(fn_entrypoint) + current_state.(st_st) + stack + stack_len + fin + rtrn + start + rst + clk + current_state.(st_scldecls) + current_state.(st_arrdecls) + (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA))) + | _, _ => error (Errors.msg <span class="s2">"More than 2^32 states."</span>) + <span class="kr">end</span> + <span class="kr">else</span> error (Errors.msg <span class="s2">"Stack size misalignment."</span>).</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">max_state</span> (<span class="nv">f</span>: function) : state := + <span class="kr">let</span> <span class="nv">st</span> := Pos.succ (max_reg_function f) <span class="kr">in</span> + mkstate st + (Pos.succ st) + (Pos.succ (max_pc_function f)) + (AssocMap.<span class="nb">set</span> st (None, VScalar <span class="mi">32</span>) (st_scldecls (init_state st))) + (st_arrdecls (init_state st)) + (st_datapath (init_state st)) + (st_controllogic (init_state st)).</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">transl_module</span> (<span class="nv">f</span> : function) : Errors.res module := + run_mon (max_state f) (transf_module f).</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">transl_fundef</span> := transf_partial_fundef transl_module.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +<span class="c">(* Definition transl_program (p : RTL.program) := transform_partial_program transl_fundef p. *)</span> + +<span class="c">(*Definition transl_main_fundef f : Errors.res HTL.fundef :=</span> +<span class="c"> match f with</span> +<span class="c"> | Internal f => transl_fundef (Internal f)</span> +<span class="c"> | External f => Errors.Error (Errors.msg "Could not find internal main function")</span> +<span class="c"> end.</span> + +<span class="c">(** Translation of a whole program. *)</span> + +<span class="c">Definition transl_program (p: RTL.program) : Errors.res HTL.program :=</span> +<span class="c"> transform_partial_program2 (fun i f => if Pos.eqb p.(AST.prog_main) i</span> +<span class="c"> then transl_fundef f</span> +<span class="c"> else transl_main_fundef f)</span> +<span class="c"> (fun i v => Errors.OK v) p.</span> +<span class="c">*)</span> + +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">main_is_internal</span> (<span class="nv">p</span> : RTL.program) : bool := + <span class="kr">let</span> <span class="nv">ge</span> := Globalenvs.Genv.globalenv p <span class="kr">in</span> + <span class="kr">match</span> Globalenvs.Genv.find_symbol ge p.(AST.prog_main) <span class="kr">with</span> + | Some b => + <span class="kr">match</span> Globalenvs.Genv.find_funct_ptr ge b <span class="kr">with</span> + | Some (AST.Internal _) => true + | _ => false + <span class="kr">end</span> + | _ => false + <span class="kr">end</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">transl_program</span> (<span class="nv">p</span> : RTL.program) : Errors.res HTL.program := + <span class="kr">if</span> main_is_internal p + <span class="kr">then</span> transform_partial_program transl_fundef p + <span class="kr">else</span> Errors.Error (Errors.msg <span class="s2">"Main function is not Internal."</span>).</span></span></span></pre> +</div> +</div></body> +</html> |