TLAPS proves ~(x = TRUE) <=> (x = FALSE) in released versions

[lemmy]

#135 surfaced that TLAPS accepts the following bogus theorem:

---- MODULE Oops ----

VARIABLE x

LEMMA 
    ~(x = TRUE) <=> (x = FALSE)
OBVIOUS

====

This bug is not present in HEAD@main:

@lemmy ➜ /workspaces/tlapm (main) $ tlapm --version
8facb9a-dirty
@lemmy ➜ /workspaces/tlapm (main) $ tlapm Oops.tla 
Zenon error: exhausted search space without finding a proof
(* created new ".tlacache/Oops.tlaps/Oops.thy" *)
(* fingerprints written in ".tlacache/Oops.tlaps/fingerprints" *)
File "./Oops.tla", line 7, characters 1-7:
[ERROR]: Could not prove or check:
           ASSUME NEW VARIABLE x
           PROVE  ~x = TRUE <=> x = FALSE
File "./Oops.tla", line 1, character 1 to line 9, character 4:
[ERROR]: 1/1 obligation failed.
There were backend errors processing module `"Oops"`.
 tlapm ending abnormally with (Failure "backend errors: there are unproved obligations")
Raised at file "stdlib.ml", line 29, characters 17-33
Called from file "src/tlapm_lib.ml", line 435, characters 12-77
Called from file "src/tlapm_lib.ml", line 543, characters 23-43
Called from file "list.ml", line 121, characters 24-34
Called from file "src/tlapm_lib.ml", line 546, characters 13-40
Called from file "src/tlapm_lib.ml", line 558, characters 8-33

This bugs is present in the last three releases (I did not check < v1.4.5):

• https://github.com/tlaplus/tlapm/releases/tag/202210041448 a963bd3
• https://github.com/tlaplus/tlapm/releases/tag/202208050903 ee56b3d
• https://github.com/tlaplus/tlapm/releases/tag/v1.4.5 9f51444

@lemmy ➜ /workspaces/tlapm (main) $ md5sum tlaps-1.5.0-x86_64-linux-gnu-inst.bin 
01a5fd8d1738d4443802babc6b34b282  tlaps-1.5.0-x86_64-linux-gnu-inst.bin
@lemmy ➜ /workspaces/tlapm (main) $ chmod +x tlaps-1.5.0-x86_64-linux-gnu-inst.bin 
@lemmy ➜ /workspaces/tlapm (main) $ sudo ./tlaps-1.5.0-x86_64-linux-gnu-inst.bin 
Installing the TLA+ Proof System

    Version: 1.5.0
Destination: /usr/local

Extracting ... done.
Compiling Isabelle theories.
Building Pure ...
Finished Pure (0:00:07 elapsed time, 0:00:06 cpu time, factor 0.85)
Building TLA+ ...
Finished TLA+ (0:00:10 elapsed time, 0:00:19 cpu time, factor 1.90)
Finished compiling Isabelle theories.
Performing a self-test ... done.

All done.

REMEMBER to add /usr/local/bin to your $PATH
You will also need to add
   /usr/local/lib/tlaps
to the toolbox's library path (File->Preferences->TLA+ Preferences->Add Directory)

@lemmy ➜ /workspaces/tlapm (main) $ tlapm --version
1.5.0
@lemmy ➜ /workspaces/tlapm (main) $ tlapm Oops.tla 
** Unexpanded symbols: ---

(* created new ".tlacache/Oops.tlaps/Oops.thy" *)
(* fingerprints written in ".tlacache/Oops.tlaps/fingerprints" *)
File "./Oops.tla", line 1, character 1 to line 9, character 4:
[INFO]: All 1 obligation proved.

@lemmy ➜ /workspaces/tlapm (main) $ md5sum tlaps-1.5.0-x86_64-linux-gnu-inst.bin 
b52ab3eb7242ebec957df97475f41c83  tlaps-1.5.0-x86_64-linux-gnu-inst.bin
@lemmy ➜ /workspaces/tlapm (main) $ chmod +x tlaps-1.5.0-x86_64-linux-gnu-inst.bin 
@lemmy ➜ /workspaces/tlapm (main) $ sudo ./tlaps-1.5.0-x86_64-linux-gnu-inst.bin 
Installing the TLA+ Proof System

    Version: 1.5.0
Destination: /usr/local

Extracting ... done.
Compiling Isabelle theories.
Building Pure ...
Finished Pure (0:00:07 elapsed time, 0:00:06 cpu time, factor 0.85)
Building TLA+ ...
Finished TLA+ (0:00:11 elapsed time, 0:00:20 cpu time, factor 1.81)
Finished compiling Isabelle theories.
Performing a self-test ... done.

All done.

REMEMBER to add /usr/local/bin to your $PATH
You will also need to add
   /usr/local/lib/tlaps
to the toolbox's library path (File->Preferences->TLA+ Preferences->Add Directory)
@lemmy ➜ /workspaces/tlapm (main) $ tlapm --version
1.5.0
@lemmy ➜ /workspaces/tlapm (main) $ tlapm Oops.tla 
(* loading fingerprints in ".tlacache/Oops.tlaps/fingerprints" *)
(* created new ".tlacache/Oops.tlaps/Oops.thy" *)
(* fingerprints written in ".tlacache/Oops.tlaps/fingerprints" *)
File "./Oops.tla", line 1, character 1 to line 9, character 4:
[INFO]: All 1 obligation proved.

@lemmy ➜ /workspaces/tlapm (main) $ sudo ./tlaps-1.4.5-x86_64-linux-gnu-inst.bin 
Installing the TLA+ Proof System

    Version: 1.4.5
Destination: /usr/local

Extracting ... done.
Compiling Isabelle theories.
Building Pure ...
Finished Pure (0:00:07 elapsed time, 0:00:06 cpu time, factor 0.85)
Building TLA+ ...
Finished TLA+ (0:00:11 elapsed time, 0:00:19 cpu time, factor 1.72)
Finished compiling Isabelle theories.
Performing a self-test ... done.

All done.

REMEMBER to add /usr/local/bin to your $PATH
You will also need to add
   /usr/local/lib/tlaps
to the toolbox's library path (File->Preferences->TLA+ Preferences->Add Directory)

@lemmy ➜ /workspaces/tlapm (main) $ tlapm --version
1.4.5 (build 33809)
@lemmy ➜ /workspaces/tlapm (main) $ tlapm Oops.tla 
** Unexpanded symbols: ---

(* created new "Oops.tlaps/Oops.thy" *)
(* fingerprints written in "Oops.tlaps/fingerprints" *)

[lemmy]

Bisecting between a963bd3 and 8facb9a (HEAD) identifies 3f08478 as the fix. This commit is the tip of @adef-inr new SMT encoding, confirming Stephan's hypothesis in #135. I confirmed that the predecessor commit 581ebd8 of the commits introducing the new SMT backend has the bug.

PS: Remember to run tlapm with --nofp when bisecting. 😠

[lemmy]

IMO this is a severe bug that warrants a new release.

[muenchnerkindl]

Agreed.