Single-party semantics
========================

The single-pary semantics class is parameterised by a language ``L`` and
should establish how programs written in that language are animated as
if they were being executed in a idealised way by a TTP.

Our single-party semantics formalisation is based on adversarial code,
influenced by the UC model. Program evaluation is managed
by an *environment*, that can provide inputs to the program
being interpreted and also collect outputs at any time.
Furthermore, the environment can request the evaluation of
the program in a small-step basis. This evaluation is carried
out by an *adversary*, that, at a high-level, models the
inside behaviour of the *environment* inside the program
execution.

The *adversary* has the possibility of requesting the execution of one
program statement at a time. The semantics also contemplates the
possibility of some side information ``sideInfo_t`` being leaked by the execution of
language instructions.

Our EasyCrypt single-party semantics formalisation is based on the
EasyCrypt's module system, that allows the definition of *signature
types* for procedures by using *module type* EasyCrypt structure.

Semantics interface
-------------------------

The semantics interface discloses 6 procedures:

* ``init(P)`` - initialises the evaluation with initial program P
* ``step`` - sequential semantics procedures, that executes one instruction of the program.
* ``stepInput(x)`` - processes the input ``x`` provided by the environment
* ``getOutput`` - releases output to the environment

::

  module type Semantics = {
    proc init(P : L) : unit
    proc step() : sideInfo_t option
    proc setInput(x : secret_t) : bool
    proc getOutput() : secret_t option
  }.

Environment interface
-------------------------

The environment semantics interface specifies how the environment
interacts with the program evaluation. It discloses 3 procedures:

* ``stepInput(x)`` - provides input ``x`` to the program semantics
* ``getOutput`` - collects output from the program
* ``activate`` - activates the adversary so that it can procede with the actual program evaluation.

::

  module type EnvSemInterface = {
    proc setInput(x: secret_t): bool
    proc getOutput(): secret_t option
    proc activate(): sideInfo_t option
  }.

The environment has oracle access to the environment semantics
interface in order to animate some program via the ``animate``
procedure. To represent the output of some program animation, we
enrich the formalisation with a special ``output_event_t`` type.

::

  module type Environment (ESI: EnvSemInterface) = {
    proc animate(): output_event_t 
  }.

Adversary interface
-------------------------

The adversary semantics interface specifies how the adversary
interacts with the program evaluation. It discloses 1 procedures: 
- ``step()`` - evaluates an instruction of the program

::

  module type AdvSemInterface = {
    proc step(): sideInfo_t option
  }.

The adversary has oracles access to the adversary semantics interface
in order to execute one instruction of a program via the ``step``
procedure.

::

  module type Adversary (ASI : AdvSemInterface) = {
    proc step() : sideInfo_t option
  }.

General evaluation strategy
----------------------------------

Armed with the structures previously defined, we can now construct a
general evaluation strategy that executes any given program and that
ends with the output event that is verified by the *environment*.

We start by specifying a concrete implementation of the *environment*
semantics oracle that is parameterised by the concrete semantics of
the program and by an adversary. This new module
``EnvironmentSemanticsInterface`` essentially defines all possible
*environment* operations based on the concrete semantics of the
program and based on the evaluation strategies disclosed by the
adversary.

::

  module EnvironmentSemanticsInterface (Sem : Semantics) (A : Adversary) = {
    proc init = Sem.init
    proc setInput(x: secret_t): bool = {
      var r;
      r <@ Sem.setInput(x);
      return r;
    }
    proc getOutput(): secret_t option = {
      var r;
      r <@ Sem.getOutput();
      return r;
    }
    proc activate(): sideInfo_t option = {
      var r;
      r <@ A(Sem).step();
      return r;
    }
  }.

Finally, a program can be computed according to the generic procedure
displayed bellow. It takes as input a program written in any language
``L``, initialises the semantics module with the concrete program and
then proceeds with the concrete program execution. It adopts as output
the same output given to by the *environment*.

::

  module Eval(Sem : Semantics, Z : Environment, A : Adversary) = {
    proc eval(P : L) = {
      var b;
      EnvironmentSemanticsInterface(Sem,A).init(P);
      b <@ Z(EnvironmentSemanticsInterface(Sem,A)).animate();
      return (b);
    }
  }.