Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / optim / oversampling / out / typed / Compound.v @ 6a93d814

History | View | Annotate | Download (1.25 KB)

1
(* ---------------------------------------------------------- *)
2
(* --- Memory Compound Updates                            --- *)
3
(* ---------------------------------------------------------- *)
4

    
5
Require Import ZArith.
6
Require Import Reals.
7
Require Import BuiltIn.
8
Require Import bool.Bool.
9
Require Import int.Int.
10
Require Import int.Abs.
11
Require Import int.ComputerDivision.
12
Require Import real.Real.
13
Require Import real.RealInfix.
14
Require Import real.FromInt.
15
Require Import map.Map.
16
Require Import Qedlib.
17
Require Import Qed.
18
Require Import Memory.
19

    
20
Definition shift_sint32 (p : addr) (k : Z) : addr := (shift p k%Z).
21

    
22
Definition shiftfield_F_g_mem_ni_1 (p : addr) : addr := (shift p 1%Z).
23

    
24
Definition shiftfield_F_g_mem_ni_0 (p : addr) : addr := (shift p 2%Z).
25

    
26
Definition shiftfield_F_g_reg___g_2 (p : addr) : addr := (shift p 0%Z).
27

    
28
Definition shiftfield_F_g_mem__reg (p : addr) : addr := (shift p 0%Z).
29

    
30
Definition shiftfield_F__arrow_reg__first (p : addr) : addr := (shift p 0%Z).
31

    
32
Definition shiftfield_F__arrow_mem__reg (p : addr) : addr := (shift p 0%Z).
33

    
34
Definition shiftfield_F_f_mem_ni_2 (p : addr) : addr := (shift p 1%Z).
35

    
36
Definition shiftfield_F_f_reg___f_2 (p : addr) : addr := (shift p 0%Z).
37

    
38
Definition shiftfield_F_f_mem__reg (p : addr) : addr := (shift p 0%Z).
39