NB: This Coq documentation contains a revised version of the Coq implementation of these papers [1], [2], [3], [4], and is also the support for ongoing research. A partial archive (14/01/2001) is available at here. Drop us a line if you are interested in a complete, up-to-date archive.

Library bbs_encode_decode

Require Import Epsilon.
Require Import ssreflect ssrbool eqtype.
Require Import Arith_ext ZArith_ext Lists_ext.
Require Import listbit machine_int multi_int.
Import MachineInt.
Require Import mips_seplog mips_frame mips_contrib mips_tactics mapstos.
Require Import sgoto compile.
Require Import encode_decode.
Require Import mont_mul_strict_prg bbs_prg.
Require Import bbs_triple bbs_termination.

Local Open Scope machine_int_scope.
Local Open Scope eqmod_scope.
Local Open Scope zarith_ext_scope.
Local Open Scope heap_scope.

Import expr_m.
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.

IMPLEMENTATION interface as used in BBS_Asm_CryptoProof.v.

The following signature summarizes what has to be proved of the implementation in Assembly of BBS. It is instantiated in the module Implem below.

Module Type IMPLEMENTATION.

Definition label := nat.

Parameter state : Type.

Definition lstate := (label * state)%type.

encode nn nk modu seed is the initial state built from the requested length nn in 32-bits words, the size nk in 32-bits words of the buffers used to store the seed and the modulus, the modulus modu, and the seed seed,

Parameter encode : nat -> nat -> Z -> Z -> state.

decode s is the pseudorandom list of booleans extracted from the final state s.

Parameter decode : state -> list bool.

Syntax of Assembly:

Parameter scode : Type.

The big-step operational semantics of [Saabas&Uustalu2007]:

Parameter exec_sgoto : scode -> option lstate -> option lstate -> Prop.

The assembly code for BBS:

Parameter bbs_asm : scode.

Restrictions imposed by the implementation of bbs_asm:

Definition Restrictions (nn nk : nat) (modu seed : Z) : Prop :=
  0 < modu /\ modu < 2 ^^ (nk * 32)%nat /\ Zodd modu /\
  0 <= seed /\ seed < modu /\
  4 * (Z_of_nat (4 * nk + nn + 2)%nat) < 2 ^^ 32.

Termination and determinism of bbs_asm:

