From ec9b22d01cd89aecb95da02067919423a0f1f884 Mon Sep 17 00:00:00 2001
From: James Pollard <james@pollard.dev>
Date: Sat, 20 Jun 2020 17:47:52 +0100
Subject: Finish structure of Aindexed2scaled ILoad proof.

---
 src/verilog/Value.v | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'src/verilog')

diff --git a/src/verilog/Value.v b/src/verilog/Value.v
index b1ee353..818f625 100644
--- a/src/verilog/Value.v
+++ b/src/verilog/Value.v
@@ -294,6 +294,11 @@ Inductive val_value_lessdef: val -> value -> Prop :=
     forall i v',
     i = valueToInt v' ->
     val_value_lessdef (Vint i) v'
+| val_value_lessdef_ptr:
+    forall b off v',
+    off = Ptrofs.repr (valueToZ v') ->
+    (Z.modulo (valueToZ v') 4) = 0%Z ->
+    val_value_lessdef (Vptr b off) v'
 | lessdef_undef: forall v, val_value_lessdef Vundef v.
 
 Inductive opt_val_value_lessdef: option val -> value -> Prop :=
-- 
cgit