Skip to content

Commit

Permalink
@ induct support.
Browse files Browse the repository at this point in the history
  • Loading branch information
@robby-phd
robby-phd committed Mar 19, 2024
1 parent 1c849d7 commit 042d4d7
Show file tree
Hide file tree
Showing 4 changed files with 97 additions and 22 deletions.
14 changes: 6 additions & 8 deletions jvm/src/test/scala/org/sireum/logika/example/list.sc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -107,7 +107,6 @@ object List {
}
}

/*
@pure def emptyZeroLengthInduct[T](l: List[T]): Unit = {
Contract(
Ensures(l.length >= 0)
Expand All @@ -117,26 +116,25 @@ object List {
case Cons(value, next) => {
Deduce(
//@formatter:off
1 ( l ≡ Cons[T](value, next) ) by Auto,
2 ( next.length >= 0 ) by Admit, // Premise,
3 ( l.length ≡ (1 + next.length) ) by Simpl,
4 ( l.length >= 0 ) by Auto and (2, 3)
1 ( l ≡ List.Cons[T](value, next) ) by Premise, // auto-generated
2 ( next.length >= 0 ) by Premise, // auto-generated
3 ( l.length ≡ (1 + next.length) ) by Simpl,
4 ( l.length >= 0 ) by Auto and (2, 3)
//@formatter:on
)
return
}
case Nil() => {
Deduce(
//@formatter:off
1 ( l ≡ Nil[T]() ) by Auto,
2 ( l.length >= 0 ) by Simpl
1 ( l ≡ List.Nil[T]() ) by Premise, // auto-generated
2 ( l.length >= 0 ) by Simpl
//@formatter:on
)
return
}
}
}
*/

type Map[K, V] = List[(K, V)]

Expand Down
26 changes: 13 additions & 13 deletions jvm/src/test/scala/org/sireum/logika/example/z-ordering.sc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,11 +9,11 @@ import org.sireum.justification.natded.prop.ImplyI
@strictpure def isOrderedH(seq: ZS): B = All(0 until seq.size)(i => All(i until seq.size)(j => seq(i) <= seq(j)))

@pure def ordered1Lemma(seq: ZS): Unit = {
Deduce(|- (isOrderedH(seq) ->: isOrdered(seq)))
Deduce(|- (isOrderedH(seq) __>: isOrdered(seq)))
}

//@pure def ordered2LemmaFail(seq: ZS): Unit = {
// Deduce(|- (isOrdered(seq) ->: isOrderedH(seq))) // Could not deduce
// Deduce(|- (isOrdered(seq) __>: isOrderedH(seq))) // Could not deduce
//}

@pure def ordered2Lemma(seq: ZS): Unit = {
Expand Down Expand Up @@ -42,8 +42,8 @@ import org.sireum.justification.natded.prop.ImplyI
m = m + 1
Deduce( // required when SMT2 query is simplified
//@formatter:off
1 #> All(n until m - 1)(j => seq(n) <= seq(j)) by Auto,
2 #> ((m - 2 >= 0) -->: (seq(m - 2) <= seq(m - 1))) by Auto
1 ( All(n until m - 1)(j => seq(n) <= seq(j)) ) by Auto,
2 ( (m - 2 >= 0) ___>: (seq(m - 2) <= seq(m - 1)) ) by Auto
//@formatter:on
)
}
Expand All @@ -54,13 +54,13 @@ import org.sireum.justification.natded.prop.ImplyI
@pure def orderedEqTheorem(seq: ZS): Unit = {
Deduce(|- (isOrderedH(seq) == isOrdered(seq)) Proof(
//@formatter:off
1 #> (isOrderedH(seq) ->: isOrdered(seq)) by ordered1Lemma(seq),
4 #> SubProof(
5 #> Assume(isOrdered(seq)),
6 #> isOrderedH(seq) by ordered2Lemma(seq) and 5
1 ( isOrderedH(seq) __>: isOrdered(seq) ) by ordered1Lemma(seq),
2 #> SubProof(
3 #> Assume( isOrdered(seq) ),
4 ( isOrderedH(seq) ) by ordered2Lemma(seq) and 3
),
2 #> (isOrdered(seq) ->: isOrderedH(seq)) by ImplyI(4),
3 #> (isOrderedH(seq) == isOrdered(seq)) by Auto and (1, 2)
5 ( isOrdered(seq) __>: isOrderedH(seq) ) by ImplyI(2),
6 ( isOrderedH(seq) == isOrdered(seq) ) by Auto and (1, 5)
//@formatter:on
))
}
Expand All @@ -69,9 +69,9 @@ import org.sireum.justification.natded.prop.ImplyI
@pure def orderedEqTheoremUsingLift(seq: ZS): Unit = {
Deduce(|- (isOrderedH(seq) == isOrdered(seq)) Proof(
//@formatter:off
1 #> (isOrderedH(seq) ->: isOrdered(seq)) by ordered1Lemma(seq),
2 #> (isOrdered(seq) -->: isOrderedH(seq)) by Lift(ordered2Lemma(seq)),
3 #> (isOrderedH(seq) == isOrdered(seq)) by Auto and (1, 2)
1 ( isOrderedH(seq) __>: isOrdered(seq) ) by ordered1Lemma(seq),
2 ( isOrdered(seq) ___>: isOrderedH(seq) ) by Lift(ordered2Lemma(seq)),
3 ( isOrderedH(seq) == isOrdered(seq) ) by Auto and (1, 2)
//@formatter:on
))
}
77 changes: 76 additions & 1 deletion shared/src/main/scala/org/sireum/logika/Logika.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4517,7 +4517,6 @@ import Util._

