Define basic well-formedness of LFunc/Factory and prove WF of Boogie Factory

.github/workflows/ci.yml

@@ -77,7 +77,7 @@ jobs:
       - name: Test BoogieToStrata
         run: dotnet test ${SOLUTION}
       - name: Test Strata Command line
-        run: .github/scripts/testStrataCommand.sh        
+        run: .github/scripts/testStrataCommand.sh
       - name: Validate examples against expected output
         working-directory: Examples
         shell: bash

Strata/DL/Lambda/Factory.lean

@@ -6,6 +6,8 @@
 
 import Strata.DL.Lambda.LExprWF
 import Strata.DL.Lambda.LTy
+import Strata.DDM.Util.Array
+import Strata.DL.Util.List
 import Strata.DL.Util.ListMap
 
 /-!
@@ -26,7 +28,7 @@ namespace Lambda
 
 open Std (ToFormat Format format)
 
-variable {T : LExprParams} [Inhabited T.Metadata] [Inhabited T.IDMeta] [DecidableEq T.IDMeta] [BEq T.IDMeta] [ToFormat T.IDMeta]
+variable {T : LExprParams} [Inhabited T.Metadata] [ToFormat T.IDMeta]
 
 ---------------------------------------------------------------------
 
@@ -77,10 +79,8 @@ an example of a `concreteEval` function for `Int.Add`:
 ```
 
 Note that if there is an arity mismatch or if the arguments are not
-concrete/constants, this fails and we return the original term `e`.
+concrete/constants, this fails and it returns .none.
 
-(TODO) Can we enforce well-formedness of the denotation function? E.g., that it
-has the right number and type of arguments, etc.?
 (TODO) Use `.bvar`s in the body to correspond to the formals instead of using
 `.fvar`s.
 -/
@@ -99,6 +99,59 @@ structure LFunc (T : LExprParams) where
   concreteEval : Option (T.Metadata → List (LExpr T.mono) → Option (LExpr T.mono)) := .none
   axioms   : List (LExpr T.mono) := []  -- For axiomatic definitions
 
+/--
+Well-formedness properties of LFunc. These are split from LFunc because
+otherwise it becomes impossible to create a 'temporary' LFunc object whose
+wellformedness might not hold yet.
+-/
+structure LFuncWF {T : LExprParams} (f : LFunc T) where
+  -- No args have same name.
+  arg_nodup:
+    List.Nodup (f.inputs.map (·.1.name))
+  -- Free variables of body must be arguments.
+  body_freevars:
+    ∀ b freevars, f.body = .some b
+      → freevars = LExpr.freeVars b
+      → (∀ fv, fv ∈ freevars →
+          ∃ arg, List.Mem arg f.inputs ∧ fv.1.name = arg.1.name)
+  -- concreteEval does not succeed if the length of args is incorrect.
+  concreteEval_argmatch:
+    ∀ fn md args res, f.concreteEval = .some fn
+      → fn md args = .some res
+      → args.length = f.inputs.length
+
+instance LFuncWF.arg_nodup_decidable {T : LExprParams} (f : LFunc T):
+    Decidable (List.Nodup (f.inputs.map (·.1.name))) := by
+  apply List.nodupDecidable
+
+instance LFuncWF.body_freevars_decidable {T : LExprParams} (f : LFunc T):
+    Decidable (∀ b freevars, f.body = .some b
+      → freevars = LExpr.freeVars b
+      → (∀ fv, fv ∈ freevars →
+          ∃ arg, List.Mem arg f.inputs ∧ fv.1.name = arg.1.name)) :=
+  match Hbody: f.body with
+  | .some b =>
+    if Hall:(LExpr.freeVars b).all
+        (fun fv => List.any f.inputs (fun arg => fv.1.name == arg.1.name))
+    then by
+      apply isTrue
+      intros b' freevars Hb' Hfreevars fv' Hmem
+      cases Hb'
+      rw [← Hfreevars] at Hall
+      rw [List.all_eq_true] at Hall
+      have Hall' := Hall fv' Hmem
+      rw [List.any_eq_true] at Hall'
+      rcases Hall' with ⟨arg', H⟩
+      exists arg'
+      solve | (simp at H ; congr)
+    else by
+      apply isFalse
+      grind
+  | .none => by
+    apply isTrue; grind
+
+-- LFuncWF.concreteEval_argmatch is not decidable.
+
 instance [Inhabited T.Metadata] [Inhabited T.IDMeta] : Inhabited (LFunc T) where
   default := { name := Inhabited.default, inputs := [], output := LMonoTy.bool }
 
@@ -115,7 +168,7 @@ instance : ToFormat (LFunc T) where
        func {f.name} : {type}{sep}\
        {body}"
 
-def LFunc.type (f : (LFunc T)) : Except Format LTy := do
+def LFunc.type [DecidableEq T.IDMeta] (f : (LFunc T)) : Except Format LTy := do
   if !(decide f.inputs.keys.Nodup) then
     .error f!"[{f.name}] Duplicates found in the formals!\
               {Format.line}\
@@ -168,6 +221,23 @@ def Factory.default : @Factory T := #[]
 instance : Inhabited (@Factory T) where
   default := @Factory.default T
 
+instance : Membership (LFunc T) (@Factory T) where
+  mem x f := Array.Mem x f
+
+/--
+Well-formedness properties of Factory.
+-/
+structure FactoryWF {T : LExprParams} (fac:Factory T) where
+  name_nodup:
+    List.Nodup (fac.toList.map (·.name.name))
+  lfuncs_wf:
+    ∀ (lf:LFunc T), lf ∈ fac → LFuncWF lf
+
+instance FactoryWF.name_nodup_decidable {T : LExprParams} (fac : Factory T):
+    Decidable (List.Nodup (fac.toList.map (·.name.name))) := by
+  apply List.nodupDecidable
+
+
 def Factory.getFunctionNames (F : @Factory T) : Array T.Identifier :=
   F.map (fun f => f.name)
 
@@ -186,13 +256,92 @@ def Factory.addFactoryFunc (F : @Factory T) (func : LFunc T) : Except Format (@F
               Existing Function: {func'}\n\
               New Function:{func}"
 
+
+/--
+If Factory.addFactoryFunc succeeds, and the input factory & LFunc were already
+well-formed, the returned factory is also well-formed.
+-/
+theorem Factory.addFactoryFunc_wf
+  (F : @Factory T) (F_wf: FactoryWF F) (func : LFunc T) (func_wf: LFuncWF func):
+  ∀ F', F.addFactoryFunc func = .ok F' → FactoryWF F' :=
+by
+  unfold Factory.addFactoryFunc
+  unfold Factory.getFactoryLFunc
+  intros F' Hmatch
+  split at Hmatch -- Case-analysis on the match condition
+  · rename_i heq
+    cases Hmatch -- F' is Array.push F
+    apply FactoryWF.mk
+    · have Hnn := F_wf.name_nodup
+      grind [Array.toList_push,List]
+    · intros lf Hmem
+      rw [Array.mem_push] at Hmem
+      cases Hmem
+      · have Hwf := F_wf.lfuncs_wf
+        apply Hwf; assumption
+      · grind
+  · grind
+
 /--
 Append a factory `newF` to an existing factory `F`, checking for redefinitions
 along the way.
 -/
 def Factory.addFactory (F newF : @Factory T) : Except Format (@Factory T) :=
   Array.foldlM (fun factory func => factory.addFactoryFunc func) F newF
 
+
+/--
+If Factory.addFactory succeeds, and the input two factories were already
+well-formed, the returned factory is also well-formed.
+-/
+theorem Factory.addFactory_wf
+  (F : @Factory T) (F_wf: FactoryWF F) (newF : @Factory T)
+  (newF_wf: FactoryWF newF):
+  ∀ F', F.addFactory newF = .ok F' → FactoryWF F' :=
+by
+  unfold Factory.addFactory
+  rw [← Array.foldlM_toList]
+  generalize Hl: newF.toList = l
+  induction l generalizing newF F
+  · rw [Array.toList_eq_nil_iff] at Hl
+    rw [List.foldlM_nil]
+    unfold Pure.pure Except.instMonad Except.pure
+    grind
+  · rename_i lf lf_tail tail_ih
+    have Hl: newF = (List.toArray [lf]) ++ (List.toArray lf_tail) := by grind
+    have Htail_wf: FactoryWF (lf_tail.toArray) := by
+      rw [Hl] at newF_wf
+      apply FactoryWF.mk
+      · have newF_wf_name_nodup := newF_wf.name_nodup
+        grind
+      · intro lf
+        have newF_wf_lfuncs_wf := newF_wf.lfuncs_wf lf
+        intro Hmem
+        apply newF_wf_lfuncs_wf
+        apply Array.mem_append_right
+        assumption
+    have Hhead_wf: LFuncWF lf := by
+      rw [Hl] at newF_wf
+      have Hwf := newF_wf.lfuncs_wf
+      apply Hwf
+      apply Array.mem_append_left
+      grind
+    intro F'
+    simp only [List.foldlM]
+    unfold bind
+    unfold Except.instMonad
+    simp only []
+    unfold Except.bind
+    intro H
+    split at H
+    · contradiction
+    · rename_i F_interm HaddFacFun
+      have HF_interm_wf: FactoryWF F_interm := by
+        apply (Factory.addFactoryFunc_wf F F_wf lf) <;> assumption
+      simp only [] at H
+      apply tail_ih F_interm HF_interm_wf (lf_tail.toArray) <;> grind
+
+
 def getLFuncCall {GenericTy} (e : LExpr ⟨T, GenericTy⟩) : LExpr ⟨T, GenericTy⟩ × List (LExpr ⟨T, GenericTy⟩) :=
   go e []
   where go e (acc : List (LExpr ⟨T, GenericTy⟩)) :=

Strata/Languages/Boogie/Factory.lean

@@ -149,8 +149,6 @@ info: [("Neg", "unaryOp"), ("Add", "binaryOp"), ("Sub", "binaryOp"), ("Mul", "bi
 #guard_msgs in
 #eval List.zip BVOpNames BVOpAritys
 
-variable [Coe String BoogieLParams.Identifier]
-
 open Lean Elab Command in
 elab "ExpandBVOpFuncDefs" "[" sizes:num,* "]" : command => do
   for size in sizes.getElems do
@@ -332,8 +330,6 @@ def mapUpdateFunc : LFunc BoogieLParams :=
                     ))))]
      ]
    }
-instance : Coe String BoogieLParams.Identifier where
-  coe | s => ⟨s, .unres⟩
 
 def emptyTriggersFunc : LFunc BoogieLParams :=
     { name := "Triggers.empty",
@@ -401,12 +397,12 @@ def bv64Extract_15_0_Func  := bvExtractFunc 64 15  0
 def bv64Extract_7_0_Func   := bvExtractFunc 64  7  0
 
 def Factory : @Factory BoogieLParams := #[
-  intAddFunc,
-  intSubFunc,
-  intMulFunc,
-  intDivFunc,
-  intModFunc,
-  intNegFunc,
+  @intAddFunc BoogieLParams _,
+  @intSubFunc BoogieLParams _,
+  @intMulFunc BoogieLParams _,
+  @intDivFunc BoogieLParams _,
+  @intModFunc BoogieLParams _,
+  @intNegFunc BoogieLParams _,
 
   @intLtFunc BoogieLParams _,
   @intLeFunc BoogieLParams _,
@@ -468,7 +464,7 @@ def Factory : @Factory BoogieLParams := #[
   bv64Extract_31_0_Func,
   bv64Extract_15_0_Func,
   bv64Extract_7_0_Func,
-] ++ ExpandBVOpFuncNames [1,8,16,32,64]
+] ++ (ExpandBVOpFuncNames [1,8,16,32,64])
 
 open Lean Elab Command in
 elab "DefBVOpFuncExprs" "[" sizes:num,* "]" : command => do
@@ -506,16 +502,16 @@ def addTriggerOp : Expression.Expr := addTriggerFunc.opExpr
 instance : Inhabited (⟨ExpressionMetadata, BoogieIdent⟩: LExprParams).Metadata where
   default := ()
 
-def intAddOp : Expression.Expr := intAddFunc.opExpr
-def intSubOp : Expression.Expr := intSubFunc.opExpr
-def intMulOp : Expression.Expr := intMulFunc.opExpr
-def intDivOp : Expression.Expr := intDivFunc.opExpr
-def intModOp : Expression.Expr := intModFunc.opExpr
-def intNegOp : Expression.Expr := intNegFunc.opExpr
-def intLtOp : Expression.Expr := intLtFunc.opExpr
-def intLeOp : Expression.Expr := intLeFunc.opExpr
-def intGtOp : Expression.Expr := intGtFunc.opExpr
-def intGeOp : Expression.Expr := intGeFunc.opExpr
+def intAddOp : Expression.Expr := (@intAddFunc BoogieLParams _).opExpr
+def intSubOp : Expression.Expr := (@intSubFunc BoogieLParams _).opExpr
+def intMulOp : Expression.Expr := (@intMulFunc BoogieLParams _).opExpr
+def intDivOp : Expression.Expr := (@intDivFunc BoogieLParams _).opExpr
+def intModOp : Expression.Expr := (@intModFunc BoogieLParams _).opExpr
+def intNegOp : Expression.Expr := (@intNegFunc BoogieLParams _).opExpr
+def intLtOp : Expression.Expr := (@intLtFunc BoogieLParams _).opExpr
+def intLeOp : Expression.Expr := (@intLeFunc BoogieLParams _).opExpr
+def intGtOp : Expression.Expr := (@intGtFunc BoogieLParams _).opExpr
+def intGeOp : Expression.Expr := (@intGeFunc BoogieLParams _).opExpr
 def realAddOp : Expression.Expr := realAddFunc.opExpr
 def realSubOp : Expression.Expr := realSubFunc.opExpr
 def realMulOp : Expression.Expr := realMulFunc.opExpr
@@ -525,11 +521,11 @@ def realLtOp : Expression.Expr := realLtFunc.opExpr
 def realLeOp : Expression.Expr := realLeFunc.opExpr
 def realGtOp : Expression.Expr := realGtFunc.opExpr
 def realGeOp : Expression.Expr := realGeFunc.opExpr
-def boolAndOp : Expression.Expr := @boolAndFunc.opExpr BoogieLParams _
-def boolOrOp : Expression.Expr := @boolOrFunc.opExpr BoogieLParams _
-def boolImpliesOp : Expression.Expr := @boolImpliesFunc.opExpr BoogieLParams _
-def boolEquivOp : Expression.Expr := @boolEquivFunc.opExpr BoogieLParams _
-def boolNotOp : Expression.Expr := @boolNotFunc.opExpr BoogieLParams _
+def boolAndOp : Expression.Expr := (@boolAndFunc BoogieLParams _).opExpr
+def boolOrOp : Expression.Expr := (@boolOrFunc BoogieLParams _).opExpr
+def boolImpliesOp : Expression.Expr := (@boolImpliesFunc BoogieLParams _).opExpr
+def boolEquivOp : Expression.Expr := (@boolEquivFunc BoogieLParams _).opExpr
+def boolNotOp : Expression.Expr := (@boolNotFunc BoogieLParams _).opExpr
 def strLengthOp : Expression.Expr := strLengthFunc.opExpr
 def strConcatOp : Expression.Expr := strConcatFunc.opExpr
 def strSubstrOp : Expression.Expr := strSubstrFunc.opExpr
@@ -563,4 +559,43 @@ Get all the built-in functions supported by Boogie.
 def builtinFunctions : Array String :=
   Factory.map (fun f => BoogieIdent.toPretty f.name)
 
+
+set_option maxRecDepth 32768 in
+set_option maxHeartbeats 4000000 in
+/--
+Wellformedness of Factory
+-/
+theorem Factory_wf :
+    FactoryWF Factory := by
+  unfold Factory
+  apply FactoryWF.mk
+  · decide -- FactoryWF.name_nodup
+  · unfold HAppend.hAppend Array.instHAppendList
+    simp only []
+    unfold Array.appendList
+    simp only [List.foldl, Array.push, List.concat]
+    intros lf
+    rw [← Array.mem_toList_iff]
+    simp only []
+    intros Hmem
+    repeat (
+      rcases Hmem with _ | ⟨ a', Hmem ⟩
+      · apply LFuncWF.mk
+        · decide -- LFuncWF.arg_nodup
+        · decide -- LFuncWF.body_freevars
+        · -- LFuncWf.concreteEval_argmatch
+          simp (config := { ground := true })
+          try (
+            try unfold unOpCeval
+            try unfold binOpCeval
+            try unfold cevalIntDiv
+            try unfold cevalIntMod
+            try unfold bvUnaryOp
+            try unfold bvBinaryOp
+            try unfold bvShiftOp
+            try unfold bvBinaryPred
+            intros lf md args res
+            repeat (rcases args with _ | ⟨ args0, args ⟩ <;> try grind)))
+    contradiction
+
 end Boogie

Strata/Languages/Boogie/OldExpressions.lean

@@ -392,6 +392,7 @@ theorem IsOldPredNormalize :
       case neg Hneg' =>
         unfold BoogieIdent.unres at *
         unfold normalizeOldExpr at Hold
+        unfold BoogieIdent.unres at *
         split at Hold <;> simp_all
         split at Hold <;> simp_all
         unfold normalizeOldExpr at Hold

Strata/Languages/Boogie/StatementWF.lean

@@ -30,9 +30,6 @@ theorem typeCheckCmdWF: Statement.typeCheckCmd C T p c = Except.ok v
   sorry
   sorry
   sorry
-  sorry
-  sorry
-  sorry
 
 theorem Statement.typeCheckAux_elim_acc: Statement.typeCheckAux.go C p proc T ss (acc1 ++ acc2) = Except.ok (pp, T') ↔
   (List.IsPrefix acc2.reverse pp ∧ Statement.typeCheckAux.go C p proc T ss acc1 = Except.ok (pp.drop acc2.length, T'))

Strata/Transform/CallElimCorrect.lean

@@ -3317,7 +3317,7 @@ theorem callElimStatementCorrect [LawfulBEq Expression.Expr] :
     <;> simp [pure] at Helim
   next res l =>
     simp [Helim] at *
-    cases Hwf with | intro Hwf =>
+    simp only [Forall, and_true] at Hwf
     cases Hwf with | mk Hwf =>
     simp [Option.isSome] at Hwf
     split at Hwf <;> simp_all
@@ -3329,7 +3329,8 @@ theorem callElimStatementCorrect [LawfulBEq Expression.Expr] :
     | call_sem lkup Hevalargs Hevalouts Hwfval Hwfvars Hwfb Hwf2 Hwf Hinitin Hinitout Hpre Hhav1 Hhav2 Hpost Hrd Hupdate =>
       next outVals argVals σA σAO σO σR p' modvals =>
       unfold BoogieIdent.unres at Hfind
-      have Hsome : (Program.Procedure.find? p procName).isSome := by simp [Hfind]
+      have Hsome : (Program.Procedure.find? p procName).isSome := by
+        grind
       simp [Option.isSome] at Hsome
       unfold BoogieIdent.unres at *
       have lkup' := lkup