diff options
| author | James Pollard <james@pollard.dev> | 2020-06-20 17:47:52 +0100 |
|---|---|---|
| committer | James Pollard <james@pollard.dev> | 2020-06-20 17:47:52 +0100 |
| commit | ec9b22d01cd89aecb95da02067919423a0f1f884 (patch) | |
| tree | 32da4beae3c813ffe366bf249aa682ed36df5b7e /src/verilog | |
| parent | d216c3b6dfbd80f49296b47ba46d18603c723804 (diff) | |
| download | vericert-kvx-ec9b22d01cd89aecb95da02067919423a0f1f884.tar.gz vericert-kvx-ec9b22d01cd89aecb95da02067919423a0f1f884.zip | |
Finish structure of Aindexed2scaled ILoad proof.
Diffstat (limited to 'src/verilog')
| -rw-r--r-- | src/verilog/Value.v | 5 |
1 files changed, 5 insertions, 0 deletions
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 := |