diff --git a/SSA/Experimental/Bits/AutoStructs/Defs.lean b/SSA/Experimental/Bits/AutoStructs/Defs.lean index 4c7199f87..a54ca26b4 100644 --- a/SSA/Experimental/Bits/AutoStructs/Defs.lean +++ b/SSA/Experimental/Bits/AutoStructs/Defs.lean @@ -228,8 +228,7 @@ inductive Relation | unsigned (ord : RelationOrdering) deriving Repr - -def evalRelation {w} (rel : Relation) (bv1 bv2 : BitVec w) : Bool := +def evalRelation (rel : Relation) {w} (bv1 bv2 : BitVec w) : Bool := match rel with | .eq => bv1 = bv2 | .signed .lt => bv1 <ₛ bv2 diff --git a/SSA/Experimental/Bits/AutoStructs/ForLean.lean b/SSA/Experimental/Bits/AutoStructs/ForLean.lean index b37f48bd8..a630b0fb3 100644 --- a/SSA/Experimental/Bits/AutoStructs/ForLean.lean +++ b/SSA/Experimental/Bits/AutoStructs/ForLean.lean @@ -72,7 +72,6 @@ theorem Std.HashMap.mem_iff_getElem? [BEq K] [LawfulBEq K] [Hashable K] [LawfulH k ∈ m ↔ ∃ v, m[k]? = some v := by sorry - @[aesop 50% unsafe] theorem Std.HashMap.get?_none_not_mem [BEq K] [LawfulBEq K] [Hashable K] [LawfulHashable K] {m : Std.HashMap K V} {k : K} : m.get? k = none → k ∉ m := by sorry diff --git a/SSA/Experimental/Bits/AutoStructs/ForMathlib.lean b/SSA/Experimental/Bits/AutoStructs/ForMathlib.lean index 6c85eb1e4..285fa8ccf 100644 --- a/SSA/Experimental/Bits/AutoStructs/ForMathlib.lean +++ b/SSA/Experimental/Bits/AutoStructs/ForMathlib.lean @@ -50,6 +50,10 @@ structure BitVecs (n : Nat) where w : Nat bvs : Vector (BitVec w) n +abbrev BitVecs.empty : BitVecs n := ⟨0, Mathlib.Vector.replicate n .nil⟩ +abbrev BitVecs.singleton {w : Nat} (bv : BitVec w) : BitVecs 1 := ⟨w, bv ::ᵥ .nil⟩ +abbrev BitVecs.pair {w : Nat} (bv1 bv2 : BitVec w) : BitVecs 2 := ⟨w, bv1 ::ᵥ bv2 ::ᵥ .nil⟩ + def BitVecs0 : Set (BitVecs n) := {⟨0, Vector.replicate n (BitVec.zero 0)⟩} @@ -83,7 +87,11 @@ def dec (bvs' : BitVecs' n) : BitVecs n where w := bvs'.length bvs := Vector.ofFn fun k => BitVec.ofFn fun i => bvs'[i].getLsbD k --- The two sets are in bijection for `n > 0`. +@[simp] +lemma dec_nil n : dec (n := n) [] = BitVecs.empty := by + ext <;> simp [dec] + +-- The two sets are in bijection. @[simp] lemma enc_length (bvs : BitVecs n) : (enc bvs).length = bvs.w := by @@ -157,6 +165,12 @@ def dec_surj (n : Nat) : Function.Surjective (dec (n := n)) := by def dec_inj {n : Nat} : Function.Injective (dec (n := n)) := by exact Function.Bijective.injective dec_bij +@[simp] +lemma dec_enc_image : dec '' (enc '' S) = S := Function.LeftInverse.image_image dec_enc _ + +@[simp] +lemma env_dec_image : enc '' (dec '' S) = S := Function.LeftInverse.image_image enc_dec _ + def BitVecs.transport (f : Fin n → Fin m) (bvs : BitVecs m) : BitVecs n := { w := bvs.w, bvs := bvs.bvs.transport f } diff --git a/SSA/Experimental/Bits/AutoStructs/FormulaToAuto.lean b/SSA/Experimental/Bits/AutoStructs/FormulaToAuto.lean index 830e9b58e..24e73ad74 100644 --- a/SSA/Experimental/Bits/AutoStructs/FormulaToAuto.lean +++ b/SSA/Experimental/Bits/AutoStructs/FormulaToAuto.lean @@ -92,58 +92,230 @@ def CNFA.autEq : CNFA (BitVec 2) := def GoodCNFA.autEq : GoodCNFA 2 := ⟨CNFA.autEq, by sorry⟩ -def CNFA.autSignedCmp (cmp: RelationOrdering) : CNFA (BitVec 2) := +def NFA.sa (_ : NFA α σ) := σ → Language α + +structure NFA.correct (M : NFA α σ) (ζ : M.sa) (L : Language α) where + cond1 : ∀ w, (w ∈ L ↔ ∃ q ∈ M.accept, w ∈ ζ q) + cond2 : ∀ w q, q ∈ M.eval w ↔ w ∈ ζ q + +lemma NFA.correct_spec {M : NFA α σ} {ζ : M.sa} {L : Language α} : + M.correct ζ L → M.accepts = L := by + rintro ⟨h1, h2⟩ + simp [accepts]; ext w + simp_all + rfl + +abbrev BVRel := ∀ ⦃w⦄, BitVec w → BitVec w → Prop + +def langRel (R : BVRel) : Set (BitVecs 2) := + { bvs | R (bvs.bvs.get 0) (bvs.bvs.get 1) } + +def NFA.autEq : NFA (BitVec 2) Unit := + { start := ⊤, accept := ⊤, step := fun () a => if a = 0 ∨ a = 3 then ⊤ else ⊥ } + +def GoodNFA.autEq : GoodNFA 2 := + ⟨Unit, { start := ⊤, accept := ⊤, step := fun () a => if a = 0 ∨ a = 3 then ⊤ else ⊥ }⟩ + +def GoodNFA.eqRel : BVRel := fun _ x y => x = y + +@[simp] +lemma in_enc : x ∈ enc '' S ↔ dec x ∈ S := by + simp; constructor + · simp; rintro y hS rfl; simp_all + · rintro hS; use dec x; simp_all + +@[simp] +lemma Mathlib.Vector.ofFn_0 {f : Fin 0 → α} : ofFn f = .nil := by + simp [ofFn] + +@[simp] +lemma BitVec.ofFn_0 {f : Fin 0 → Bool} : ofFn f = .nil := by + apply eq_nil + +@[simp] +lemma dec_snoc_in_langRel : + dec (w ++ [a]) ∈ langRel R ↔ R (.cons a[0] ((dec w).bvs.get 0)) (.cons a[1] ((dec w).bvs.get 1)) := by + sorry + +def GoodNFA.sa (M : GoodNFA n) := M.σ → (∀ ⦃w⦄, BitVec w → BitVec w → Prop) + +structure GoodNFA.correct2 (M : GoodNFA 2) (ζ : M.sa) (L : BVRel) where + cond1 : ∀ (bv1 bv2 : BitVec w), (L bv1 bv2 ↔ ∃ q ∈ M.M.accept, ζ q bv1 bv2) + cond2 q : q ∈ M.M.start ↔ ζ q .nil .nil + cond3 q a w (bv1 bv2 : BitVec w) : q ∈ M.M.stepSet { q | ζ q bv1 bv2 } a ↔ + ζ q (BitVec.cons a[0] bv1) (BitVec.cons a[1] bv2) + +lemma GoodNFA.correct2_spec (M : GoodNFA 2) (ζ : M.sa) (L : BVRel) : + M.correct2 ζ L → M.accepts = langRel L := by + rintro ⟨h1, h2, h3⟩ + simp [accepts, accepts'] + have heq : dec '' (enc '' langRel L) = langRel L := by simp + rw [←heq] + congr! + suffices h : M.M.correct (fun q => enc '' langRel (ζ q)) (enc '' langRel L) by + apply NFA.correct_spec h + constructor + · intros w; rw [in_enc]; simp [langRel, h1]; simp_rw [@in_enc _ _ w]; rfl + intros w; induction w using List.list_reverse_induction + case base => + intros q; simp [autEq]; rw [in_enc]; simp [h2, langRel]; rfl + case ind w a ih => + rintro q + simp + rw [in_enc] + have h : M.M.eval w = { q | w ∈ enc '' langRel (ζ q) } := by + ext; rw [ih]; dsimp; rfl + rw [dec_snoc_in_langRel] + rw [h]; simp_rw [in_enc] + simp [langRel, h3] + +@[simp] +lemma BitVec.duh : cons b1 bv1 = cons b2 bv2 ↔ (b1 = b2) ∧ bv1 = bv2 := by + sorry + +@[simp] lemma BitVec.lk30 : (3#2 : BitVec 2)[0] = true := by rfl +@[simp] lemma BitVec.lk31 : (3#2 : BitVec 2)[1] = true := by rfl +@[simp] lemma BitVec.lk20 : (2#2 : BitVec 2)[0] = false := by rfl +@[simp] lemma BitVec.lk21 : (2#2 : BitVec 2)[1] = true := by rfl +@[simp] lemma BitVec.lk10 : (1#2 : BitVec 2)[0] = true := by rfl +@[simp] lemma BitVec.lk11 : (1#2 : BitVec 2)[1] = false := by rfl +@[simp] lemma BitVec.lk00 : (0#2 : BitVec 2)[0] = false := by rfl +@[simp] lemma BitVec.lk01 : (0#2 : BitVec 2)[1] = false := by rfl + +lemma GoodNFA.autEq_correct : autEq.correct2 (fun _ => eqRel) eqRel := by + constructor <;> simp [autEq, eqRel] + rintro ⟨⟩ ⟨a⟩ w bv1 bv2 + fin_cases a <;> simp [NFA.stepSet] + +def CNFA.autUnsignedCmp (cmp: RelationOrdering) : CNFA (BitVec 2) := let m := CNFA.empty let (seq, m) := m.newState let (sgt, m) := m.newState let (slt, m) := m.newState - let (sgtfin, m) := m.newState - let (sltfin, m) := m.newState let m := m.addInitial seq let m := m.addManyTrans [0#2, 3#2] seq seq let m := m.addTrans 1#2 seq sgt let m := m.addTrans 2#2 seq slt - let m := m.addTrans 1#2 seq sltfin - let m := m.addTrans 2#2 seq sgtfin let m := m.addManyTrans [0#2, 1#2, 3#2] sgt sgt - let m := m.addManyTrans [0#2, 2#2, 3#2] sgt sgtfin - let m := m.addTrans 1#2 sgt sltfin let m := m.addTrans 2#2 sgt slt let m := m.addManyTrans [0#2, 2#2, 3#2] slt slt - let m := m.addManyTrans [0#2, 1#2, 3#2] slt sltfin - let m := m.addTrans 2#2 slt sgtfin let m := m.addTrans 1#2 slt sgt match cmp with - | .lt => m.addFinal sltfin - | .le => (m.addFinal sltfin).addFinal seq - | .gt => m.addFinal sgtfin - | .ge => (m.addFinal sgtfin).addFinal seq + | .lt => m.addFinal slt + | .le => (m.addFinal slt).addFinal seq + | .gt => m.addFinal sgt + | .ge => (m.addFinal sgt).addFinal seq -def GoodCNFA.autSignedCmp (cmp: RelationOrdering) : GoodCNFA 2 := - ⟨CNFA.autSignedCmp cmp, by sorry⟩ +def GoodCNFA.autUnsignedCmp (cmp: RelationOrdering) : GoodCNFA 2 := + ⟨CNFA.autUnsignedCmp cmp, by sorry⟩ +inductive NFA.unsignedCmpState : Type where +| eq | gt | lt -def CNFA.autUnsignedCmp (cmp: RelationOrdering) : CNFA (BitVec 2) := +def NFA.unsignedCmpStep (q : NFA.unsignedCmpState) (a : BitVec 2) : Set NFA.unsignedCmpState := + match q, a with + | .eq, 0 => { .eq } | .eq, 3 => { .eq } | .eq, 1 => { .gt } | .eq, 2 => { .lt } + | .gt, 0 => { .gt } | .gt, 1 => { .gt } | .gt, 3 => { .gt } | .gt, 2 => { .lt } + | .lt, 0 => { .lt } | .lt, 1 => { .gt } | .lt, 2 => { .lt } | .lt, 3 => { .lt } + +def NFA.autUnsignedCmp (cmp: RelationOrdering) : NFA (BitVec 2) unsignedCmpState where + step := unsignedCmpStep + start := {.eq} + accept := match cmp with | .lt => {.lt} | .le => {.lt, .eq} | .gt => {.gt} | .ge => {.gt, .eq} + +def GoodNFA.autUnsignedCmp (cmp: RelationOrdering) : GoodNFA 2 := + ⟨_, NFA.autUnsignedCmp cmp⟩ + +def AutoStructs.RelationOrdering.urel (cmp : RelationOrdering) : BVRel := + match cmp with + | .lt => fun _ bv1 bv2 => bv1 <ᵤ bv2 + | .le => fun _ bv1 bv2 => bv1 ≤ᵤ bv2 + | .gt => fun _ bv1 bv2 => bv1 >ᵤ bv2 + | .ge => fun _ bv1 bv2 => bv1 ≥ᵤ bv2 + +def GoodNFA.autUnsignedCmpSA (q : NFA.unsignedCmpState) : BVRel := + match q with + | .eq => fun _ bv1 bv2 => bv1 = bv2 + | .lt => fun _ bv1 bv2 => bv1 <ᵤ bv2 + | .gt => fun _ bv1 bv2 => bv1 >ᵤ bv2 + +lemma BitVec.ule_iff_ult_or_eq {w : ℕ} (bv1 bv2 : BitVec w): + (bv2 ≥ᵤ bv1) = true ↔ (bv2 >ᵤ bv1) = true ∨ bv1 = bv2 := by + simp [BitVec.ule, BitVec.ult, le_iff_lt_or_eq, BitVec.toNat_eq] + +@[simp] +lemma BitVec.cons_ugt_ff {w} {bv1 bv2 : BitVec w} : + (BitVec.cons false bv1 >ᵤ BitVec.cons false bv2) ↔ bv1 >ᵤ bv2 := by + simp [BitVec.ult] +@[simp] +lemma BitVec.cons_ugt_tt {w} {bv1 bv2 : BitVec w} : + (BitVec.cons true bv1 >ᵤ BitVec.cons true bv2) ↔ bv1 >ᵤ bv2 := by + simp [BitVec.ult] + sorry +@[simp] +lemma BitVec.cons_ugt_tf {w} {bv1 bv2 : BitVec w} : + (BitVec.cons true bv1 >ᵤ BitVec.cons false bv2) ↔ True := by + sorry +@[simp] +lemma BitVec.cons_ugt_ft {w} {bv1 bv2 : BitVec w} : + (BitVec.cons false bv1 >ᵤ BitVec.cons true bv2) ↔ false := by + sorry +@[simp] +lemma ucmp_tricho : (bv1 >ᵤ bv2) = false → (bv2 >ᵤ bv1) = false → bv1 = bv2 := by + sorry + +lemma GoodNFA.autUnsignedCmp_correct cmp : autUnsignedCmp cmp |>.correct2 autUnsignedCmpSA cmp.urel := by + let getState {w} (bv1 bv2 : BitVec w) : NFA.unsignedCmpState := + if bv1 >ᵤ bv2 then .gt else if bv2 >ᵤ bv1 then .lt else .eq + constructor <;> simp [NFA.autUnsignedCmp, autUnsignedCmp, autUnsignedCmpSA, AutoStructs.RelationOrdering.urel] + · cases cmp <;> simp [BitVec.ule_iff_ult_or_eq]; tauto + · rintro (_ | _ | _) <;> simp + · rintro (_ | _ | _) a w bv1 bv2 <;> simp [NFA.stepSet, NFA.unsignedCmpStep] + · constructor + · rintro ⟨i, hi⟩; cases i <;> fin_cases a <;> simp_all [NFA.unsignedCmpStep, instFinEnumBitVec_sSA] + · rintro ⟨_, _⟩; use .eq; simp; fin_cases a <;> simp_all [instFinEnumBitVec_sSA] + · constructor + · rintro ⟨i, hi⟩; cases i <;> fin_cases a <;> simp_all [NFA.unsignedCmpStep, instFinEnumBitVec_sSA] + · rintro _; fin_cases a <;> simp_all [instFinEnumBitVec_sSA] + · use .gt; simp_all + · use (getState bv1 bv2); simp [getState]; split_ifs <;> simp_all; apply ucmp_tricho <;> assumption + · use .gt; simp_all + · constructor + · rintro ⟨i, hi⟩; cases i <;> fin_cases a <;> simp_all [NFA.unsignedCmpStep, instFinEnumBitVec_sSA] + · rintro _; fin_cases a <;> simp_all [instFinEnumBitVec_sSA] + · use .lt; simp_all + · use (getState bv1 bv2); simp [getState]; split_ifs <;> simp_all; apply ucmp_tricho <;> assumption + · use .lt; simp_all + +def CNFA.autSignedCmp (cmp: RelationOrdering) : CNFA (BitVec 2) := let m := CNFA.empty let (seq, m) := m.newState let (sgt, m) := m.newState let (slt, m) := m.newState + let (sgtfin, m) := m.newState + let (sltfin, m) := m.newState let m := m.addInitial seq let m := m.addManyTrans [0#2, 3#2] seq seq let m := m.addTrans 1#2 seq sgt let m := m.addTrans 2#2 seq slt + let m := m.addTrans 1#2 seq sltfin + let m := m.addTrans 2#2 seq sgtfin let m := m.addManyTrans [0#2, 1#2, 3#2] sgt sgt + let m := m.addManyTrans [0#2, 2#2, 3#2] sgt sgtfin + let m := m.addTrans 1#2 sgt sltfin let m := m.addTrans 2#2 sgt slt let m := m.addManyTrans [0#2, 2#2, 3#2] slt slt + let m := m.addManyTrans [0#2, 1#2, 3#2] slt sltfin + let m := m.addTrans 2#2 slt sgtfin let m := m.addTrans 1#2 slt sgt match cmp with - | .lt => m.addFinal slt - | .le => (m.addFinal slt).addFinal seq - | .gt => m.addFinal sgt - | .ge => (m.addFinal sgt).addFinal seq + | .lt => m.addFinal sltfin + | .le => (m.addFinal sltfin).addFinal seq + | .gt => m.addFinal sgtfin + | .ge => (m.addFinal sgtfin).addFinal seq -def GoodCNFA.autUnsignedCmp (cmp: RelationOrdering) : GoodCNFA 2 := - ⟨CNFA.autUnsignedCmp cmp, by sorry⟩ +def GoodCNFA.autSignedCmp (cmp: RelationOrdering) : GoodCNFA 2 := + ⟨CNFA.autSignedCmp cmp, by sorry⟩ def CNFA.autMsbSet' : CNFA (BitVec 1) := let m := CNFA.empty @@ -310,6 +482,7 @@ lemma absNfaToFomrmula_spec (φ : Formula) : case binop op φ1 φ2 ih1 ih2 => rcases op <;> simp [absNfaOfFormula, binopAbsNfa, langBinop, ih1, ih2] + /- Note: it is important to define this function and not inline it, otherwise each call to the tactic will compile a new function, which takes ~350ms on