diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 304a45c0..d0180376 100644 --- a/.github/workflows/ci.yml +++ b/.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 diff --git a/Strata/DL/Lambda/Factory.lean b/Strata/DL/Lambda/Factory.lean index 68e8341c..7fa3ea66 100644 --- a/Strata/DL/Lambda/Factory.lean +++ b/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,6 +256,32 @@ 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. @@ -193,6 +289,59 @@ 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⟩)) := diff --git a/Strata/Languages/Boogie/Factory.lean b/Strata/Languages/Boogie/Factory.lean index fa049324..d99db8b9 100644 --- a/Strata/Languages/Boogie/Factory.lean +++ b/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 diff --git a/Strata/Languages/Boogie/OldExpressions.lean b/Strata/Languages/Boogie/OldExpressions.lean index a1d6263a..c18e0e70 100644 --- a/Strata/Languages/Boogie/OldExpressions.lean +++ b/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 diff --git a/Strata/Languages/Boogie/StatementWF.lean b/Strata/Languages/Boogie/StatementWF.lean index e9e90c5e..751b41b3 100644 --- a/Strata/Languages/Boogie/StatementWF.lean +++ b/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')) diff --git a/Strata/Transform/CallElimCorrect.lean b/Strata/Transform/CallElimCorrect.lean index c09748d9..c01f5229 100644 --- a/Strata/Transform/CallElimCorrect.lean +++ b/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