Skip to content

Commit

Permalink
Add findLongestMatch function for Zipper, prove equivalence with Rege…
Browse files Browse the repository at this point in the history 
…x' (#122)

* Add findLongestMatch function for Zipper, prove equivalence with Regex'

* fix Forall imports
  • Loading branch information
@samuelchassot
samuelchassot authored Jan 29, 2025
1 parent 2c7a436 commit 3e326b5
Show file tree
Hide file tree
Showing 2 changed files with 227 additions and 5 deletions.
9 changes: 5 additions & 4 deletions lexers/regex/verifiedlexer/src/main/scala/ch/epfl/lexer/Utils.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ import stainless.lang.{ghost => ghostExpr, _}
import stainless.proof.check
import scala.annotation.tailrec
import stainless.lang.StaticChecks._
import stainless.lang.Quantifiers
import ch.epfl.lexer.ListUtils.lemmaSubseqRefl

object SetUtils {
Expand Down Expand Up @@ -435,7 +436,7 @@ object SetUtils {
@ghost
def lemmaFlatMapForallElem[A, B](s: Set[A], f: A => Set[B], p: B => Boolean, elm: B): Unit = {
require(s.flatMap(f).contains(elm))
require(Forall.Forall[A](a => f(a).forall(p)))
require(Quantifiers.Forall[A](a => f(a).forall(p)))

unfold(s.flatMapPost(f)(elm))
assert(s.flatMap(f).contains(elm))
Expand All @@ -444,7 +445,7 @@ object SetUtils {
val witness = ListUtils.getWitness(s.toList, a => f(a).contains(elm))
assert(f(witness).contains(elm))
assert(f(witness).toList.contains(elm))
unfold(Forall.Forall[A](a => f(a).forall(p)))
unfold(Quantifiers.Forall[A](a => f(a).forall(p)))
assert(f(witness).forall(p))
assert(f(witness).toList.forall(p))
ListSpecs.forallContained(f(witness).toList, p, elm)
Expand All @@ -454,7 +455,7 @@ object SetUtils {
@opaque
@ghost
def lemmaFlatMapForallToList[A, B](s: Set[A], f: A => Set[B], p: B => Boolean, l: List[B]): Unit = {
require(Forall.Forall[A](a => f(a).forall(p)))
require(Quantifiers.Forall[A](a => f(a).forall(p)))
require(ListSpecs.subseq(l, s.flatMap(f).toList))
decreases(l)
l match
Expand All @@ -473,7 +474,7 @@ object SetUtils {
@opaque
@ghost
def lemmaFlatMapForall[A, B](s: Set[A], f: A => Set[B], p: B => Boolean): Unit = {
require(Forall.Forall[A](a => f(a).forall(p)))
require(Quantifiers.Forall[A](a => f(a).forall(p)))
ListUtils.lemmaSubseqRefl(s.flatMap(f).toList)
lemmaFlatMapForallToList(s, f, p, s.flatMap(f).toList)

Expand Down
223 changes: 222 additions & 1 deletion lexers/regex/verifiedlexer/src/main/scala/ch/epfl/lexer/VerifiedRegex.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,8 @@ import ch.epfl.map.TupleListOpsGenK.invariantList
import ch.epfl.map.MutableHashMap

import stainless.lang.StaticChecks._
import stainless.annotation.isabelle.lemma


// import ch.epfl.map.OptimisedChecks.*

object MemoisationRegex {
Expand Down Expand Up @@ -551,6 +552,13 @@ object ZipperRegex {
}
}

def derivationZipper[C](z: Zipper[C], input: List[C]): Zipper[C] = {
input match {
case Cons(hd, tl) => derivationZipper(derivationStepZipper(z, hd), tl)
case Nil() => z
}
}

// @inlineOnce
def derivationStepZipper[C](z: Zipper[C], a: C): Zipper[C] = {
z.flatMap(c => derivationStepZipperUp(c, a))
Expand Down Expand Up @@ -2454,6 +2462,211 @@ object ZipperRegex {
}
}.ensuring(_ => matchZipper(z, s) == s.isEmpty)


// --------- Find Longest Match Zipper ------------------------------

def findLongestMatchZipper[C](z: Zipper[C], input: List[C]): (List[C], List[C]) = {
findLongestMatchInnerZipper(z, Nil(), input)
}.ensuring (res => res._1 ++ res._2 == input)

def findLongestMatchInnerZipper[C](z: Zipper[C], testedP: List[C], totalInput: List[C]): (List[C], List[C]) = {
require(ListUtils.isPrefix(testedP, totalInput))
decreases(totalInput.size - testedP.size)

if (testedP == totalInput) {
if (nullableZipper(z)) {
(testedP, Nil[C]())
} else {
(Nil[C](), totalInput)
}
} else {
ghostExpr(ListUtils.lemmaIsPrefixThenSmallerEqSize(testedP, totalInput))
if (testedP.size == totalInput.size) {
ghostExpr(ListUtils.lemmaIsPrefixRefl(totalInput, totalInput))
ghostExpr(ListUtils.lemmaIsPrefixSameLengthThenSameList(totalInput, testedP, totalInput))
check(false)
}
assert(testedP.size < totalInput.size)
val suffix = ListUtils.getSuffix(totalInput, testedP)
val newP = testedP ++ List(suffix.head)
ghostExpr(ListUtils.lemmaAddHeadSuffixToPrefixStillPrefix(testedP, totalInput))
if (nullableZipper(z)) {
val recursive = findLongestMatchInnerZipper(derivationStepZipper(z, suffix.head), newP, totalInput)
if (recursive._1.isEmpty) {
(testedP, ListUtils.getSuffix(totalInput, testedP))
} else {
recursive
}
} else {
findLongestMatchInnerZipper(derivationStepZipper(z, suffix.head), newP, totalInput)
}
}
}.ensuring (res => res._1 ++ res._2 == totalInput && (res._1.isEmpty || res._1.size >= testedP.size))

// ----------------------------- Find Longest Match Zipper Theorems ------------------------------

@ghost
def longestMatchSameAsRegex[C](r: Regex[C], z: Zipper[C], input: List[C]): Unit = {
require(validRegex(r))
require(unfocusZipper(z.toList) == r)

val (longestPrefixZ, suffixZ) = findLongestMatchZipper(z, input)
val (longestPrefixR, suffixR) = findLongestMatch(r, input)

assert(longestPrefixZ ++ suffixZ == input)
assert(longestPrefixR ++ suffixR == input)
ListUtils.lemmaConcatTwoListThenFirstIsPrefix(longestPrefixZ, suffixZ)
ListUtils.lemmaConcatTwoListThenFirstIsPrefix(longestPrefixR, suffixR)

longestMatchIsAcceptedByMatchOrIsEmpty(z, input)
VerifiedRegexMatcher.longestMatchIsAcceptedByMatchOrIsEmpty(r, input)
assert(matchZipper(z, longestPrefixZ) || longestPrefixZ.isEmpty)
assert(matchR(r, longestPrefixR) || longestPrefixR.isEmpty)
theoremZipperRegexEquiv(z, z.toList, r, longestPrefixR)
theoremZipperRegexEquiv(z, z.toList, r, longestPrefixZ)

if(longestPrefixR.size > longestPrefixZ.size){
longestMatchNoBiggerStringMatch(z, input, longestPrefixZ, longestPrefixR)
check(false)
} else if(longestPrefixZ.size > longestPrefixR.size){
VerifiedRegexMatcher.longestMatchNoBiggerStringMatch(r, input, longestPrefixR, longestPrefixZ)
check(false)
} else{
ListUtils.lemmaIsPrefixSameLengthThenSameList(longestPrefixZ, longestPrefixR, input)
ListUtils.lemmaSamePrefixThenSameSuffix(longestPrefixZ, suffixZ, longestPrefixR, suffixR, input)
assert(longestPrefixZ == longestPrefixR)
assert(suffixZ == suffixR)
}
}.ensuring(_ => findLongestMatchZipper(z, input) == findLongestMatch(r, input))


@ghost
def longestMatchIsAcceptedByMatchOrIsEmpty[C](z: Zipper[C], input: List[C]): Unit = {
longestMatchIsAcceptedByMatchOrIsEmptyRec(z, z, Nil(), input)

}.ensuring (_ => findLongestMatchInnerZipper(z, Nil(), input)._1.isEmpty || matchZipper(z, findLongestMatchInnerZipper(z, Nil(), input)._1))

@ghost
def longestMatchNoBiggerStringMatch[C](baseZ: Zipper[C], input: List[C], returnP: List[C], bigger: List[C]): Unit = {
require(ListUtils.isPrefix(returnP, input))
require(ListUtils.isPrefix(bigger, input))
require(bigger.size >= returnP.size)
require(findLongestMatchInnerZipper(baseZ, Nil(), input)._1 == returnP)

if (bigger.size == returnP.size) {
ListUtils.lemmaIsPrefixSameLengthThenSameList(bigger, returnP, input)
} else {
if (matchZipper(baseZ, bigger)) {
lemmaKnownAcceptedStringThenFromSmallPAtLeastThat(baseZ, baseZ, input, Nil(), bigger)
check(false)
}
}

}.ensuring (_ => bigger == returnP || !matchZipper(baseZ, bigger))


// ----------------------------- Find Longest Match Zipper Lemmas ------------------------------
@ghost
def lemmaKnownAcceptedStringThenFromSmallPAtLeastThat[C](baseZ: Zipper[C], z: Zipper[C], input: List[C], testedP: List[C], knownP: List[C]): Unit = {
require(ListUtils.isPrefix(testedP, input))
require(ListUtils.isPrefix(knownP, input))
require(knownP.size >= testedP.size)
require(matchZipper(baseZ, knownP))
require(derivationZipper(baseZ, testedP) == z)
decreases(knownP.size - testedP.size)

if (testedP.size == knownP.size) {
ListUtils.lemmaIsPrefixSameLengthThenSameList(testedP, knownP, input)
lemmaIfMatchZipperThenLongestMatchFromThereReturnsAtLeastThis(baseZ, z, input, testedP)
check(findLongestMatchInnerZipper(z, testedP, input)._1.size >= knownP.size)
} else {
assert(testedP.size < input.size)
val suffix = ListUtils.getSuffix(input, testedP)
val newP = testedP ++ List(suffix.head)
ListUtils.lemmaAddHeadSuffixToPrefixStillPrefix(testedP, input)

lemmaDerivativeOnLWithANewCharIsANewDerivativeStep(baseZ, z, testedP, suffix.head)
lemmaKnownAcceptedStringThenFromSmallPAtLeastThat(baseZ, derivationStepZipper(z, suffix.head), input, newP, knownP)

check(findLongestMatchInnerZipper(z, testedP, input)._1.size >= knownP.size)
}

}.ensuring (_ => findLongestMatchInnerZipper(z, testedP, input)._1.size >= knownP.size)

@ghost
def lemmaIfMatchZipperThenLongestMatchFromThereReturnsAtLeastThis[C](baseZ: Zipper[C], z: Zipper[C], input: List[C], testedP: List[C]): Unit = {
require(ListUtils.isPrefix(testedP, input))
require(matchZipper(baseZ, testedP))
require(derivationZipper(baseZ, testedP) == z)

lemmaMatchZipperIsSameAsWholeDerivativeAndNil(baseZ, testedP)
assert(matchZipper(z, Nil()))
assert(nullableZipper(z))

}.ensuring (_ => findLongestMatchInnerZipper(z, testedP, input)._1.size >= testedP.size)

@ghost
def longestMatchIsAcceptedByMatchOrIsEmptyRec[C](baseZ: Zipper[C], z: Zipper[C], testedP: List[C], input: List[C]): Unit = {
require(ListUtils.isPrefix(testedP, input))
require(derivationZipper(baseZ, testedP) == z)
decreases(input.size - testedP.size)

if (findLongestMatchInnerZipper(z, testedP, input)._1.isEmpty) {
()
} else {
if (testedP == input) {
if (nullableZipper(z)) {
lemmaMatchZipperIsSameAsWholeDerivativeAndNil(baseZ, testedP)
} else {
()
}
} else {
ListUtils.lemmaIsPrefixThenSmallerEqSize(testedP, input)
if (testedP.size == input.size) {
ListUtils.lemmaIsPrefixRefl(input, input)
ListUtils.lemmaIsPrefixSameLengthThenSameList(input, testedP, input)
check(false)
}
assert(testedP.size < input.size)
val suffix = ListUtils.getSuffix(input, testedP)
val newP = testedP ++ List(suffix.head)
ListUtils.lemmaAddHeadSuffixToPrefixStillPrefix(testedP, input)
if (nullableZipper(z)) {
val recursive = findLongestMatchInnerZipper(derivationStepZipper(z, suffix.head), newP, input)
if (recursive._1.isEmpty) {
lemmaMatchZipperIsSameAsWholeDerivativeAndNil(baseZ, testedP)
} else {
lemmaDerivativeOnLWithANewCharIsANewDerivativeStep(baseZ, z, testedP, suffix.head)
longestMatchIsAcceptedByMatchOrIsEmptyRec(baseZ, derivationStepZipper(z, suffix.head), newP, input)
}
} else {
lemmaDerivativeOnLWithANewCharIsANewDerivativeStep(baseZ, z, testedP, suffix.head)
longestMatchIsAcceptedByMatchOrIsEmptyRec(baseZ, derivationStepZipper(z, suffix.head), newP, input)
}
}
}

}.ensuring (_ => findLongestMatchInnerZipper(z, testedP, input)._1.isEmpty || matchZipper(baseZ, findLongestMatchInnerZipper(z, testedP, input)._1))

@ghost
def lemmaMatchZipperIsSameAsWholeDerivativeAndNil[C](z: Zipper[C], input: List[C]): Unit = {
input match {
case Cons(hd, tl) => lemmaMatchZipperIsSameAsWholeDerivativeAndNil(derivationStepZipper(z, hd), tl)
case Nil() => ()
}
}.ensuring (_ => matchZipper(z, input) == matchZipper(derivationZipper(z, input), Nil()))

@ghost
def lemmaDerivativeOnLWithANewCharIsANewDerivativeStep[C](baseZ: Zipper[C], z: Zipper[C], input: List[C], c: C): Unit = {
require(derivationZipper(baseZ, input) == z)

input match {
case Cons(hd, tl) => lemmaDerivativeOnLWithANewCharIsANewDerivativeStep(derivationStepZipper(baseZ, hd), z, tl, c)
case Nil() => ()
}

}.ensuring (_ => derivationZipper(baseZ, input ++ List(c)) == derivationStepZipper(z, c))

}

object VerifiedRegexMatcher {
Expand Down Expand Up @@ -2859,6 +3072,14 @@ object VerifiedRegexMatcher {

}.ensuring (res => (res.isDefined && matchR(r1, res.get._1) && matchR(r2, res.get._2) && res.get._1 ++ res.get._2 == s) || !res.isDefined)

def findLongestMatchWithZipper[C](r: Regex[C], input: List[C]): (List[C], List[C]) = {
require(validRegex(r))
val zipper = ZipperRegex.focus(r)
ghostExpr(ZipperRegex.longestMatchSameAsRegex(r, zipper, input))
ZipperRegex.findLongestMatchInnerZipper(zipper, Nil(), input)
}.ensuring (res => res == findLongestMatch(r, input))


def findLongestMatch[C](r: Regex[C], input: List[C]): (List[C], List[C]) = {
require(validRegex(r))
findLongestMatchInner(r, Nil(), input)
Expand Down

0 comments on commit 3e326b5

Please sign in to comment.