diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-05-26 13:02:15 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-05-26 13:02:15 +0100 |
commit | b3c58bddaa0aa06f2c0905eeb3eb5318cb6361aa (patch) | |
tree | 95761cc497381249e54378f1071afa6694235607 /src/translation/HTLgen.v | |
parent | bdd3b6734690100a7c696cf57bfe52963ec2c6ef (diff) | |
download | vericert-b3c58bddaa0aa06f2c0905eeb3eb5318cb6361aa.tar.gz vericert-b3c58bddaa0aa06f2c0905eeb3eb5318cb6361aa.zip |
Finished proof of spec completely
Diffstat (limited to 'src/translation/HTLgen.v')
-rw-r--r-- | src/translation/HTLgen.v | 35 |
1 files changed, 33 insertions, 2 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 670dcd4..26dc630 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -142,6 +142,37 @@ Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit := | _, _ => Error (Errors.msg "HTL.add_instr") end. +Lemma add_instr_skip_state_incr : + forall s n st, + (st_datapath s)!n = None -> + (st_controllogic s)!n = None -> + st_incr s + (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + (AssocMap.add n st s.(st_datapath)) + (AssocMap.add n Vskip s.(st_controllogic))). +Proof. + constructor; intros; + try (simpl; destruct (peq n n0); subst); + auto with htlh. +Qed. + +Definition add_instr_skip (n : node) (st : stmnt) : mon unit := + fun s => + match check_empty_node_datapath s n, check_empty_node_controllogic s n with + | left STM, left TRANS => + OK tt (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + (AssocMap.add n st s.(st_datapath)) + (AssocMap.add n Vskip s.(st_controllogic))) + (add_instr_skip_state_incr s n st STM TRANS) + | _, _ => Error (Errors.msg "HTL.add_instr") + end. + Definition nonblock (dst : reg) (e : expr) := Vnonblock (Vvar dst) e. Definition block (dst : reg) (e : expr) := Vblock (Vvar dst) e. @@ -285,9 +316,9 @@ Definition transf_instr (fin rtrn: reg) (ni: node * instruction) : mon unit := | Ireturn r => match r with | Some r' => - add_instr n n (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r'))) + add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r'))) | None => - add_instr n n (block fin (Vlit (ZToValue 1%nat 1%Z))) + add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vlit (ZToValue 1%nat 0%Z)))) end end end. |