diff options
| author | James Pollard <james@pollard.dev> | 2020-06-11 22:50:01 +0100 |
|---|---|---|
| committer | James Pollard <james@pollard.dev> | 2020-06-11 22:50:01 +0100 |
| commit | 088a554043e3d4b8b8b424dbda9a136e3f4571e5 (patch) | |
| tree | 49d817abbcc703b0e34c4d63e03a4bd404aef87f /src/verilog/Verilog.v | |
| parent | d0257b0a47ad998e01715e9bc6ba612b834765f1 (diff) | |
| download | vericert-kvx-088a554043e3d4b8b8b424dbda9a136e3f4571e5.tar.gz vericert-kvx-088a554043e3d4b8b8b424dbda9a136e3f4571e5.zip | |
Rough outline of stack address proof
Diffstat (limited to 'src/verilog/Verilog.v')
| -rw-r--r-- | src/verilog/Verilog.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 845d706..0e999de 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -56,10 +56,10 @@ Definition merge_associations {A : Type} (assoc : associations A) := mkassociations (AssocMapExt.merge A assoc.(assoc_nonblocking) assoc.(assoc_blocking)) (AssocMap.empty A). -Definition arr_assocmap_lookup (a : assocmap_arr) (r : reg) (i : nat) : option value := +Definition arr_assocmap_lookup (a : assocmap_arr) (r : reg) (i : nat) : value := match a ! r with - | None => None - | Some arr => nth_error arr i + | None => natToValue 32 0 + | Some arr => nth i arr (natToValue 32 0) end. Fixpoint list_set {A : Type} (i : nat) (x : A) (l : list A) : list A := @@ -297,7 +297,7 @@ Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop | 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 -> + arr_assocmap_lookup stack r (valueToNat i) = v -> expr_runp fext reg stack (Vvari r iexp) v | erun_Vinputvar : forall fext reg stack r v, |