diff options
author | James Pollard <james@pollard.dev> | 2020-06-09 16:03:22 +0100 |
---|---|---|
committer | James Pollard <james@pollard.dev> | 2020-06-09 16:03:22 +0100 |
commit | 7971f2f570de84204aeca2cb72001dc3e824501d (patch) | |
tree | da10753bc6563944309bd23b4dff41185a3e9e43 /src/verilog/Verilog.v | |
parent | 6426456c4cc7c6d11cf0204ff3d3c0aa18762323 (diff) | |
parent | 86e1d027bb556e0e1f5a39c93b41130603f4f9ad (diff) | |
download | vericert-7971f2f570de84204aeca2cb72001dc3e824501d.tar.gz vericert-7971f2f570de84204aeca2cb72001dc3e824501d.zip |
Merge branch 'develop' into arrays-proof
Diffstat (limited to 'src/verilog/Verilog.v')
-rw-r--r-- | src/verilog/Verilog.v | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 74c08fe..845d706 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -32,7 +32,8 @@ From compcert Require Integers Events. From compcert Require Import Errors Smallstep Globalenvs. Import HexNotationValue. -Import AssocMapNotation. + +Local Open Scope assocmap. Set Implicit Arguments. @@ -291,17 +292,13 @@ Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop expr_runp fext reg stack (Vlit v) v | erun_Vvar : forall fext reg stack v r, - reg!r = Some v -> + reg#r = v -> expr_runp fext reg stack (Vvar r) v | erun_Vvari : forall fext reg stack v iexp i r, expr_runp fext reg stack iexp i -> arr_assocmap_lookup stack r (valueToNat i) = Some v -> expr_runp fext reg stack (Vvari r iexp) v - | erun_Vvar_empty : - forall fext reg stack r sz, - reg!r = None -> - expr_runp fext reg stack (Vvar r) (ZToValue sz 0) | erun_Vinputvar : forall fext reg stack r v, fext!r = Some v -> |