lib.option.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 *)

def OptionType_1(option, option_Some, option_None, input) {
  type option.
  fun option_Some(input): option [data].
  const option_None: option.
  equation forall x: input;
    option_Some(x) <> option_None.
}

def OptionType_2(option, option_Some, option_None, input1, input2) {
  type option.
  fun option_Some(input1, input2): option [data].
  const option_None: option.
  equation forall x1: input1, x2: input2;
    option_Some(x1, x2) <> option_None.
}