Merge pull request #9 from verse-lab/simple-tester

A simple testing mechanism

Author: F47-503

CaseStudies/Extension.lean

@@ -45,3 +45,22 @@ initialize velvetObligations :
         res := res.union <| Std.HashMap.ofList a.toList
       return res
   }
+
+/-- Storing slightly more information than `VelvetObligation`.  -/
+structure VelvetTestingCtx extends VelvetObligation where
+  newIds : Array Ident
+  modBinders : Array (TSyntax `Lean.Parser.Term.bracketedBinder)
+deriving Inhabited
+
+abbrev VelvetTestingContextMap := Std.HashMap Name VelvetTestingCtx
+
+initialize velvetTestingContextMap :
+  SimplePersistentEnvExtension (Name × VelvetTestingCtx) VelvetTestingContextMap ←
+  registerSimplePersistentEnvExtension {
+    addEntryFn := fun s (n, o) => s.insert n o
+    addImportedFn := fun as => Id.run do
+      let mut res : VelvetTestingContextMap := ∅
+      for a in as do
+        res := res.union <| Std.HashMap.ofList a.toList
+      return res
+  }

CaseStudies/TestingUtil.lean

@@ -0,0 +1,31 @@
+import Aesop
+import Batteries.Tactic.PermuteGoals
+import Batteries.Tactic.Basic
+
+def Decidable.Nat.decidableBallLT' {p : Nat → Prop} (n : Nat)
+  [∀ i, Decidable (p i)] :
+  ((∀ i, i < n → p i) ↔ (∀ i, p i)) → Decidable (∀ i, p i) := by
+  intro h ; rw [← h] ; infer_instance
+
+open Lean Meta Macro Parser Tactic in
+def deriveDecidableNatUpperBound (tms : List <| TSyntax `term)
+  : MacroM (TSyntax `Lean.Parser.Tactic.tacticSeq) := do
+  match tms with
+  | [] => `(Lean.Parser.Tactic.tacticSeq| (infer_instance) )
+  | tm :: tms' =>
+    let res ← deriveDecidableNatUpperBound tms'
+    let h := mkIdent `h
+    `(Lean.Parser.Tactic.tacticSeq|
+      refine @$(mkIdent ``Decidable.Nat.decidableBallLT') _ ($tm) ?_ ?_
+      on_goal 1=> intro _
+      on_goal 1=>
+        $res
+      constructor
+      next => (intro $h:ident ; intros ; apply $h:ident <;> (try split_ands) <;> (solve
+          | omega
+          | aesop))
+      next => aesop)
+
+macro "decidable_by_nat_upperbound" "[" tms:term,* "]" : term => do
+  let res ← deriveDecidableNatUpperBound tms.getElems.toList
+  `(term| by $res)

CaseStudies/Velvet/Syntax.lean

@@ -223,7 +223,7 @@ elab_rules : command
   $[require $req:term]*
   $[ensures $ens:term]* do $doSeq:doSeq
   ) => do
-  let (defCmd, obligation) ← Command.runTermElabM fun _vs => do
+  let (defCmd, obligation, testingCtx) ← Command.runTermElabM fun _vs => do
     let bindersIdents ← toBracketedBinderArrayLeafny binders
 
     let modIds ← getModIds binders
@@ -251,6 +251,9 @@ elab_rules : command
     let pre <- req.andListWithName reqName
     let post <- ens.andListWithName ensName
 
+    let namelessPre <- req.andList
+    let namelessPost <- ens.andList
+
     let mut ret <- `(term| ())
     for modId in modIds do
       let modId := mkIdent <| modId.getId.appendAfter "New"
@@ -265,9 +268,13 @@ elab_rules : command
       pre := pre
       post := post
     }
-    return (defCmd, obligation)
+    let newIds := modIds.map (fun x => Lean.mkIdent <| x.getId.appendAfter "New")
+    let modBinders ← newIds.zip mutTypes |>.mapM fun (newId, mutType) =>
+      `(bracketedBinder| ($newId : $mutType))
+    return (defCmd, obligation, { obligation with pre := namelessPre , post := namelessPost , modBinders , newIds })
   elabCommand defCmd
   velvetObligations.modify (·.insert name.getId obligation)
+  velvetTestingContextMap.modify (·.insert name.getId testingCtx)
 
 notation "{" P "}" c "{" v "," Q "}" => triple P c (fun v => Q)
 
@@ -302,3 +309,88 @@ elab_rules : command
 
 set_option linter.unusedVariables false in
 def atomicAssertion {α : Type u} (n : Name) (a : α) := a
+
+syntax "extract_program_for" ident : command
+syntax "prove_precondition_decidable_for" ident ("by" tacticSeq)? : command
+syntax "prove_postcondition_decidable_for" ident ("by" tacticSeq)? : command
+syntax "derive_tester_for" ident : command
+
+def obtainVelvetTestingCtx (nameRaw : Ident) : CommandElabM (VelvetTestingCtx × Name) := do
+  let ctxMap ← velvetTestingContextMap.get
+  let name := nameRaw.getId
+  unless ctxMap.contains name do
+    throwError "{name} is not a Velvet program"
+  return (ctxMap[name]!, name)
+
+elab_rules : command
+  | `(command| extract_program_for $nameRaw:ident ) => do
+  -- assuming the thing is computable, then extract the program first
+  let (ctx, name) ← obtainVelvetTestingCtx nameRaw
+  let bindersIdents := ctx.binderIdents
+  let ids := ctx.ids
+  let execName := name.appendAfter "Exec"
+  let execDefCmd ← `(command|
+    def $(mkIdent execName) $bindersIdents* :=
+      $(mkIdent ``NonDetT.extractWeak) ($nameRaw $ids*) (by extract_tactic))
+  elabCommand execDefCmd
+
+def elabDefiningDecidableInstancesForVelvetSpec (nameRaw : Ident)
+    (pre? : Bool) (tac : Option (TSyntax `Lean.Parser.Tactic.tacticSeq)) : CommandElabM Unit := do
+  let (ctx, name) ← obtainVelvetTestingCtx nameRaw
+  let bindersIdents := ctx.binderIdents
+  let (target, suffix, binders) :=
+    if pre?
+    then (ctx.pre, "PreDecidable", bindersIdents)
+    else (ctx.post, "PostDecidable", bindersIdents ++ ctx.modBinders)
+  let decidableInstName := name.appendAfter suffix
+  -- let proof := tac.getD (← `(term| (by infer_instance) ))
+  let tac := tac.getD (← `(Lean.Parser.Tactic.tacticSeq| skip ))
+  let proof := (← `(Lean.Parser.Tactic.tacticSeq|
+    repeat' refine @instDecidableAnd _ _ ?_ ?_
+    all_goals (try infer_instance)
+    ($tac) ))
+  let decidableInstDefCmd ← `(command|
+    def $(mkIdent decidableInstName) $binders* :
+      $(mkIdent ``Decidable) ($target) := by $proof)
+  elabCommand decidableInstDefCmd
+
+elab_rules : command
+  | `(command| prove_precondition_decidable_for $nameRaw:ident ) => do
+    elabDefiningDecidableInstancesForVelvetSpec nameRaw true none
+  | `(command| prove_precondition_decidable_for $nameRaw:ident by $tac) => do
+    elabDefiningDecidableInstancesForVelvetSpec nameRaw true (some tac)
+  | `(command| prove_postcondition_decidable_for $nameRaw:ident ) => do
+    elabDefiningDecidableInstancesForVelvetSpec nameRaw false none
+  | `(command| prove_postcondition_decidable_for $nameRaw:ident by $tac) => do
+    elabDefiningDecidableInstancesForVelvetSpec nameRaw false (some tac)
+
+elab_rules : command
+  | `(command| derive_tester_for $nameRaw:ident ) => do
+  let (ctx, name) ← obtainVelvetTestingCtx nameRaw
+  let execName ← do
+    try resolveGlobalConstNoOverloadCore <| name.appendAfter "Exec"
+    catch _ =>
+      throwError "no executable found for {name}, please extract the program first"
+  let ids := ctx.ids
+  let retId := ctx.retId
+  let ret := ctx.ret
+  let bindersIdents := ctx.binderIdents
+  let bundle (pre? : Bool) := if pre?
+    then (ctx.pre, name.appendAfter "PreDecidable", ids)
+    else (ctx.post, name.appendAfter "PostDecidable", ids ++ ctx.newIds)
+  let decideTerm bundled : CommandElabM (TSyntax `term) := do
+    let (target, instname, args) := bundled
+    try
+      let instname ← resolveGlobalConstNoOverloadCore instname
+      `(term| (@$(mkIdent ``decide) _ ($(Syntax.mkApp (mkIdent instname) args))))
+    catch _ =>
+      `(term| ($(mkIdent ``decide) ($target)))
+  let matcherTerm ← `(term|
+      match ($(Syntax.mkApp (mkIdent execName) ids)) with
+      | $(mkIdent ``DivM.res) ⟨$retId, $ret⟩ => $(← decideTerm <| bundle false)
+      | _ => false)
+  let ifTerm ← `(term| if $(← decideTerm <| bundle true) then $matcherTerm else true)
+  let testerName := name.appendAfter "Tester"
+  let testerDefCmd ← `(command|
+    def $(mkIdent testerName) $bindersIdents* : Bool := $ifTerm)
+  elabCommand testerDefCmd

CaseStudies/Velvet/VelvetExamples/Examples.lean

@@ -9,6 +9,7 @@ import Loom.MonadAlgebras.WP.Tactic
 import Loom.MonadAlgebras.WP.DoNames'
 
 import CaseStudies.Velvet.Std
+import CaseStudies.TestingUtil
 
 open PartialCorrectness DemonicChoice Lean.Elab.Term.DoNames
 
@@ -91,6 +92,25 @@ method insertionSort
         mind := mind - 1
       n := n + 1
     return
+
+extract_program_for insertionSort
+prove_precondition_decidable_for insertionSort
+prove_postcondition_decidable_for insertionSort by
+  (exact (decidable_by_nat_upperbound [(size arr), (size arr)]))
+derive_tester_for insertionSort
+
+-- doing simple testing
+run_elab do
+  let g : Plausible.Gen (_ × Bool) := do
+    let arr ← Plausible.SampleableExt.interpSample (Array Int)
+    let res := insertionSortTester arr
+    pure (arr, res)
+  for _ in [1: 500] do
+    let res ← Plausible.Gen.run g 10
+    unless res.2 do
+      IO.println s!"postcondition violated for input {res.1}"
+      break
+
 prove_correct insertionSort by
   dsimp [insertionSort]
   loom_solve