2.4.1 モジュール

EasyCryptリファレンスマニュアルの非公式な訳です。
いろいろガバガバなのは許してくれ

Easycryptのモジュールは、それぞれ異なる名前空間を持ち、型付きのグローバル変数と手続きからなる。以下のシンプルなモジュールMの定義は、多くのモジュール言語の例になっている。

require import Int Bool DInterval.

module M = {
  var x : int
  proc init (bnd : int) : unit = {
    x <$ [-bnd .. bnd];
  }

  proc incr(n: int) : unit = {
    x <- x + n;
  }

  proc get() : int = {
    return x;
  }

  proc main() : bool = {
    var n : int;
    init(100);
    incr(10); incr(-50);
    n <@ get();
    return n < 0;
  }
}.

Mは手続きinit, incr, get, mainに使われる1個のグローバル変数xをもつ。グローバル変数は手続きで使われる前に宣言されなければならない。
手続きinit("initialize")はint型のパラメータ(または引数)bnd("bound")をもつ。initはxに、絶対値がbnd以下の整数値を一様ランダムに選んで代入する確率的代入を使う。initの戻り値は、単一の要素ttをもつunitであり、ttはinitが終了するときに明示的に返される。
手続きincr("increment")は、xの値をそのパラメータnだけ増やす。手続きgetはパラメータは持たないが、return文を使って単にxを値を返す。return文は手続きの最後にのみ使ってよい。
そして手続きmainはパラメータはとらず、次の処理を行った結果のbooleanを返す。(省略)

EasyCryptは手続きの返り値の型、パラメータの型、そしてローカル変数のパラメータの型を推論しようとする。たとえば、上記の例は次のようにかける。

module M' = {
  var x : int

  proc init(bnd) = {
    x <$ [-bnd .. bnd];
  }

  proc incr(n) = {
    x <- x + n; 
  }
 
  proc get() = {
    return x;
  }

  proc main() = {
    var n;
    init(100);
    incr(10); incr(-50);
    n <@ get();
    return n < 0;
  }
}.

ここまで見てきたように、手続きの定義や文はセミコロンで終わる。たとえば次のように、複数のローカル変数の定義をまとめることもできる。

var x, y, z : int;
var u, v;
var x, y, z : int <- 10;
var x, y, z <- 10;

手続きのパラメータは変数であり、手続きが実行される間に変更されることがある。手続きのパラメータとローカル変数の名前は異なるものでなければならない。3つの代入文は、それぞれ許される右辺が違う。
・確率的代入(<$)の右辺は単一の部分分布でなければならない。適当な(proper)部分分布から選ばれたときは、確率的代入は失敗し、これを呼び出した手続き呼び出しは失敗することがある。
・ふつうの代入(<-)の右辺は任意の式でよいが、手続きの使用を含んではならない
・手続き呼び出し代入(<@)の右辺は単一の手続き呼び出しでなければならない

もしも代入の右辺がタプルを出力するなら、左辺では以下のようにパターンマッチングを使える。

(x, y, z) <- ...;

この場合は...では三つ組を出力している。

残る2つの文、条件分岐とwhileループは次のように書ける。

require import Bool Int DInterval.

module N = {
  proc loop() : int = {
    var y, z : int;
    y <- 0;
    while (y < 10) {
      z <$ [1 .. 10];
      if (z <= 5) {
        y <- y - z;
      }
      else {
        y <- y + (z - 5);
      }
    }
    return y;
  }
}.

次のように、モジュールはすでに定義されているモジュールのグローバル変数と手続きにアクセスできる。

module M'' = {
  var x : int

  proc f() : unit = {
    x <- x + 1;
  }
}.


module N' = {
  var x : int
  
  proc g(n m : int, b: bool) : bool = {
    if (b) M''.f();
    M''.x <- M''.x + x + n - m;
    return 0 < M''.x;
  }
  proc h = M''.f
}.

Nの手続きgは、モジュールMのグローバル変数xと、M''の手続きfにアクセスしている。gのパラメータリストは次のように書くのと等価である。

n : int, m: int, b: bool

モジュールは自分自身のグローバル変数を、自分自身の名前を使って参照できる。つまり、手続きM''.fの定義ではこのように書ける。

proc f() : unit = {
  M''.x <- M''.x + 1;
}

Nの手続きhは、手続きM''.fのエイリアスである。これを呼び出すのは直接M''.fを呼び出すのと等価である。あるモジュールのエイリアスとしてモジュール名を宣言したいのなら、次のようにできる。

module L = N.

手続き呼び出しは、すべての宣言されたモジュールのすべてのグローバル変数の値を記録しているメモリのコンテキストの上で実行される。したがってすべてのグローバル変数は(定義によって)初期化される。一方で手続きのローカル変数は、最初はそれらの型の任意の値をとる。これは我々が全く関知しないEasyCryptのプログラム論理によってモデル化されている。たとえば、次のX.f()の確率がtrueを返すことは未定義である。しかし我々はこれについて何も証明できない。

module X = {
  proc f() : bool = {
    var b : bool;
    return b;
  }
}.

一方で、常に0を返す次のY.fのように、単にローカル変数が使われる前に初期化されていないからといって、使った結果が決定できないわけではない。

module Y = {
  proc f() : int = {
    var x : int;
    return x - x;
  }
}.