# 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 }}.

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

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.

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.