1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
|
Require Import EqNat Peano_dec.
Require Import Bedrock.Word.
(* Very basic definitions *)
Definition wordSize := 32.
Definition Name := nat.
Definition WordCount := nat.
Definition WordList (words: WordCount) :=
{x: list (word wordSize) | length x = words}.
Inductive Pointer :=
| ListPtr: forall n, WordList n -> Pointer.
Definition TypeBindings := Name -> option WordCount.
Definition Bindings := Name -> option Pointer.
(* Primary inductive language definitions *)
Inductive CTerm (words: WordCount) :=
| CConst : WordList words -> CTerm words
| CVar : Name -> CTerm words
| CConcat: forall t1 t2, t1 + t2 = words -> CTerm t1 -> CTerm t2 -> CTerm words
| CHead: forall n: nat, gt n words -> CTerm n -> CTerm words
| CTail: forall n: nat, gt n words -> CTerm n -> CTerm words.
Inductive CExpr (words: WordCount) :=
| CLift : (CTerm words) -> (CExpr words)
| CNot : (CExpr words) -> (CExpr words)
| COpp : (CExpr words) -> (CExpr words)
| COr : (CExpr words) -> (CExpr words) -> (CExpr words)
| CAnd : (CExpr words) -> (CExpr words) -> (CExpr words)
| CXor : (CExpr words) -> (CExpr words) -> (CExpr words)
| CRShift : forall n: nat, (CExpr words) -> (CExpr words)
| CLShift : forall n: nat, (CExpr words) -> (CExpr words)
| CPlus : (CExpr words) -> (CExpr words) -> (CExpr words)
| CMinus : (CExpr words) -> (CExpr words) -> (CExpr words)
| CMult : forall n: nat, n*2 = words ->
(CExpr n) -> (CExpr n) -> (CExpr words)
| CDiv : (CExpr words) -> (CExpr words) -> (CExpr words)
| CMod : (CExpr words) -> (CExpr words) -> (CExpr words).
Definition bindType (name: Name) (type: WordCount) (bindings: TypeBindings)
: Name -> option WordCount :=
fun x => if (beq_nat x name) then Some type else bindings x.
Inductive Sub (inputs: TypeBindings) (output: WordCount) :=
| CRet : CExpr output -> Sub inputs output
| CCompose : forall resultName resultSize,
inputs resultName = None
-> (Sub inputs resultSize)
-> (Sub (bindType resultName resultSize inputs) output)
-> (Sub inputs output)
| CIte : (Sub inputs 1) (* condition *)
-> (Sub inputs output) (* then *)
-> (Sub inputs output) (* else *)
-> (Sub inputs output)
| CLet : forall (name: Name) (n: WordCount),
CExpr n
-> (Sub (bindType name n inputs) output)
-> (Sub inputs output)
| CRepeat : forall (bindOutputTo: Name) (n: nat),
inputs bindOutputTo <> None
-> (Sub (bindType bindOutputTo output inputs) output)
-> (Sub inputs output).
(* Some simple option-monad sugar *)
Definition optionReturn {A} (x : A) := Some x.
Definition optionBind {A B} (a : option A) (f : A -> option B) : option B :=
match a with
| Some x => f x
| None => None
end.
Notation "'do' A <- B ; C" := (optionBind B (fun A => C))
(at level 200, X ident, A at level 100, B at level 200).
Definition optionType {n m} (w: WordList n): option (WordList m).
destruct (eq_nat_dec n m);
abstract (try rewrite e in *; first [exact (Some w) | exact None]).
Defined.
Definition wordListConcat {t1 t2 words}:
t1 + t2 = words -> WordList t1 -> WordList t2 -> WordList words.
intros; exists ((proj1_sig H0) ++ (proj1_sig H1))%list.
abstract (destruct H0, H1; simpl;
rewrite List.app_length; intuition).
Defined.
Definition wordListHead {n words}:
gt n words -> WordList n -> WordList words.
intros; exists (List.firstn words (proj1_sig H0)).
abstract (destruct H0; simpl;
rewrite List.firstn_length; intuition).
Defined.
Lemma skipnLength: forall A m (x: list A),
ge (length x) m ->
length (List.skipn m x) = length x - m.
Proof.
intros; assert (length x = length (List.firstn m x ++ List.skipn m x)%list).
- rewrite List.firstn_skipn; trivial.
- rewrite H0; rewrite List.app_length; rewrite List.firstn_length.
replace (min m (length x)) with m; try rewrite min_l; intuition.
Qed.
Definition wordListTail {n words}:
gt n words -> WordList n -> WordList words.
intros; exists (List.skipn (n - words) (proj1_sig H0)).
abstract (destruct H0; simpl;
rewrite skipnLength; rewrite e; intuition).
Defined.
(* Now some basic evaluation routines *)
Fixpoint evalTerm {n} (bindings: Bindings) (term: CTerm n):
option (WordList n) :=
match term with
| CConst lst => Some lst
| CVar name =>
do p <- bindings name ;
match p with
| ListPtr m lst => optionType lst
end
| CConcat t1 t2 pf term1 term2 =>
do a <- evalTerm bindings term1;
do b <- evalTerm bindings term2;
Some (wordListConcat pf a b)%list
| CHead n pf t =>
do x <- evalTerm bindings t;
Some (wordListHead pf x)
| CTail n pf t =>
do x <- evalTerm bindings t;
Some (wordListTail pf x)
end.
Fixpoint evalExpr {n} (expr: CExpr n): option (word n) :=
match expr with
| CLift term => None
| CNot a => None
| COpp a => None
| COr a b =>
do x <- evalExpr a;
do y <- evalExpr b;
Some (x |^ y)%word
| CAnd a b => None
| CXor a b => None
| CRShift shift a => None
| CLShift shift a => None
| CPlus a b => None
| CMinus a b => None
| CMult _ _ a b => None
| CDiv a b => None
| CMod a b => None
end.
Fixpoint evalSub (inputs: Name -> option WordCount) (output: WordCount) (sub: Sub inputs output)
: word output :=
match sub with
| CRet e => natToWord output 0
| CCompose resName resSize _ a b => natToWord output 0
| CIte cond thenSub elseSub => natToWord output 0
| CLet name wordCount expr inside => natToWord output 0
| CRepeat inName times _ inside => natToWord output 0
end.
(* Equivalence Lemmas *)
|
