diff options
| author |  Jason Gross <jagro@google.com> | 2016-08-12 15:37:28 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-08-23 16:01:45 -0700 |
| commit | f9f012e80be8e1a49b8509c0f8c2410b32d53920 (patch) | |
| tree | e29bef89f3a296c3cff5133388971bf26be7b4e7 /src/BoundedArithmetic | |
| parent | 975421705a8e1196cd04c2fc396284bdbd857de7 (diff) | |
Fix some things
Diffstat (limited to 'src/BoundedArithmetic')
| -rw-r--r-- | src/BoundedArithmetic/Interface.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/BoundedArithmetic/Interface.v b/src/BoundedArithmetic/Interface.v index 4a14a160b..6ad38288a 100644 --- a/src/BoundedArithmetic/Interface.v +++ b/src/BoundedArithmetic/Interface.v @@ -36,7 +36,7 @@ Section InstructionGallery. Record load_immediate := { ldi :> imm -> W }. - Class is_load_immediate {ldi : load_immediate} := + Class is_load_immediate {ldi : load_immediate} := decode_load_immediate : forall x, 0 <= x < 2^n -> decode (ldi x) = x. Record shift_right_doubleword_immediate := { shrd :> W -> W -> imm -> W }. @@ -83,7 +83,7 @@ Section InstructionGallery. Record sub_with_carry := { subc :> W -> W -> bool -> bool * W }. - Class is_sub_with_carry (subc:W->W->bool->bool*W) := + Class is_sub_with_carry (subc : sub_with_carry) := { fst_sub_with_carry : forall x y c, fst (subc x y c) = ((decode x - decode y - bit c) <? 0); decode_snd_sub_with_carry : forall x y c, decode (snd (subc x y c)) = (decode x - decode y - bit c) mod 2^n |