`copilot-theorem`: README mentions inexisting `Driver.hs`, `lightProver`

[ivanperez-keera]

Description

copilot-theorem's README mentions a file Driver.hs that is not part of the library:

As an example, the following prover is used in Driver.hs:

and later

Some examples are in the examples folder. The Driver.hs contains the main function to run any example. 

It also says that there are two provers: one based on Kind2, and one called lightProver. The latter no longer exists, but we do have a What4 module now.

These mentions should be adjusted or removed.

Type

• Bug: incorrect documentation.

Additional context

None.

Requester

• Max Fan (NASA)

Method to check presence of bug

Running a search through the tree brings up several mentions:

$ grep -nIHre 'Driver.hs'
copilot-theorem/README.md:205:As an example, the following prover is used in `Driver.hs`:
copilot-theorem/README.md:254:Some examples are in the *examples* folder. The `Driver.hs` contains the `main`
copilot-theorem/README.md:257:by changing one *import* directive in `Driver.hs`.

$ grep -nIHre 'lightProver'
copilot-theorem/README.md:79:prove (lightProver def) (check "gt0") spec
copilot-theorem/README.md:82:where `lightProver def` stands for the *light prover* with default
copilot-theorem/README.md:150:`lightProver :: Options -> Prover` function which builds a prover from a record
copilot-theorem/README.md:209:  lightProver def {onlyBmc = True, kTimeout = 5}

$ grep -nIHre '\<Light\>' | grep -ve 'XML'
copilot-theorem/README.md:71:  the `Copilot.Theorem.Light` and `Copilot.Theorem.Kind2` module.
copilot-theorem/README.md:123:Two provers are provided by default: `Light` and `Kind2`.
copilot-theorem/README.md:149:The *light prover* is defined in `Copilot.Theorem.Light`. This module exports the
copilot-theorem/README.md:399:#### The Light prover
copilot-theorem/README.md:402:basic *k-induction* algorithm [1]. The `Light` directory contains three files:

Expected result

The output of the above grep commands should be empty, indicating that that inexisting file/modules/functions are not mentioned.

Desired result

The output of the above grep commands should be empty, indicating that that inexisting file/modules/functions are not mentioned.

Proposed solution

The claims should be adjusted to match the existing file tree, modules and exports, either by updating the references to point to their current locations, or by removing the claims altogether.

Further notes

None.

[ivanperez-keera]

Change Manager: Confirmed that the README is outdated and mentions in-existing functions, modules and files.

[ivanperez-keera]

Technical Lead: Confirmed that the issue should be addressed.

[RyanGlScott]

I investigated these parts of copilot-theorem recently as well. I believe what the README refers to as lightProver has been superseded by the new kInduction prover, which is separate from the Kind2 and What4 provers. See also 976bc5f, which removes lightProver in favor of kInduction.

[fdedden]

I have picked up fixing the README.

@RyanGlScott yes, it seems that lightProver has been superseded by kInduction (and the code has been refactored a bit since then). copilot-theorem is pretty much the only part of Copilot where I have nearly no knowledge about. What is the difference between kInduction:

copilot/copilot-theorem/src/Copilot/Theorem/Prover/SMT.hs

Lines 110 to 116 in f823901

	kInduction :: SmtFormat a => Options -> Backend a -> Proof Universal
	kInduction opts backend = check P.Prover
	{ P.proverName = "K-Induction"
	, P.startProver = return . ProofState opts backend Map.empty . translateWithBounds
	, P.askProver = kInduction' (startK opts) (maxK opts)
	, P.closeProver = const $ return ()
	}

and kind2Prover:

copilot/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs

Lines 44 to 49 in f823901

	kind2Prover :: Options -> Prover
	kind2Prover opts = Prover
	{ proverName = "Kind2"
	, startProver = return . ProverST opts . TS.translate
	, askProver = askKind2
	, closeProver = const $ return () }

Sounds like they solve the same problem with a different backend?

The README is rather outdated and incomplete, so maybe we just want to remove all parts mentioning lightProver and do a complete rewrite later on?

[RyanGlScott]

Sounds like they solve the same problem with a different backend?

Yes, that is my understanding as well.

[fdedden]

Yeah, I think we may want to revisit and clean the library. @ivanperez-keera I propose we simply remove any obsolete information from the README, so that it is at least not plain incorrect about things. Later on we can investigate if kInduction and kind2Prover are actually equal, and deprecate one of them (in the end both are based on Yices). After this (and possibly other cleanup work) we can rewrite the README. What do you think?