(almost) prove the automaton that recognizes unsigned relations

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

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

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 }
 

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