Is it possible to prove that a given AST transformation is a perfect reversal of another?

Question

I want to use AST transformation using jscodeshift to do a large scale refactor, changing our test runner from Jest to Bun Test.

A concern that I'm trying to mitigate is that we might migrate the tests, it seems like it's working fine, but in three or six months time realise it's not working for us want to back out. Simply reverting the commit wouldn't do, by that time there are probably hundreds of new changes to the tests.

The strategy then, is to create two codemons, one to do the refactor, and another to reverse it, if need be.

As it is, the kind of transformation I'm doing is pretty simple, and I'm pretty confident that it's reversible/I can make do with comprehensive tests. But it does get me wondering, for a more complex transformation can we prove that a reverse transformation provides a perfect reversal?

Not all transformations are reversible, as a simple example:

If I were to transform

import alice from 'a'; 
import john from "b'; 

to

import alice from 'foo'; 
import john from 'foo'; 

Then we can't reverse 'foo' to 'a' or 'b' because we don't know which one it originally was (assuming that the alice and john variables are not sufficient hints at what the original import was).

Question is - is there technique or tooling that proves that two AST transforms provide perfect reversals of each other?