Parameter exec_bbs_asm : forall nn nk modu seed, Restrictions nn nk modu seed ->
  { s_f : state |
    exec_sgoto bbs_asm (Some (O, encode nn nk seed modu)) (Some (240, s_f)) /\
    forall s', exec_sgoto bbs_asm (Some (O, encode nn nk seed modu)) s' ->
    s' = Some (240, s_f) }%nat.

bbs_fun is a generalization of BBS.bbs with relaxed types (see file file ZArith_ext.v). The assembly code bbs_asm implements bbs_fun:

Parameter bbs_semop : forall nn nk modu seed, Restrictions nn nk modu seed ->
  forall s_f,
    exec_sgoto bbs_asm (Some (O, encode nn nk seed modu)) (Some (240%nat, s_f)) ->
    decode s_f = bbs_fun (nn * 32) seed modu.

End IMPLEMENTATION.

encode/decode functions, lemmas for correctness and termination for BBS. To be used to instantiate the IMPLEMENTATION interface (see at the end of this file).

Module Import compile_m := Compile WMIPS_Hoare.
Import sgoto_hoare_m.
Import sgoto_m.
Import goto_deter_m.

Local Open Scope sgoto_scope.

Section bbs.

Restrictions imposed by the implementation of bbs_asm

Hypothesis nk : nat.

Hypothesis modu : Z.
Hypothesis Hmodu : 0 < modu.
Hypothesis Hmodu' : modu < 2 ^^ (nk * 32).
Hypothesis Hoddmodu : Zodd modu.

Hypothesis seed : Z.
Hypothesis Hseed : 0 <= seed.
Hypothesis Hseedmodu : seed < modu.

Hypothesis nn : nat.
Hypothesis Hcond : 4 * Z_of_nat (4 * nk + nn + 2) < Zbeta 1.

A series of technical lemmas just to help instantiating the Separation Logic triple of BBS.

Lemma inv_mod_prop : forall (m : int 32),
  Zodd (u2Z m) -> u2Z m * (inv_mod_beta (u2Z m)) =m -1 {{ Zbeta 1 }}.

Lemma inv_mod_prop' : forall (m : int 32),
  Zodd (u2Z m) -> 0 <= inv_mod_beta (u2Z m) < 2 ^^ 32.

Lemma Halpha : u2Z (nth 0 (Z2ints 32 nk modu) zero32) *
  u2Z (Z2u 32 (inv_mod_beta (u2Z (nth 0 (Z2ints 32 nk modu) zero32)))) =m -1 {{ Zbeta 1 }}.

Lemma HlenX0 : length (Z2ints 32 nk seed) = nk.

Lemma HlenB2K : length (Z2ints 32 nk ((Zbeta nk ^^ 2) mod (Sum nk (Z2ints 32 nk modu)))) = nk.

Lemma HlenM : length (Z2ints 32 nk modu) = nk.

Lemma HlenY : length (Z2ints 32 nk 0) = nk.

Lemma Hvl : u2Z (Z2u 32 (4 * Z_of_nat (2 * nk + 2))) = 4 * (Z_of_nat (2 * nk + 2)).

Lemma Hnl : u2Z (Z2u 32 (4 * Z_of_nat (2 * nk + 2))) + 4 * Z_of_nat nn < Zbeta 1.

Lemma Hnx : u2Z zero32 + 4 * Z_of_nat (S nk) < Zbeta 1.

Lemma HSumX0SumM : Sum nk (Z2ints 32 nk seed) < Sum nk (Z2ints 32 nk modu).

Lemma HSumB2KSumM :
  Sum nk (Z2ints 32 nk (Zbeta nk ^^ 2 mod (Sum nk (Z2ints 32 nk modu)))) < Sum nk (Z2ints 32 nk modu).

Lemma HSumB2K : Sum nk (Z2ints 32 nk (Zbeta nk ^^ 2 mod (Sum nk (Z2ints 32 nk modu)))) =m Zbeta nk ^^ 2 {{ Sum nk (Z2ints 32 nk modu) }}.

Lemma HoddM' : Zodd (Sum nk (Z2ints 32 nk modu)).

Require Import omegaz.

Lemma Hvy : u2Z (Z2u 32 (4 * Z_of_nat (2 * nk + nn + 2))) = 4 * (Z_of_nat (2 * nk + nn + 2)).

Lemma Hny : u2Z (Z2u 32 (4 * Z_of_nat (2 * nk + nn + 2))) + 4 * Z_of_nat (S nk) < Zbeta 1.

Let us be given 25 registers...

Variables i L_ l n j thirtytwo k alpha x y m one ext int_ X_ Y_ M_ quot C_ t s_ b2k B2K_ w' w : reg.

We instantiate the Separation Logic triple of BBS, this gives us a proof of functional correctness.

Definition bbs_triple_spec
  (Hset : nodup (i :: L_ :: l :: n :: j :: thirtytwo :: k :: alpha :: x :: y ::
    m :: one :: ext :: int_ :: X_ :: Y_ :: M_ :: quot :: C_ :: t :: s_ :: b2k ::
    B2K_ :: w' :: w :: r0 :: nil)) :=
  bbs_triple _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Hset nk
  (Z2u 32 (inv_mod_beta (u2Z (nth 0 (Z2ints 32 nk modu) zero32)))) (Z2ints 32 nk modu)
  Halpha nn (Z2ints 32 nn 0) (len_Z2ints nn 32 0) (Z2ints 32 nk seed) (Z2ints 32 nk 0)
  (Z2ints 32 nk ((Zbeta nk ^^ 2) mod (Sum nk (Z2ints 32 nk modu)))) HlenX0 HlenB2K
  HlenM HlenY _ _ (Z2u 32 (4 * Z_of_nat (S nk))) (Z2u 32 (4 * Z_of_nat (3 * nk + nn + 3))) _ Hny Hnx Hnl HSumX0SumM
  HSumB2KSumM HSumB2K HoddM'.

encode nn nk modu seed is the initial state built from the requested length nn in 32-bits words, the size nk in 32-bits words of the buffer used to store the seed and the modulus, the modulus modu, and the seed seed.

Definition encode (nn nk : nat) (seed modu : Z) : state :=
  let nx := O in
  let nm := S nk in
  let nl := (2 * nk + 2)%nat in
  let ny := (2 * nk + nn + 2)%nat in
  let nb2k := (3 * nk + nn + 3)%nat in
  (store.upd k (Z2u 32 (Z_of_nat nk))
  (store.upd n (Z2u 32 (Z_of_nat nn))
  (store.upd x (Z2u 32 (4 * Z_of_nat nx))
  (store.upd m (Z2u 32 (4 * Z_of_nat nm))
  (store.upd l (Z2u 32 (4 * Z_of_nat nl))
  (store.upd y (Z2u 32 (4 * Z_of_nat ny))
  (store.upd b2k (Z2u 32 (4 * Z_of_nat nb2k))
  (store.upd alpha (Z2u 32 (inv_mod_beta (u2Z (nth 0 (Z2ints 32 nk modu) zero32))))
  (store.upd thirtytwo (Z2u 32 32) (store.null_multiplier nil))))))))) ,
  list2heap nx (Z2ints 32 nk seed) +++ heap.sing (nx + nk) zero32 +++
  list2heap nm (Z2ints 32 nk modu) +++ heap.sing (nm + nk) zero32 +++
  list2heap nl (Z2ints 32 nn 0) +++
  list2heap ny (Z2ints 32 nk 0) +++ heap.sing (ny + nk) zero32 +++
  list2heap nb2k (Z2ints 32 nk (Zbeta nk ^^ 2 mod (Sum nk (Z2ints 32 nk modu)))))%nat.

decode s is the pseudorandom list of booleans extracted from the final state s.

Definition decode (st : state) : list bool :=
  let: (s, h) := st in
  let: nn := Zabs_nat (u2Z [n]_s) in
  list_flat (map (@bits 32) (heap2list (Zabs_nat (u2Z ([ l ]_s [.>>] 2))) nn h)).

Lemma decode_heap : forall s h L, (var_e l |--> L ** TT) s h ->
  u2Z ([ var_e l ]e_ s) + 4 * Z_of_nat (length L) < Zbeta 1 ->
  u2Z [ n ]_s = Z_of_nat (length L) ->
  decode (s, h) = list_flat (map (@bits 32) L).

We prove a specialized version of the Separation Logic triple of BBS with the encode/decode functions.

Ltac Zpower_tac :=
  match goal with
    | |- context [Zpower 2 32] => rewrite -Zbeta1_Zpower2
  end.

Ltac disj_seq_tac :=
  match goal with
    | |- Lists_ext.disj (List.seq ?a ?b) (?c :: nil) =>
      apply Lists_ext.disj_seq_singl; omegaz

    | |- Lists_ext.disj (List.seq ?a ?b) (?c :: nil) =>
      apply Lists_ext.disj_seq_singl2; omegaz

    | |- Lists_ext.disj (?c :: nil) (List.seq ?a ?b) =>
      apply Lists_ext.disj_sym; apply Lists_ext.disj_seq_singl; omegaz

    | |- Lists_ext.disj (?c :: nil) (List.seq ?a ?b) =>
      apply Lists_ext.disj_sym; apply Lists_ext.disj_seq_singl2; omegaz

    | |- Lists_ext.disj (List.seq ?a ?b) (List.seq ?c ?d) =>
      apply Lists_ext.disj_seq_seq; omegaz

    | |- Lists_ext.disj (?a :: nil) (?b :: nil) =>
      apply Lists_ext.disj_singl; omegaz
  end.

Lemma disj_not_In_for_tac : forall {A : Type} (n : A) l,
  disj (n :: nil) l -> ~ In n l.

Ltac disj_heap :=
  match goal with
    | |- heap.sing ?a _ # (list2heap ?b ?l) =>
      apply heap.disj_sym; disj_heap
    | |- (list2heap ?b ?l) # heap.sing ?a _ =>
      apply heap.disj_sing_R ;
      apply/seq_ext.inP ;
      rewrite ?dom_list2heap ?seq_ext.s2l2s ?len_Z2ints ?heap.dom_sing ?len_rep /=;
      apply disj_not_In_for_tac;
      by disj_seq_tac
    | |- list2heap ?a ?l # list2heap ?b ?k =>
      apply disj_list2heap ;
        rewrite ?dom_list2heap ?seq_ext.s2l2s ?len_Z2ints ?len_rep /=; by disj_seq_tac
    | |- heap.sing ?a _ # heap.sing ?b _ =>
      apply heap.disj_sing; omega
  end.

Lemma bbs_triple_encode_decode :
  nodup (i :: L_ :: l :: n :: j :: thirtytwo :: k :: alpha :: x :: y :: m ::
    one :: ext :: int_ :: X_ :: Y_ :: M_ :: quot :: C_ :: t :: s_ :: b2k :: B2K_ ::
    w' :: w :: r0 :: nil) ->
  {{ fun s h => encode nn nk seed modu = (s, h) }}
  bbs i L_ l n j thirtytwo k alpha x y m one ext int_ X_ Y_ M_ quot C_ t s_ b2k B2K_ w' w
  {{ fun s h => decode (s, h) = bbs_fun (nn * 32) seed modu }}.

Ltac repeat_disj_heap :=
  match goal with
    | |- _ # (_ +++ _) =>
      apply heap.disj_union_R; [by disj_heap | repeat_disj_heap]
    | |- _ # _ =>
      by disj_heap
  end.

Lemma bbs_termination' :
  nodup (i :: L_ :: l :: n :: j :: thirtytwo :: k :: alpha :: x :: y :: m ::
    one :: ext :: int_ :: X_ :: Y_ :: M_ :: quot :: C_ :: t :: s_ :: b2k ::
    B2K_ :: w' :: w :: r0 :: nil) ->
  { s_f : state |
    Some (encode nn nk seed modu) --
    bbs i L_ l n j thirtytwo k alpha x y m one ext int_ X_ Y_ M_ quot C_ t s_ b2k B2K_ w' w --->
    Some s_f }.

From the termination of BBS written with while-loops, we derive the termination of BBS written with jumps.

Lemma exec_bbs_asm :
  nodup (i :: L_ :: l :: n :: j :: thirtytwo :: k :: alpha :: x :: y :: m ::
    one :: ext :: int_ :: X_ :: Y_ :: M_ :: quot :: C_ :: t :: s_ :: b2k ::
    B2K_ :: w' :: w :: r0 :: nil) ->
  { s_f : state |
    Some (O, encode nn nk seed modu) >-
    compile_f O (bbs i L_ l n j thirtytwo k alpha x y m one ext int_ X_ Y_ M_
      quot C_ t s_ b2k B2K_ w' w) ---> Some (240%nat, s_f) }.

The assembly code bbs_asm implements bbs_fun.

Lemma bbs_semop : forall s_f,
  nodup (i :: L_ :: l :: n :: j :: thirtytwo :: k :: alpha :: x :: y :: m ::
    one :: ext :: int_ :: X_ :: Y_ :: M_ :: quot :: C_ :: t :: s_ :: b2k ::
    B2K_ :: w' :: w :: r0 :: nil) ->
  Some (O, encode nn nk seed modu) >-
  compile_f O (bbs i L_ l n j thirtytwo k alpha x y m one ext int_ X_ Y_ M_
    quot C_ t s_ b2k B2K_ w' w) ---> Some (240%nat, s_f) ->
  decode s_f = bbs_fun_rec (nn * 32) ((seed * seed) mod modu) modu.

End bbs.

Instantiation of the IMPLEMENTATION interface used in BBS_Asm_CryptoProof.v

Module Implem : IMPLEMENTATION.

Definition label : Set := compile_m.sgoto_hoare_m.sgoto_m.goto_deter_m.goto_m.label.

Definition state : Type := mips_cmd.state.

Definition lstate := (label * state)%type.

Definition l := reg_t0.
Definition n := reg_t1.
Definition thirtytwo := reg_t2.
Definition k := reg_t3.
Definition alpha := reg_t4.
Definition x := reg_t5.
Definition y := reg_t6.
Definition m := reg_t7.
Definition b2k := reg_t8.

Definition encode := encode l n thirtytwo k alpha x y m b2k.

Definition decode := decode l n.

Definition scode := compile_m.sgoto_hoare_m.sgoto_m.scode.

Definition exec_sgoto := compile_m.sgoto_hoare_m.sgoto_m.exec_sgoto.

Definition w := reg_t9.
Definition w' := reg_s0.
Definition B2K_ := reg_s1.
Definition s_ := reg_s2.
Definition t := reg_s3.
Definition C_ := reg_s4.
Definition quot := reg_s5.
Definition M_ := reg_s6.
Definition Y_ := reg_s7.
Definition X_ := reg_a0.
Definition int_ := reg_a1.
Definition ext := reg_a2.
Definition one := reg_a3.
Definition j := reg_v0.
Definition L_ := reg_v1.
Definition i := reg_at.

Definition bbs_asm :=
  compile_m.compile_f O (bbs i L_ l n j thirtytwo k alpha x y m one ext int_ X_ Y_ M_ quot C_ t s_ b2k B2K_ w' w).

Definition Restrictions (nn nk : nat) (modu seed : Z) : Prop :=
  0 < modu /\ modu < 2 ^^ (nk * 32) /\ Zodd modu /\
  0 <= seed /\ seed < modu /\
  4 * (Z_of_nat (4 * nk + nn + 2)) < 2 ^^ 32.

Lemma exec_bbs_asm :forall nn nk modu seed, Restrictions nn nk modu seed ->
  { s_f : state |
    exec_sgoto bbs_asm (Some (O, encode nn nk seed modu)) (Some (240, s_f)) /\
    forall s',
    exec_sgoto bbs_asm (Some (O, encode nn nk seed modu)) s' -> s' = Some (240, s_f)}%nat.

Lemma bbs_semop : forall nn nk modu seed, Restrictions nn nk modu seed ->
  forall s_f,
  exec_sgoto bbs_asm (Some (O, encode nn nk seed modu)) (Some (240%nat, s_f)) ->
  decode s_f = bbs_fun (nn * 32) seed modu.

End Implem.