Skip to content

Commit 683b47f

Browse files
georgerenniegeorgerennie
committed
Define structural well-formedness and start proving preservation
1 parent add0dc5 commit 683b47f

2 files changed

Lines changed: 246 additions & 0 deletions

File tree

‎Valaig/Aig/IdxValidity.lean‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,15 @@ setup_get_set_definitions
1212
attribute [local simp, local grind]
1313
Var.validIn Lit.validIn InputIdx.validIn LatchIdx.validIn GenericIdx.validIn
1414

15+
-- General theorems about validity
16+
section
17+
18+
theorem validIn_mono {var var' : Var} (valid : var.validIn aig) (order : var' < var) :
19+
var'.validIn aig := by
20+
grind [Var.lt_idx]
21+
22+
end
23+
1524
section latch
1625
variable {latch : LatchIdx} {valid : latch.validIn aig}
1726

‎Valaig/Aig/WellFormed.lean‎

Lines changed: 237 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,237 @@
1+
module
2+
3+
public import Valaig.Aig.BasicNew
4+
import all Valaig.Aig.BasicNew
5+
public import Valaig.Aig.IdxValidity
6+
7+
public section pub
8+
namespace Valaig.Aig
9+
10+
setup_get_set_definitions
11+
12+
/--
13+
All input indices point to an input in the Aig.
14+
-/
15+
@[expose, simp]
16+
def InputsValid (aig : Aig) : Prop :=
17+
∀ {idx : InputIdx} (valid : idx.validIn aig),
18+
∃ (valid' : (idx.getVar aig valid).validIn aig),
19+
aig[idx.getVar aig valid] = .input idx
20+
21+
/--
22+
All inputs in the Aig point to a corresponding input index.
23+
-/
24+
def InputIdxsValid (aig : Aig) : Prop :=
25+
∀ {var : Var} (valid : var.validIn aig),
26+
match aig[var] with
27+
| .input idx =>
28+
∃ (valid' : idx.validIn aig), idx.getVar aig valid' = var
29+
| _ => True
30+
31+
/--
32+
All latch indices point to a latch in the Aig.
33+
-/
34+
@[expose, simp]
35+
def LatchesValid (aig : Aig) : Prop :=
36+
∀ {idx : LatchIdx} (valid : idx.validIn aig),
37+
∃ (valid' : (idx.getVar aig valid).validIn aig),
38+
aig[idx.getVar aig valid] = .latch idx
39+
40+
/--
41+
All latches in the Aig point to a corresponding latch index.
42+
-/
43+
def LatchIdxsValid (aig : Aig) : Prop :=
44+
∀ {var : Var} (valid : var.validIn aig),
45+
match aig[var] with
46+
| .latch idx =>
47+
∃ (valid' : idx.validIn aig), idx.getVar aig valid' = var
48+
| _ => True
49+
50+
/--
51+
All latch reset literals are valid in the Aig.
52+
This follows from `LatchesValid` and `AcyclicResets`.
53+
-/
54+
@[expose, simp]
55+
def ResetsValid (aig : Aig) : Prop :=
56+
∀ {idx : LatchIdx} (valid : idx.validIn aig),
57+
(idx.getReset aig valid).validIn aig
58+
59+
/--
60+
All latch next state literals are valid in the Aig.
61+
-/
62+
@[expose, simp]
63+
def NextsValid (aig : Aig) : Prop :=
64+
∀ {idx : LatchIdx} (valid : idx.validIn aig),
65+
(idx.getNext aig valid).validIn aig
66+
67+
/--
68+
The gates of the Aig are acyclic.
69+
This is enforced by requiring each gate's inputs to have lower variable
70+
indices than themselves.
71+
-/
72+
@[expose, simp]
73+
def AcyclicGates (aig : Aig) : Prop :=
74+
∀ {var : Var} {rhs0 rhs1} (valid : var.validIn aig),
75+
aig[var] = .and rhs0 rhs1 → rhs0.var < var ∧ rhs1.var < var
76+
77+
/--
78+
The reset function of the Aig is acyclic.
79+
This is enfoced by requiring each latch's reset to have a lower variable
80+
index than the latch's output.
81+
-/
82+
@[expose, simp]
83+
def AcyclicResets (aig : Aig) : Prop :=
84+
∀ {idx : LatchIdx} (valid : idx.validIn aig),
85+
(idx.getReset aig valid).var < idx.getVar aig valid
86+
87+
@[local grind]
88+
structure WellFormed (aig : Aig) : Prop where
89+
inputsValid : aig.InputsValid
90+
inputIdxsValid : aig.InputIdxsValid
91+
92+
-- ResetsValid isn't included as it follows from latchesValid and acyclicReset
93+
latchesValid : aig.LatchesValid
94+
latchIdxsValid : aig.LatchIdxsValid
95+
nextsValid : aig.NextsValid
96+
97+
acyclicGates : aig.AcyclicGates
98+
acyclicReset : aig.AcyclicResets
99+
100+
@[grind .]
101+
theorem WellFormed.resetsValid {aig : Aig} (wf : aig.WellFormed) :
102+
aig.ResetsValid := by
103+
intro _ valid
104+
rcases wf.latchesValid valid with ⟨varValid, _⟩
105+
have resetLt := wf.acyclicReset valid
106+
exact validIn_mono varValid resetLt
107+
108+
/-
109+
We consider the same patterns for invariant preservation as in the case of the get/set lemmas
110+
-/
111+
112+
variable {aig : Aig}
113+
114+
/-
115+
LatchIdx.setNext Lemmas.
116+
-/
117+
section setNext
118+
variable {setIdx : LatchIdx} {setValid : setIdx.validIn aig} {newNext : Lit}
119+
120+
@[grind .]
121+
theorem AcyclicGates_InputIdx_setNext (acyclicGates : aig.AcyclicGates) :
122+
(setIdx.setNext aig newNext setValid).AcyclicGates := by
123+
simp_all; assumption
124+
125+
@[grind .]
126+
theorem AcyclicResets_InputIdx_setNext (acyclicResets : aig.AcyclicResets) :
127+
(setIdx.setNext aig newNext setValid).AcyclicResets := by
128+
simp_all; grind
129+
130+
@[grind .]
131+
theorem WellFormed_InputIdx_setNext (wellFormed : aig.WellFormed) :
132+
(setIdx.setNext aig newNext setValid).WellFormed := by
133+
constructor <;> sorry -- grind
134+
135+
end setNext
136+
137+
/-
138+
LatchIdx.setReset Lemmas.
139+
-/
140+
section setReset
141+
variable {setIdx : LatchIdx} {setValid : setIdx.validIn aig} {newReset : Lit}
142+
143+
@[grind .]
144+
theorem AcyclicGates_InputIdx_setReset (acyclicGates : aig.AcyclicGates) :
145+
(setIdx.setReset aig newReset setValid).AcyclicGates := by
146+
simp_all; assumption
147+
148+
@[grind .]
149+
theorem AcyclicResets_InputIdx_setReset (acyclicResets : aig.AcyclicResets)
150+
(acyclic : newReset.var < setIdx.getVar aig setValid) :
151+
(setIdx.setReset aig newReset setValid).AcyclicResets := by
152+
simp_all; grind
153+
154+
@[grind .]
155+
theorem WellFormed_InputIdx_setReset (wellFormed : aig.WellFormed)
156+
(acyclic : newReset.var < setIdx.getVar aig setValid) :
157+
(setIdx.setReset aig newReset setValid).WellFormed := by
158+
constructor <;> sorry -- grind
159+
160+
end setReset
161+
162+
/-
163+
Aig.addInput Lemmas.
164+
-/
165+
section addInput
166+
167+
@[grind .]
168+
theorem AcyclicGates_Aig_addInput (acyclicGates : aig.AcyclicGates) :
169+
aig.addInput.fst.AcyclicGates := by
170+
simp_all; grind
171+
172+
@[grind .]
173+
theorem AcyclicResets_Aig_addInput (acyclicResets : aig.AcyclicResets) :
174+
aig.addInput.fst.AcyclicResets := by
175+
simp_all
176+
177+
@[grind .]
178+
theorem WellFormed_Aig_addInput (wellFormed : aig.WellFormed) :
179+
aig.addInput.fst.WellFormed := by
180+
constructor <;> sorry -- grind
181+
182+
end addInput
183+
184+
/-
185+
Aig.addLatch Lemmas.
186+
-/
187+
section addLatch
188+
variable {next reset : Lit}
189+
190+
@[grind .]
191+
theorem AcyclicGates_Aig_addLatch (acyclicGates : aig.AcyclicGates) :
192+
(aig.addLatch next reset).fst.AcyclicGates := by
193+
simp_all; grind
194+
195+
@[grind .]
196+
theorem AcyclicResets_Aig_addLatch (acyclicResets : aig.AcyclicResets)
197+
(resetValid : reset.validIn aig) :
198+
(aig.addLatch next reset).fst.AcyclicResets := by
199+
simp_all; grind [Var.lt_idx, Lit.validIn, Var.validIn]
200+
201+
@[grind .]
202+
theorem WellFormed_Aig_addLatch (wellFormed : aig.WellFormed)
203+
(resetValid : reset.validIn aig) :
204+
(aig.addLatch next reset).fst.WellFormed := by
205+
constructor <;> sorry -- grind
206+
207+
end addLatch
208+
209+
/-
210+
Aig.addAnd Lemmas.
211+
-/
212+
section addAnd
213+
variable {rhs0 rhs1 : Lit}
214+
215+
-- We don't currently need acyclicGates as the underlying AIG maintains this, but we will want it
216+
-- in the future
217+
set_option linter.unusedVariables false in
218+
@[grind .]
219+
theorem AcyclicGates_Aig_addAnd (acyclicGates : aig.AcyclicGates)
220+
(h0 : rhs0.validIn aig) (h1 : rhs1.validIn aig) :
221+
(aig.addAnd rhs0 rhs1 h0 h1).fst.AcyclicGates := by
222+
simp_all [Var.validIn, Var.lt_idx]
223+
intro var
224+
have := @Std.Sat.AIG.hdag (i := var.idx)
225+
grind
226+
227+
@[grind .]
228+
theorem AcyclicResets_Aig_addAnd (acyclicResets : aig.AcyclicResets) :
229+
(aig.addAnd rhs0 rhs1 h0 h1).fst.AcyclicResets := by
230+
simp_all
231+
232+
@[grind .]
233+
theorem WellFormed_Aig_addAnd (wellFormed : aig.WellFormed) :
234+
(aig.addAnd rhs0 rhs1 h0 h1).fst.WellFormed := by
235+
constructor <;> sorry -- grind
236+
237+
end addAnd

0 commit comments

Comments
 (0)