Library compile_example

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq.
Require Import ZArith_ext.
Require Import machine_int.
Import MachineInt.

Require Import multi_int.
Require Import mips_seplog.
Require Import compile.

Local Open Scope multi_int_scope.

Module compile_m := Compile WMIPS_Hoare.

Require Import mont_mul_prg mont_mul_triple.

Definition k := reg_s6.
Definition alpha := reg_s7.
Definition x := reg_a0.
Definition y := reg_a1.
Definition z := reg_a2.
Definition m := reg_a3.

Definition one := reg_t0.
Definition ext := reg_t1.
Definition int_ := reg_t2.
Definition X_ := reg_t3.
Definition Y_ := reg_t4.
Definition M_ := reg_t5.
Definition Z_ := reg_t6.
Definition quot := reg_t7.
Definition C := reg_t8.

Definition t := reg_v0.
Definition s_ := reg_v1.

Lemma Hset : uniq (k :: alpha :: x :: y :: z :: m :: one :: ext :: int_ :: X_ ::
  Y_ :: M_ :: Z_ :: quot :: C :: t :: s_ :: r0 :: nil). Proof. done. Qed.

Section test.

Variable nk : nat.
Variables X Y M : seq (int 32).
Hypothesis Hx : length X = nk.
Hypothesis Hy : length Y = nk.
Hypothesis Hm : length M = nk.
Hypothesis HX : \S_{ nk } X < \S_{ nk } M.
Hypothesis HY : \S_{ nk } Y < \S_{ nk } M.
Variables vx vy vm vz : int 32.
Hypothesis Hnz : u2Z vz + 4 * Z_of_nat nk < Zbeta 1.
Variable valpha : int 32.

Local Open Scope eqmod_scope.
Local Open Scope machine_int_scope.

Hypothesis Halpha : u2Z (M `32_ 0) * u2Z valpha =m -1 {{ Zbeta 1 }}.

Application: Generation of Hoare-logic Proofs from While

in [Affeldt&Marti2006], we verified in Coq an implementation of the Montgomery multiplication written in the SmartMIPS instruction set. We worked on a version of the program where branches were replaced by while-loops and while-loops where compiled away by a certified macro-expander afterwards. Strictly speaking, there was therefore no Hoare-logic proof for the assembly code to be run.
The rest of this section shows that one can recover a Hoare-logic proof for the assembly code to be run by using the previously formalized theorem preservation_hoare .
montgomery is the program with while-loops. We instantiate it with a set of registers:

Definition mont_mul_cmd : while.cmd := montgomery k alpha x y z m one ext int_ X_ Y_ M_ Z_ quot C t s_.

Given a certain set of parameters (concrete initial values to put in registers and in the mutable memory), the proof of correctness mont_mul_triple gives a proof-term that is the proof that the Montgomery multiplication with while-loops is correct. In other words, this is a proof of correctness prior to compilation. This is clear when checked with the Check command.

Definition mont_mul_cmd_hoare :=
  mont_mul_triple _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Hset nk valpha vx vy vm vz X Y M Halpha Hx Hy Hm Hnz HX HY.

Local Open Scope mips_expr_scope.
Import assert_m.
Local Open Scope mips_assert_scope.
Local Open Scope mips_cmd_scope.
Local Open Scope mips_hoare_scope.

Check mont_mul_cmd_hoare.

Now, let us consider mont_mul_scode, the Montgomery multiplication with gotos, obtained by automatically macro-expanding if-then-else's and while-loops and locating the code at starting label 0 (using a function corresponding to the compile predicate ):

Definition mont_mul_scode : compile_m.sgoto_hoare_m.sgoto_m.scode := compile_m.compile_f O mont_mul_cmd.

Set Printing Depth 100.
Eval vm_compute in (compile_m.compile_f O mont_mul_cmd).

Lemma Hcompile : compile_m.compile O mont_mul_cmd mont_mul_scode 38%nat.
Proof.
have <- : (O + size (compile_m.sgoto_hoare_m.sgoto_m.sdom mont_mul_scode) = 38)%nat by vm_compute.
apply compile_m.compile_f_compile.
rewrite /mont_mul_scode.
reflexivity.
Qed.

By application of preservation_hoare and given the proof that the Montgomery multiplication with while-loops is correct, we obtain a proof-term that is the proof that the Montgomery multiplication with gotos is correct. Again, this can be checked with the Check command: the same triple as above is shown to hold, with the additional information that the starting label is 0, and the ending label is 38.

Definition mont_mul_sgoto_hoare :=
  compile_m.preservation_hoare _ _ _ mont_mul_cmd_hoare _ _ _ Hcompile.


End test.