def evalMatch(split: Split.Type, smt2: Smt2, cache: Logika.Cache, rOpt: Option[State.Value.Sym], rtCheck: B, state: State,
stmt: AST.Stmt.Match, reporter: Reporter): ISZ[State] = {

def evalCasePattern(s1: State, lcontext: ISZ[String], c: AST.Case, v: State.Value): (State, State.Value.Sym, Bindings, HashMap[String, (Z, ISZ[Position])]) = {
val (s2, pcond, m) = evalPattern(smt2, cache, rtCheck, s1, v, c.pattern, reporter)
val (s3, bindings) = addBindings(smt2, cache, rtCheck, s2, lcontext, m, reporter)
Expand All @@ -4543,6 +4542,82 @@ import Util._
val (s9, locals) = rewriteLocals(s8, F, lcontext, m.keys)
return (s9, sym, m, HashMap.empty[String, (Z, ISZ[Position])] ++ (for (p <- locals.entries) yield (p._1._2, (p._2._2, p._2._1))))
}
def evalInductMatch(): ISZ[State] = {
@pure def unifyPattern(p1: AST.Pattern, p2: AST.Pattern): Option[HashMap[AST.Exp, AST.Exp]] = {
@strictpure def ident(vb: AST.Pattern.VarBinding): AST.Exp =
AST.Exp.Ident(vb.id, AST.ResolvedAttr(vb.attr.posOpt, Some(AST.ResolvedInfo.LocalVar(vb.idContext, AST.ResolvedInfo.LocalVar.Scope.Current, F, T, vb.id.value)), vb.attr.typedOpt))
(p1, p2) match {
case (p1: AST.Pattern.Ref, p2: AST.Pattern.Ref) if p1.attr.resOpt == p2.attr.resOpt => return Some(HashMap.empty)
case (p1: AST.Pattern.VarBinding, p2: AST.Pattern.VarBinding) if p1.id.value == p2.id.value && p1.idContext == p2.idContext =>
return Some(HashMap.empty[AST.Exp, AST.Exp] + ident(p1) ~> ident(p2))
case (p1: AST.Pattern.Structure, p2: AST.Pattern.Structure) if p1.attr.typedOpt == p2.attr.typedOpt =>
var m = HashMap.empty[AST.Exp, AST.Exp]
for (i <- 0 until p1.patterns.size) {
unifyPattern(p1.patterns(i), p2.patterns(i)) match {
case Some(m2) => m = m ++ m2.entries
case _ => return None()
}
}
return Some(m)
case _ => return None()
}
}
val posOpt = stmt.exp.posOpt
val cm = context.methodOpt.get
val claim: AST.Exp =
if (cm.requires.isEmpty) AST.Util.bigAnd(cm.ensures, posOpt)
else AST.Util.bigImply(T, cm.requires :+ AST.Util.bigAnd(cm.ensures, posOpt), posOpt)
var (s1, v) = evalExp(Split.Disabled, smt2, cache, rtCheck, state, stmt.exp, reporter)(0)
var branches = ISZ[Branch]()
lang.FrontEnd.induct(th, HashSet.empty, context.methodName, claim, stmt.exp, posOpt.get) match {
case Some(ir) =>
val lcontext = context.methodName
var cases = ir.cases
for (cas <- stmt.cases) {
var found = F
for (icas <- ir.cases if !found) {
unifyPattern(cas.pattern, icas.pattern) match {
case Some(sm) =>
found = T
cases = cases - icas
val premises: ISZ[AST.Exp] = if (sm.isEmpty) {
icas.premises
} else {
val es = AST.Util.ExpSubstitutor(sm)
for (p <- icas.premises) yield es.transformExp(p).getOrElse(p)
}
val (s2, sym, m, bidMap) = evalCasePattern(s1, lcontext, cas, v)
s1 = s2
val assumeAttr = AST.ResolvedAttr(posOpt, TypeChecker.assumeResOpt, TypeChecker.assertumeTypedOpt)
val assumeIdent = AST.Exp.Ident(AST.Id("assume", AST.Attr(posOpt)), assumeAttr)
val exprAttr = AST.TypedAttr(posOpt, AST.Typed.unitOpt)
val assumes: ISZ[AST.Stmt] = for (p <- premises) yield AST.Stmt.Expr(
AST.Exp.Invoke(None(), assumeIdent, ISZ(), ISZ(p), assumeAttr), exprAttr)
branches = branches :+ Branch("match case pattern", sym,
cas.body(stmts = assumes ++ cas.body.stmts), m, bidMap)
case _ =>
}
}
if (!found) {
reporter.error(cas.pattern.posOpt, kind, s"Could not match the induction pattern")
}
}
val (s3, leafClaims) = evalBranches(T, split, smt2, cache, rtCheck, rOpt, lcontext, s1, branches, reporter)
val shouldSplit: B = split match {
case Split.Default => config.splitAll || config.splitMatch
case Split.Enabled => T
case Split.Disabled => F
}
return mergeBranches(shouldSplit, s3, leafClaims)
case _ =>
reporter.error(posOpt, kind, st"Could not induct on ${stmt.exp.prettyST}".render)
return ISZ(state(status = State.Status.Error))
}
}

if (stmt.isInduct) {
return evalInductMatch()
}

var r = ISZ[State]()
val lcontext: ISZ[String] = context.methodOpt match {
Expand Down
2 changes: 2 additions & 0 deletions shared/src/main/scala/org/sireum/logika/Util.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -894,10 +894,12 @@ object Util {
case AST.Exp.BinaryOp.CondAnd => (let.op, AST.ResolvedInfo.BuiltIn.Kind.BinaryCondAnd)
case AST.Exp.BinaryOp.CondOr => (let.op, AST.ResolvedInfo.BuiltIn.Kind.BinaryCondOr)
case AST.Exp.BinaryOp.CondImply => (let.op, AST.ResolvedInfo.BuiltIn.Kind.BinaryCondImply)
case "-->:" => (AST.Exp.BinaryOp.CondImply, AST.ResolvedInfo.BuiltIn.Kind.BinaryCondImply)
case AST.Exp.BinaryOp.And => (let.op, AST.ResolvedInfo.BuiltIn.Kind.BinaryAnd)
case AST.Exp.BinaryOp.Or => (let.op, AST.ResolvedInfo.BuiltIn.Kind.BinaryOr)
case AST.Exp.BinaryOp.Xor => (let.op, AST.ResolvedInfo.BuiltIn.Kind.BinaryXor)
case AST.Exp.BinaryOp.Imply => (let.op, AST.ResolvedInfo.BuiltIn.Kind.BinaryImply)
case "->:" => (AST.Exp.BinaryOp.Imply, AST.ResolvedInfo.BuiltIn.Kind.BinaryImply)
case AST.Exp.BinaryOp.Eq => (let.op, AST.ResolvedInfo.BuiltIn.Kind.BinaryEq)
case AST.Exp.BinaryOp.Equiv => (AST.Exp.BinaryOp.EquivUni, AST.ResolvedInfo.BuiltIn.Kind.BinaryEquiv)
case AST.Exp.BinaryOp.EquivUni => (let.op, AST.ResolvedInfo.BuiltIn.Kind.BinaryEquiv)
Expand Down

0 comments on commit 042d4d7

Please sign in to comment.