lib.truncate.ocvl

(* Analysing the HPKE Standard - Supplementary Material
   Joël Alwen; Bruno Blanchet; Eduard Hauck; Eike Kiltz; Benjamin Lipp; 
   Doreen Riepel

This is supplementary material accompanying the paper:

Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
Long version: https://eprint.iacr.org/2020/1499 *)

(* The types input_t and output_t MUST be fixed. *)
def truncate(input_t, output_t, truncate_f) {

  param N.

  fun truncate_f(input_t): output_t.

  (* If we truncate a uniformly distributed random value, 
     we obtain a uniformly distributed random value *)
  equiv(truncate(truncate_f))
    foreach i<=N do h <-R input_t;
      O_trunc() := return(truncate_f(h))
    <=(0)=>
    foreach i<=N do k <-R output_t;
      O_trunc() := return(k).
}