Proving a refactor is correct and the new code behaves correctly relative to old code

[seebees]

Sometimes I want to refactor some code.
Compose/decompose or just move things around.
These kinds of changes can get rather complicated
and involve lots of small changes,
especially in Dafny with all the details I can put into specifications.

As I work the problem the scope of change can get mingled with what was previously correct.
To try and avoid this I will often write a lemma to prove that my two "ways" are equivalent.

However, the problem comes when I want to commit something.
The goal of the refactor is to not leave the old code around.
So while the lemma is useful to me,
and maybe it could exist in the PR for a time,
eventually it needs to be removed.
It needs to be removed because the code that it is based on is getting removed.
Once it is removed, if any additional changes happen,
how do I know that everything is still equivalent?

My idea was to have a way to include a file from a git SHA1.
Obviously this would need to be carefully done,
but it would let me commit a lemma that includes code from a previous version of a file in git history.
In fact, this verification could stick around after the refactor to ensure correctness.

I offer an example.
Say I have a predicate function that defines a type of Valid.

module Foo
  predicate method ValidBar(bar: Bar){
    //Something important
  }
}

I want to move this predicate and expand on it slightly.
I also want to start using a Subset type based on this new predicate.
Rather than having requires ValidBar all over the place.

module NotFoo {
  predicate method MoreValidBar(bar: Bar) {
    // `ValidBar` is a SubSet of MoreValidBar requirements
  }
  type BetterBar = b: Bar | MoreValidBar(b)
}

Now for the magic.
I was thinking of something like this.

include "NotFoo.dfy"
gitInclude "SHA1/Foo.dfy"

module IntegrationMagic {
  import NotFoo
  gitImport Foo = SHA1.Foo

  lemma NeverBreakOldCode(b: NotFoo.BetterBar)
    ensures Foo.ValidBar(b)
  {}

SHA1 is the git commit with Foo.dfy that I want to verify against.
So if I want to verify things in old versions of Foo or even delete Foo because I'm done with it,
this test will continue to act as a memory and keep me honest.

[keyboardDrummer]

I don't understand the need for the feature you propose. Why don't you move the things you want to delete - but still tests against - to a folder called OLD, instead of deleting them?

If you can't move the old stuff because you've already edited/deleted it, then you can recover it using git.

[seebees]

I could move thing thing to an Old file, but then they still exist, someone could use them.
When things exist in a code base people are tempted to use them :).
Only if I delete them from the code base do they no longer exist.

[keyboardDrummer]

When things exist in a code base people are tempted to use them :).
Only if I delete them from the code base do they no longer exist.

So.. rename the method to DoNotUseThisIsOld_<PreviousName>, or put it in a module with a name along that line?

[seebees]

:) I know what you are saying.
That is a "Good Intention" and not a "Mechanism".
The juice may not be worth the squeeze for my idea.
But the point I'm trying to make is "Just moving files around" is harder than it seems. :)

[MikaelMayer]

I think it's great that you prove that the new code is correct with respect to the old code.

and maybe it could exist in the PR for a time,
eventually it needs to be removed.
It needs to be removed because the code that it is based on is getting removed.
Once it is removed, if any additional changes happen,
how do I know that everything is still equivalent?`

That's true: if your remove something, you loose the guarantee. That's the same with code, if you remove code, you'll lose the functionality of this code. If you want to be backwards compatible with code, you have to create code and use explicit versioning instead of deleting the previous one. For verification methods and predicates, it's the same.

So for example, if you anticipate you are going to evolve your types and predicates, you could keep all these even more precise predicates and types within versions in a sub-folder of your project, v1.ValidBar v2.ValidBar, and you keep the proofs of their "equivalence" or "implication" within another file, and in your code, you migrate v1.ValidBar to v2.ValidBar once you prove the equivalence. That way, you can keep your lemma around in case something goes wrong and you want to see where your specification was incorrect.

[seebees]

Sure, I can do this. Just like I can move my code to an OLD folder.

The point is we never "anticipate evolving our types" per se.
The reason we write the specification the way we did is because we thought it was correct.
It is only in the face of reality that we find we need to evolve or change something.

I can have lots of files with lots of comments that make clear that my intention is "B is new better and equivalent to A".
Or, if I could just pluck out the old version then all this is clear by just looking.

[MikaelMayer]

What you want is actually specifications for specifications. Does my specification implies this? Does my specification correctly requires that? If specifications are complex and intended to evolve, maybe you want some firm foundations that specifications do not deviate from.
That's why you write lemmas. Note that you could make your lemmas private to the module, so that no one can use them.

[seebees]

Making all these things private, e.g. do not export either the "work" or the "lemma" is a viable option.
But that would clutter the "production code".
However, creating a module that literally exports nothing,
that would hold the old methods, import the new methods and compare them with lemmas...

That is possible, very possible. thanks :)

[hirataqdees]

Hi @seebees , I agree that having different version of almost the same specs around might result in a clutter, but including files from a git history seems like relying on the out-of-sight files. I like the notion of making lemmas and older spec private as mentioned by Mikael.