Skip to content

Commit fbd531f

Browse files
georgerenniegeorgerennie
committed
Add validity lemmas in VeIR style, like InBounds
1 parent 6241035 commit fbd531f

5 files changed

Lines changed: 143 additions & 13 deletions

File tree

‎Valaig/Aig/Basic.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,8 @@ import Valaig.Aig.DefsLemmas
55
import Valaig.Aig.RefsLemmas
66
import Valaig.ForStd
77

8+
open Valaig.Aig.Std
9+
810
namespace Valaig.Aig.Raw
911

1012
attribute [local simp, local grind] Raw.size

‎Valaig/Aig/Lemmas.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,8 @@ import Valaig.Aig.Basic
22

33
namespace Valaig
44

5+
open Valaig.Aig.Std
6+
57
attribute [local grind] Aig.Raw.aig
68
attribute [local grind! .] Std.Sat.AIG.hzero
79
attribute [local grind! .] Std.Sat.AIG.hconst

‎Valaig/Aig/Refs.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -87,7 +87,7 @@ def next (v : Var) : Var :=
8787
def ofRef {α} [DecidableEq α] [Hashable α] {aig : Std.Sat.AIG α} (ref : aig.Ref) : Var :=
8888
.ofIdx ref.gate
8989

90-
@[simp, grind =]
90+
@[simp, grind! .]
9191
theorem ofRef_idx {α} [DecidableEq α] [Hashable α] {aig : Std.Sat.AIG α} (ref : aig.Ref) :
9292
(ofRef ref).idx = ref.gate := by
9393
simp only [ofRef]

‎Valaig/Aig/StdSatLemmas.lean‎

Lines changed: 15 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,13 @@
1-
import Std.Sat.AIG.Basic
2-
import Std.Sat.AIG.Cached
3-
import Std.Sat.AIG.CachedGates
4-
import Std.Sat.AIG.CachedLemmas
5-
import Std.Sat.AIG.CachedGatesLemmas
1+
module
62

7-
namespace Valaig.Aig
3+
public import Std.Sat.AIG.Basic
4+
public import Std.Sat.AIG.Cached
5+
public import Std.Sat.AIG.CachedGates
6+
public import Std.Sat.AIG.CachedLemmas
7+
public import Std.Sat.AIG.CachedGatesLemmas
8+
9+
public section
10+
namespace Valaig.Aig.Std
811

912
open Std.Sat AIG
1013

@@ -25,14 +28,14 @@ theorem mkAtom_size (aig : AIG α) (var : α) :
2528
simp only [mkAtom_eq_decls_push, Array.size_push]
2629

2730
/--
28-
`AIG.mkAtom` returns a reference to the next element in the underlying AIG
31+
`AIG.mkAtom` returns a reference to the next element in the underlying AIG.
2932
-/
3033
theorem mkAtom_ref_eq_decls_size (aig : AIG α) (var : α) :
3134
(aig.mkAtom var).ref.gate = aig.decls.size := by
3235
simp only [mkAtom]
3336

3437
/--
35-
- `AIG.mkGate` only potentially appends gates, not atoms/constants
38+
`AIG.mkGate` only potentially appends gates, not atoms/constants.
3639
-/
3740
theorem mkGate_matches_gate (aig : AIG α) {input : aig.BinaryInput} {idx : Nat}
3841
{hlow : idx ≥ aig.decls.size} {hhigh : idx < (aig.mkGate input).aig.decls.size} :
@@ -44,7 +47,7 @@ theorem mkGate_matches_gate (aig : AIG α) {input : aig.BinaryInput} {idx : Nat}
4447
exact Nat.eq_of_le_of_lt_succ hlow hhigh
4548
simp [←hres, heq]
4649

