diff --git a/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/lexer/Utils.scala b/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/lexer/Utils.scala index 66e79192..6a252e54 100644 --- a/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/lexer/Utils.scala +++ b/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/lexer/Utils.scala @@ -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 { @@ -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)) @@ -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) @@ -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 @@ -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) diff --git a/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/lexer/VerifiedRegex.scala b/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/lexer/VerifiedRegex.scala index c5f8e1cf..be8f38de 100644 --- a/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/lexer/VerifiedRegex.scala +++ b/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/lexer/VerifiedRegex.scala @@ -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 { @@ -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)) @@ -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 { @@ -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)