Translation from Stainless to Coq

Initially based on a project done by Bence Czipó, this translation is an early experimental stage.

The –coq option of Stainless replaces the standard verification checker (which uses Inox) by a translation to Coq. Each function from the *.scala file is translated to a Coq file, and obligations corresponding to assertions, preconditions, and postconditions are solved using predefined tactics in Coq.

Requirements

• Coq 8.11.2

• Coq Equations 1.2.2+8.11

These can be installed using opam as explained in the Equations README.md.

Usage of the Coq option

First, clone the Stainless repository. In the slc-lib directory, run ./configure and make.

Then, assuming the Stainless binary stainless-scalac is in your path, run: stainless-scalac --coq File.scala on the file of your choice. As an example, consider the test function from the Arith.scala file:

def test(a: BigInt, b: BigInt, c: BigInt): BigInt = {
  require(a > b && c > BigInt(0))
  c + a
} ensuring( _ > c + b )

Running stainless-scalac --coq frontends/benchmarks/coq/Arith.scala generates the file tmp/test.v which contains the following Coq definition.

Definition test (a: Z) (b: Z) (c: Z) (contractHyp4: (ifthenelse (Z.gtb a b) bool
        (fun _ => Z.gtb c (0)%Z )
        (fun _ => false ) = true)) : {x___1: Z | (Z.gtb x___1 (Z.add c b) = true)} :=
Z.add c a.

Fail Next Obligation.

The coqc executable in run on the file, and the status is reported by Stainless. In the translation to Coq, the BigInt type is encoded as Z. The precondition (require) is encoded as an extra argument contractHyp4, and the postcondition is encoded as a refinement on the return type of test. Here, the obligation related to the postcondition is solved automatically thanks to the obligation tactic defined above in the tmp/test.v file. The statement Fail Next Obligation. then succeeds because all obligations have been solved (any command in Coq can be prefixed with Fail, and the resulting command succeeds when the original command fails).