val lo (a: _) : erel a
val lo (a: _) : erel a
let lo a : erel a = fun x y -> (x == y <: prop)
(*
   Copyright 2008-2019 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.

   Authors: K. Kohbrok, M. Kohlweiss, T. Ramananandro, N. Swamy
*)

module Setoids

/// Markulf and Konrad do proofs of cryptographic security by
/// reasoning about equivalences of cryptographic functionalities
/// expressed as functors.
///
/// Konrad's slides from a talk at Bertinoro provide a good overview
/// https://github.com/kkohbrok/kkohbrok.github.io/raw/master/talks/skech2018.pdf
///
/// For instance, they write things like:
///              PKAE⁰
///    =         MOD-PKAE⁰ . (ODH⁰ | AE⁰) . KEY
///    ~εₒ + εₐ  MOD-PKAE¹ . (ODH¹ | AE¹) . KEY
///    =         PKAE¹
///
/// to express the security of a authenticated encryption construction.
///
/// Elements like ODH⁰ are functors (parameterized modules) expressing
/// cryptographic hypotheses
///      `.` is functor composition
///      `|` is functor product
///
/// The equivalences are all contextual, i.e., an attacker functor
/// when interacting cannot tell two sides of an equivalence apart,
/// except with a probability ε

/// In trying to formalize what this style of proof might mean in F*,
/// we develop here a small theory of equivalences for simply typed,
/// but pure, higher order, monadic F* code packaged into an encoding
/// of modules and functors within F*'s term language.
///
/// This is still work in progress: we have yet to validate whether
/// this style of proof might work at a scale needed for interesting
/// crypto proofs. But, it's already quite a bit of fun, I think.

/// It turns out that the techniques we use are related to setoids and
/// partial equivalence relations. To learn more about those, you
/// might want to read:
///
///   Setoids in type theory:
///       http://www.cs.nott.ac.uk/~pszvc/publications/Setoids_JFP_2003.pdf
///   PER model of secure information flow
///       https://www.cse.chalmers.se/~andrei/esop99.pdf

(** First, some basics **)

/// `rel'` : The type of relations
let rel (s:Type) = s -> s -> Type0

/// `type_of` :
///
/// A convenience to compute that type of elements of a relation
unfold
let type_of #a (r:rel a) = a

/// Reflexivity
let refl #s (r: rel s) =
  forall x. x `r` x

/// Symmetry
let sym #s (r: rel s) =
  forall x y. x `r` y <==> y `r` x

/// Transitivity
let trans #s (r: rel s) =
  forall x y z. x `r` y /\ y `r` z ==> x `r` z

/// A partial equivalence relation (PER) is not necessarily reflexive,
/// but is symmetric and transitive
let is_per #a (r:rel a) =
  sym r /\
  trans r

/// `per a`: a partial equivalence relation on `a`
let per (a:Type) = r:rel a{ is_per r }

/// `equiv r`: `r` is an equivalence relation
///   i.e., a reflexive PER
let equiv (#s:Type) (r: rel s) =
  refl r /\
  is_per r

/// `rel` : The type of equivalence relations
let erel (s:Type) = r:rel s { equiv r }

/// `erel_of_per`: Any PER can be seen as an an equivalence relation
///  on the diagonal of its domain
let erel_of_per (#a:Type) (r:per a)
  : erel (x:a{x `r` x})
  = r

/// In fact, every pair of elements in the PER is also on its diagonal
///   (through symmetry and transitivity)
let per_diagonal #a (r:per a) (x y : a)
  : Lemma
    (requires x `r` y)
    (ensures
      x `r` x /\
      y `r` y)
  = ()


/// `perₜ` : A partial setoid.
///
///    Note, rather than using `perₜ` below, we use instead its
///    curried form, which turns out to be more convenient for type
///    inference
let per_t = (t:Type & per t)

/// `( ** )`: product relation
///  Building a relation on pairs from
///  relations on its components
let ( ** ) (#a:Type) (#b:Type) (arel:rel a) (brel:rel b) (p0 p1:(a & b)) : prop =
  let (x0, y0) = p0 in
  let (x1, y1) = p1 in
  x0 `arel` x1 /\
  y0 `brel` y1

/// ` arrow_rel' `:
///  A relation on arrows, from relations on domain and co-domain
let arrow_rel (#a:Type) (#b:Type) (arel:rel a) (brel:rel b) (f g : (a -> b)) : prop =
    forall x0 x1. x0 `arel` x1 ==>
             f x0 `brel` g x1

/// `arrow_rel` is a PER when its arguments are PERs
///
///  Note, `arrow_rel` is not an equivalence relation on `a -> b`
///  since it need not be reflexive.
let arrow #a #b (ra:per a) (rb:per b) : per (a -> b) = arrow_rel ra rb

/// ` ^--> `: the type of functions that take related arguments to related results
let ( ^--> ) (#a:Type) (#b:Type) (arel:rel a) (brel:rel b) =
  f:(a -> b){ f `arrow_rel arel brel` f}

/// `e_arrow_rel`: But it is an equivalence relation on reflexive
/// elements of `arrow_rel`
let e_arrow_rel #a #b (ra:per a) (rb:per b) : erel (ra ^--> rb) = arrow_rel ra rb

/// Now for some simple examples

/// `id` is relationally parametric:
let id (arel:rel 'a) : (arel ^--> arel) = fun x -> x

/// `lo`: The "low security relation", i.e., adversary visible values
/
prims.fst.checked FStar.Squash.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.DependentMap.fsti.checked
Setoids.fst
a: Type -> Setoids.erel a
Prims.eq2 Prims.prop Setoids.erel
let lo a : erel a =
  
fun x y -> (x == y <: prop)