47-
theorem mkGateCached.go_matches_gate (aig : AIG α) {input : aig.BinaryInput} {idx : Nat}
50+
private theorem mkGateCached.go_matches_gate (aig : AIG α) {input : aig.BinaryInput} {idx : Nat}
4851
{hlow : idx ≥ aig.decls.size} {hhigh : idx < (mkGateCached.go aig input).aig.decls.size} :
4952
∃ (lhs rhs : Fanin), (mkGateCached.go aig input).aig.decls[idx] = .gate lhs rhs := by
5053
generalize hres : (mkGateCached.go aig input).aig.decls = res at *
@@ -56,7 +59,7 @@ theorem mkGateCached.go_matches_gate (aig : AIG α) {input : aig.BinaryInput} {i
5659
· grind only [Array.getElem_push]
5760

5861
/--
59-
- `AIG.mkGateCached` only potentially appends gates, not atoms/constants
62+
`AIG.mkGateCached` only potentially appends gates, not atoms/constants.
6063
-/
6164
theorem mkGateCached_matches_gate (aig : AIG α) {input : aig.BinaryInput} {idx : Nat}
6265
{hlow : idx ≥ aig.decls.size} {hhigh : idx < (aig.mkGateCached input).aig.decls.size} :
@@ -65,11 +68,11 @@ theorem mkGateCached_matches_gate (aig : AIG α) {input : aig.BinaryInput} {idx
6568
split <;> apply mkGateCached.go_matches_gate <;> trivial
6669

6770
/--
68-
- `AIG.mkAndCached` only potentially appends gates, not atoms/constants
71+
`AIG.mkAndCached` only potentially appends gates, not atoms/constants.
6972
-/
7073
theorem mkAndCached_matches_gate (idx : Nat) (aig : AIG α) (input : aig.BinaryInput)
7174
{hlow : idx ≥ aig.decls.size} {hhigh : idx < (aig.mkAndCached input).aig.decls.size} :
7275
∃ (lhs rhs : Fanin), (aig.mkAndCached input).aig.decls[idx] = .gate lhs rhs := by
7376
simp_all only [mkAndCached, mkGateCached_matches_gate]
7477

75-
end Valaig.Aig
78+
end Valaig.Aig.Std

‎Valaig/Aig/Valid.lean‎

Lines changed: 123 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,123 @@
1+
module
2+
3+
public import Valaig.Aig.BasicNew
4+
public import Valaig.Aig.RefsLemmas
5+
import all Valaig.Aig.BasicNew
6+
public import Valaig.Aig.StdSatLemmas
7+
8+
public section pub
9+
namespace Valaig.Aig
10+
variable {aig : Aig}
11+
12+
-- Let grind/simp see inside all the definitions
13+
attribute [local simp, local grind]
14+
Var.validIn Lit.validIn InputIdx.validIn LatchIdx.validIn GenericIdx.validIn
15+
InputIdx.setVar InputIdx.getVar
16+
LatchIdx.setVar LatchIdx.setNext LatchIdx.setReset
17+
LatchIdx.getVar LatchIdx.getNext LatchIdx.getReset
18+
Aig.size Aig.addInput Aig.addLatch Aig.addAnd
19+
20+
attribute [local grind] InputIdx LatchIdx
21+
attribute [local grind =_] Var.ext_idx
22+
23+
section input
24+
25+
@[simp, grind =]
26+
theorem InputIdx.setVar_genericIdx_mono (idx : GenericIdx) :
27+
idx.validIn (setVar input aig var valid) ↔ idx.validIn aig := by
28+
simp
29+
30+
end input
31+
32+
section latch
33+
34+
@[simp, grind =]
35+
theorem LatchIdx.setVar_genericIdx_mono (idx : GenericIdx) :
36+
idx.validIn (setVar latch aig var valid) ↔ idx.validIn aig := by
37+
simp
38+
39+
@[simp, grind =]
40+
theorem LatchIdx.setNext_genericIdx_mono (idx : GenericIdx) :
41+
idx.validIn (setNext latch aig next valid) ↔ idx.validIn aig := by
42+
simp
43+
44+
@[simp, grind =]
45+
theorem LatchIdx.setReset_genericIdx_mono (idx : GenericIdx) :
46+
idx.validIn (setReset latch aig next valid) ↔ idx.validIn aig := by
47+
simp
48+
49+
end latch
50+
51+
section atom
52+
attribute [local simp, local grind =]
53+
Std.mkAtom_eq_decls_push Std.mkAtom_size Std.mkAtom_ref_eq_decls_size
54+
55+
/-
56+
addInput Lemmas.
57+
-/
58+
59+
@[grind .]
60+
theorem Aig.addInput_genericIdx_mono_impl (idx : GenericIdx) :
61+
idx.validIn aig → idx.validIn aig.addInput.fst := by
62+
simp; grind only
63+
64+
@[simp, grind =]
65+
theorem Aig.addInput_genericIdx_mono (idx : GenericIdx) :
66+
idx.validIn aig.addInput.fst ↔
67+
(idx.validIn aig
68+
∨ idx = .input aig.addInput.snd
69+
∨ idx = .node (aig.addInput.snd.getVar aig.addInput.fst)) := by
70+
simp; grind
71+
72+
@[grind .]
73+
theorem Aig.addInput_newInput_validIn :
74+
aig.addInput.snd.validIn aig.addInput.fst := by
75+
simp
76+
77+
/-
78+
addLatch Lemmas.
79+
-/
80+
81+
@[grind .]
82+
theorem Aig.addLatch_genericIdx_mono_impl (idx : GenericIdx) :
83+
idx.validIn aig → idx.validIn (aig.addLatch next reset).fst := by
84+
simp; grind only
85+
86+
@[simp, grind =]
87+
theorem Aig.addLatch_genericIdx_mono (idx : GenericIdx) :
88+
idx.validIn (aig.addLatch next reset).fst ↔
89+
(idx.validIn aig
90+
∨ idx = .latch (aig.addLatch next reset).snd
91+
∨ idx = .node ((aig.addLatch next reset).snd.getVar (aig.addLatch next reset).fst)) := by
92+
simp; grind
93+
94+
@[grind .]
95+
theorem Aig.addLatch_newLatch_validIn :
96+
(aig.addLatch next reset).snd.validIn (aig.addLatch next reset).fst := by
97+
simp
98+
99+
end atom
100+
101+
section gate
102+
attribute [local grind! .] Std.Sat.AIG.mkAndCached_le_size
103+
104+
/-
105+
addAnd Lemmas.
106+
-/
107+
108+
@[grind .]
109+
theorem Aig.addAnd_genericIdx_mono_impl (idx : GenericIdx) :
110+
idx.validIn aig → idx.validIn (aig.addAnd rhs0 rhs1 h0 h1).fst := by
111+
simp; grind
112+
113+
@[grind .]
114+
theorem Aig.addAnd_newAnd_validIn :
115+
(aig.addAnd rhs0 rhs1 h0 h1).snd.validIn (aig.addAnd rhs0 rhs1 h0 h1).fst := by
116+
simp
117+
-- TODO: Whycan't I get grind to see this another way
118+
have {aig : Std.Sat.AIG AtomIdx} {entry: aig.Ref} := entry.hgate
119+
grind only
120+
121+
end gate
122+
123+
end Valaig.Aig

0 commit comments

Comments
 (0)