%% v3.1 [2018/04/18]
%\documentclass[Proof,technicalreport]{ieicej}
\documentclass[technicalreport]{ieicej}

\usepackage[dvipdfmx]{graphicx}
\usepackage{graphicx}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage{textcomp}
\usepackage{latexsym}
%\usepackage[fleqn]{amsmath}
%\usepackage{amssymb}
\usepackage{url}

\usepackage{listings}
\lstset{
  frame=single,
  keepspaces=true,
  stringstyle={\ttfamily},
  commentstyle={\ttfamily},
  identifierstyle={\ttfamily},
  keywordstyle={\ttfamily},
  basicstyle={\ttfamily},
  breaklines=true,
  xleftmargin=0zw,
  xrightmargin=0zw,
  framerule=.2pt,
  columns=[l]{fullflexible},
  numbers=left,
  stepnumber=1,
  numberstyle={\scriptsize},
  numbersep=1em,
  language={},
  tabsize=4,
  lineskip=-0.5zw,
    inputencoding=utf8,
    extendedchars=true,
    escapechar={@}
}
\renewcommand{\lstlistingname}{Code}
\usepackage{caption}
\captionsetup[lstlisting]{font={small,tt}}

\def\IEICEJcls{\texttt{ieicej.cls}}
\def\IEICEJver{3.1}
\newcommand{\AmSLaTeX}{%
 $\mathcal A$\lower.4ex\hbox{$\!\mathcal M\!$}$\mathcal S$-\LaTeX}
%\newcommand{\PS}{{\scshape Post\-Script}}
\def\BibTeX{{\rmfamily B\kern-.05em{\scshape i\kern-.025em b}\kern-.08em
 T\kern-.1667em\lower.7ex\hbox{E}\kern-.125em X}}

\jtitle{GearsOSのHoare Logicをベースにした検証手法}
%% \jsubtitle{技術研究報告原稿のための解説とテンプレート}
%% \etitle{How to Use \LaTeXe\ Class File (\IEICEJcls\ version \IEICEJver) 
%%         for the Technical Report of the Institute of Electronics, Information 
%%         and Communication Engineers}
%% \esubtitle{Guide to the Technical Report and Template}
\authorlist{
 \authorentry[masataka@cr.ie.u-ryukyu.ac.jp]{外間 政尊}{Masataka Hokama}{1}% 
 \authorentry[kono@cr.ie.u-ryukyu.ac.jp]{河野 真治}{Shinji Kono}{2}% 
}
\affiliate[1]{琉球大学大学院理工学研究科情報工学専攻}
  {Interdisciplinary Information Engineering, Graduate School of Engineering and Science, University of the Ryukyus.}
\affiliate[2]{琉球大学工学部情報工学科}
  {Information Engineering, University of the Ryukyus.}
%\MailAddress{$\dagger$hanako@denshi.ac.jp,
% $\dagger\dagger$\{taro,jiro\}@jouhou.co.jp}
\begin{document}
\begin{jabstract}
  あらまし
\end{jabstract}
\begin{jkeyword}
  プログラミング言語,
  CbC, Gears OS, Agda
  %% あと他…？
\end{jkeyword}
%% \begin{eabstract}
%%   %% メールを見た感じ日本語のみとなっていたので不必要…？
%% \end{eabstract}
%% \begin{ekeyword}
%%   %% 不必要？
%% \end{ekeyword}
\maketitle
\section{まえがき}
% とりあえずabstをそのまま
Gears OS は継続を主とするプログラミング言語 CbC で記
述されている。
OS やアプリケーションの信頼性を上げるには仕様を満
たしていることを確認する必要がある。
現在 GearsOS の仕様の確認には定理証明系である Agda を
用いている。
CbC では関数呼び出しを用いず goto 文により遷移する
。
これは Agda 上では継続渡しの記述を用いた関数として
記述する。
また、継続にはある関数を実行するための事前条件や
事後条件などをもたせることが可能である。
Floyd–Hoare logic (以下 Hoare Logic) は事前条件が成り立っているときにある
関数を実行して、それが停止する際に事後条件を満た
すことを確認することで、検証を行うアイディアである。
これは継続を用いた Agda 上では事前条件とその証明をを継続で関数
に渡し、関数からさらに継続した先で事後条件とその証明が成り
立つという形で記述できる。
本研究では GearsOS の仕様確認に Hoare Logic をベースと
した証明を導入し、今まで行っていた証明との比較を
行う。

\section{GearsOS}
Gears OS は信頼性をノーマルレベルの計算に対して保証し、拡張性をメタレベルの計算で実現することを目標に開発している OSである。

Gears OS は処理の単位を Code Gear、データの単位を Data Gear と呼ばれる単位でプログラムを構成する。
信頼性や拡張性はメタ計算として、通常の計算とは区別して記述する。


\section{CodeGearとDataGear}

Gears OS ではプログラムとデータの単位として CodeGear、 DataGear を用いる。 Gear
 は並列実行の単位、データ分割、 Gear 間の接続等になる。
CodeGear はプログラムの処理そのもので、図\ref{fig:cgdg}で示しているように任意の数の
Input DataGear を参照し、処理が完了すると任意の数の Output DataGear に書き込む。

CodeGear 間の移動は継続を用いて行われる。継続は関数呼び出しとは異なり、呼び出し
た後に元のコードに戻らず、次の CodeGear へ継続を行う。これは、関数型プログラミングでは末尾関数呼び出しを行うことに相当する。

Gear では処理やデータ構造が CodeGear、 DataGear に閉じている。したがって、
DataGear は Agda のデータ構造(data と record)で表現できる。
CodeGear は Agda の CPS (Continuation Passing Style) で関数として表現することができる。

\begin{figure}[htpb]
 \begin{center}
   \scalebox{0.3}{\includegraphics{pic/codeGear_dataGear.pdf}}
 \end{center}
 \caption{CodeGear と DataGear の関係}
 \label{fig:cgdg}
\end{figure}

また Gears OS 自体もこの Code Gear、Data Gear を用いた CbC(Continuation based C) で実装される。
そのため、Gears OS の実装は Code Gear、Data Gear を用いたプログラミングスタイルの指標となる。

\section{Agda}


\section{CbC と Agda}
%% CbC の CodeGear, DataGear を用いたプログラミングスタイルと Agda での対応
ここでは CodeGear、DataGear を用いたプログラムを検証するため、
Agda 上での CodeGear、 DataGear の対応をみていく。


CodeGear は Agda では継続渡しで書かれた関数と等価である。
継続は不定の型 (\verb+t+) を返す関数で表される。
CodeGear 自体も同じ型 \verb+t+ を返す関数となる。
例えば、 Stack への push を行う関数 pushStack は以下のような型を持つ。

\begin{lstlisting}[caption=pushStack の型,label=push-stack]
   pushStack : a -> (Stack a si -> t) -> t
\end{lstlisting}

\verb+pushStack+ が関数名で、コロンの後ろに型を記述する。
最初の引数は Stack に格納される型\verb+a+ を持つ。
二つ目の引数は継続であり、\verb+Stack a si+ (\verb+si+という実装を持つ\verb+a+を格納するStack)を受け取り不定の型\verb+t+を返す関数である。
この CodeGear 自体は不定の型\verb+t+を返す。

GearsOS で CodeGear の性質を証明するには、 Agda で記述された CodeGear と
DataGear に対してメタ計算として証明を行う。証明すべき性質は、不定の型を持つ継続
\verb+t+ に記述することができる。例えば、 Stack にある値\verb+x+をpushして、pop
すると \verb+ x'+ が取れてくる。\verb+Just x+ と\verb+Just x'+ は等しい必要があ
る。これは Agda では \verb+(Just x ≡ x')+ と記述される。
ここで Just とは Agda の以下のデータ構造である。

% \begin{verbatim}
\begin{lstlisting}[caption=data型の例:Maybe,label=maybe]
data Maybe {n : Level } (a : Set n) : Set n where
  Nothing : Maybe a
  Just    : a -> Maybe a
\end{lstlisting}
% \end{verbatim}

これは DataGear に相当し、\verb+Nothing+ と \verb+Just+ の二つの状態を保つ。
pop した時に、 Stack が空であれば\verb+Nothing+ を返し、そうでなければ\verb+Just+ のついた返り値を返す。

この性質を Agda で表すと、以下のような型になる。
Agda では証明すべき論理式は型で表される。
継続部分に直接証明すべき性質を型として記述できる。
Agda ではこの型に対応する$\lambda$項を与えると証明が完了したことになる。

\begin{lstlisting}[caption=pushとpop,label=push-pop]
push->pop : {l : Level} {D : Set l} (x : D )
        (s : SingleLinkedStack D) -> 
        pushStack (stackInSomeState s)
        x (\s -> popStack s 
        ( \s3 x1 -> (Just x ≡ x1)))
\end{lstlisting}

このように、CodeGear を Agda で記述し、継続部分に証明すべき性質を Agda で記述する。

%% GearsOS での記述は interface によってモジュール化される。
%% よって、このモジュール化もAgda により記述する必要がある。
%% CbC で記述された任意の CodeGear と Meta CodeGear が Agda にそのまま変換されるわけではないが、変換可能なように記述されると仮定する。

\section{HoareLogic}
%% HoareLogic の説明と Commands、 Rules の説明。公理としてのものなのですべて説明。

HoareLogic とは C.A.R Hoare、 R.W Floyd らによるプログラムの検証のアイディアである。
これはプログラムの部分的な正当性を検証するアイディアで、
事前条件(Pre-Condition) P が成り立つとき、コマンド C を実行した後に
事後条件(Post-Condition) Q が成り立つ。
これを ${P} C {Q}$ のように表し、コマンドをつなげてプログラム全体を記述することで、
プログラム内のすべての部分について検証を行うことができる。
%% これは、プログラムを Skip、 Abort、 Seq、 PComm、 If、 While の6つの規則で記述することで

HoareLogic ではプログラムを  Assign、 Sequential Composition、 If、 While というコマンドで
記述する。

%% Skip は動作をしないコマンドで事前条件や事後条件に変化を与えない。
%% About は途中で処理を中断するコマンドで Skip と同様、条件に変化を与えることはない。
%% Assign は変数に値を代入するコマンドで、事前条件では代入する前の変数が存在することと
%% 事後条件ではその変数に値が代入されていることになる。
%% Sequential


\section{AgdaでのHoareLogic}
本章では、Agda 上での HoareLogic についての記述と検証を行う。
今回は、\ref{agda-while} のような while Loop に対しての検証を行うこととする。

\begin{lstlisting}[caption=while Loop,label=agda-while]
  n = 10;
  i = 0;

  while (n>0)
  {
    i++;
    n--;
  }
\end{lstlisting}

\ref{agda-while}では最初期の事前条件は何もなく、プログラムが停止するときの条件として、 $i==10 ∧ n == 0$ が成り立つ。
また、 $n = 10$、 $i = 0$、 といった代入に事前条件と、事後条件をつけ、 while文 にループの普遍条件をつけることになる。

\ref{agda-hoare} は Agda上での HoareLogic の構築子である。

$Env$ は\ref{agda-while}の n、 i といった変数をまとめたものであり、型として Agda 上での自然数の型である Nat を持つ。
PrimComm は Primitive Command で、 n、i といった変数に 代入するときに使用される関数である。
Cond は Condition で、 変数を受け取って　Bool値を返す関数となっている。
Agda のデータで定義されている Comm は HoareLogic での Command を表す。
Skip は何も変更しない Command で、 Abort はプログラムを中断する Command である。

PComm は PrimComm を受けて Command を返す型で定義されていて、 変数を代入するときに使われる。
Seq は Sequence Composition で Command を2つ受けて Command を返す型で定義されている。これは、ある Command から Command に移り、その結果を次の Command に渡す型になっている。
If は Cond と Comm を2つ受け取り、 Cond の中身によって Comm を変える Command である。
While は Cond と Comm を受け取り、 Cond の中身が True である間、 Comm を繰り返す Command である。

\begin{lstlisting}[caption=Agda での HoareLogic の構成,label=agda-hoare]
record Env : Set where
  field
    varn : ℕ
    vari : ℕ
open Env

PrimComm : Set
PrimComm = Env → Env

Cond : Set
Cond = (Env → Bool) 

data Comm : Set where
  Skip  : Comm
  Abort : Comm
  PComm : PrimComm -> Comm
  Seq   : Comm -> Comm -> Comm
  If    : Cond -> Comm -> Comm -> Comm
  While : Cond -> Comm -> Comm
\end{lstlisting}

Agda 上の HoareLogic で使われるプログラムは Comm 型の関数となる。
プログラムの処理を Seq でつないでいき、最終的な状態にたどり着くと値を返して止まる。
%% \ref{agda-hoare-simpl} は 変数 $i$、 $n$ に代入を行うプログラムである。
%% これは Seq で PComm を2つ繋げた形になる。
\ref{agda-hoare-prog}は\ref{agda-while}で書いた While Loop を HoareLogic での Comm で記述したものである。
ここでの $\$$は $()$の対応を合わせる Agda の糖衣で、行頭から行末までを $()$で囲っていることと同義である。

\begin{lstlisting}[caption= HoareLogic のプログラム ,label=agda-hoare-prog]
program : Comm
program = 
    Seq ( PComm (λ env → record env {varn = 10}))
    $ Seq ( PComm (λ env → record env {vari = 0}))
    $ While (λ env → lt zero (varn env ) )
      (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} ))
        $ PComm (λ env → record env {varn = ((varn env) - 1)} ))

\end{lstlisting}

しかし、 この Comm は Command をならべているだけである。
そのため、この Command を Agda 上で実行するため、 \ref{agda-hoare-interpret} のような interpreter を記述した。
\begin{lstlisting}[caption=Agda での HoareLogic interpreter ,label=agda-hoare-interpret]
{-# TERMINATING #-}
interpret : Env → Comm → Env
interpret env Skip = env
interpret env Abort = env
interpret env (PComm x) = x env
interpret env (Seq comm comm1) = interpret (interpret env comm) comm1
interpret env (If x then else) with x env
... | true = interpret env then
... | false = interpret env else
interpret env (While x comm) with x env
... | true = interpret (interpret env comm) (While x comm)
... | false = env
\end{lstlisting}

\ref{agda-hoare-interpret}は 初期状態の Env と 実行する Command の並びを受けとって、実行後の Env を返すものとなっている。

\begin{lstlisting}[caption=Agda での HoareLogic の実行 ,label=agda-hoare-run]
test : Env
test =  interpret ( record { vari = 0  ; varn = 0 } ) programt
\end{lstlisting}
\ref{agda-hoare-run}のように interpret に $vari = 0 , varn = 0$ の record を渡し、 実行する Comm を渡して 評価してやると$record { varn = 0 ; vari = 10 }$ のような Env が返ってくる。

次に先程書いたプログラムの証明について記述する。

\ref{agda-hoare-rule} は Agda 上での HoareLogic での証明の構成である。
HTProof では Condition と Command もう一つ Condition を受け取って、 Set を返す Agda のデータである。
-- これは Pre と Post の Condition を Command で変化させる

\begin{lstlisting}[caption=Agda での HoareLogic の構成,label=agda-hoare-rule]
data HTProof : Cond -> Comm -> Cond -> Set where
  PrimRule : {bPre : Cond} -> {pcm : PrimComm} -> {bPost : Cond} ->
             (pr : Axiom bPre pcm bPost) ->
             HTProof bPre (PComm pcm) bPost
  SkipRule : (b : Cond) -> HTProof b Skip b
  AbortRule : (bPre : Cond) -> (bPost : Cond) ->
              HTProof bPre Abort bPost
  WeakeningRule : {bPre : Cond} -> {bPre' : Cond} -> {cm : Comm} ->
                {bPost' : Cond} -> {bPost : Cond} ->
                Tautology bPre bPre' ->
                HTProof bPre' cm bPost' ->
                Tautology bPost' bPost ->
                HTProof bPre cm bPost
  SeqRule : {bPre : Cond} -> {cm1 : Comm} -> {bMid : Cond} ->
            {cm2 : Comm} -> {bPost : Cond} ->
            HTProof bPre cm1 bMid ->
            HTProof bMid cm2 bPost ->
            HTProof bPre (Seq cm1 cm2) bPost
  IfRule : {cmThen : Comm} -> {cmElse : Comm} ->
           {bPre : Cond} -> {bPost : Cond} ->
           {b : Cond} ->
           HTProof (bPre /\ b) cmThen bPost ->
           HTProof (bPre /\ neg b) cmElse bPost ->
           HTProof bPre (If b cmThen cmElse) bPost
  WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} ->
              HTProof (bInv /\ b) cm bInv ->
              HTProof bInv (While b cm) (bInv /\ neg b)
\end{lstlisting}

\ref{agda-hoare-rule}を使って先程の while Program を証明する。
証明は \ref{agda-hoare-rule}の proof1 の様になる。

\begin{lstlisting}[caption=Agda 上での WhileLoop の検証,label=agda-hoare-while]
initCond : Cond
initCond env = true

stmt1Cond : Cond
stmt1Cond env = Equal (varn env) 10

stmt2Cond : Cond
stmt2Cond env = (Equal (varn env) 10) ∧ (Equal (vari env) 0)

whileInv : Cond
whileInv env = Equal ((varn env) + (vari env)) 10

whileInv' : Cond
whileInv' env = Equal ((varn env) + (vari env)) 11

termCond : Cond
termCond env = Equal (vari env) 10
  
proof1 : HTProof initCond program termCond
proof1 =
      SeqRule {λ e → true} ( PrimRule empty-case )
    $ SeqRule {λ e →  Equal (varn e) 10} ( PrimRule lemma1   )
    $ WeakeningRule {λ e → (Equal (varn e) 10) ∧ (Equal (vari e) 0)}  lemma2 (
            WhileRule {_} {λ e → Equal ((varn e) + (vari e)) 10}
            $ SeqRule (PrimRule {λ e →  whileInv e  ∧ lt zero (varn e) } lemma3 )
                     $ PrimRule {whileInv'} {_} {whileInv}  lemma4 ) lemma5
\end{lstlisting}

proof1 は\ref{agda-hoare-prog}の program と似た形をとっている。
Comannd に対応する証明規則があるため、証明はプログラムに対応する形になる。

\begin{lstlisting}[caption=Gears 上での WhileLoop の検証,label=Gears-hoare-while]
proofGears : {c10 :  ℕ } → Set
proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 ))))

proofGearsMeta : {c10 :  ℕ } → whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1(λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 ))))
proofGearsMeta {c10} = {!!}
\end{lstlisting}

\begin{thebibliography}{99}
%\bibitem{ohno}
%大野義夫編，\TeX\ 入門，
%共立出版，東京，1989. 

%\bibitem{Seroul}
%R. Seroul and S. Levy, A Beginner's Book of \TeX, 
%Springer-Verlag, New York, 1989. 

%\bibitem{nodera1}
%野寺隆志，楽々\LaTeX{}，
%共立出版，東京，1990. 

%\bibitem{itou}
%伊藤和人，\LaTeX\ トータルガイド，
%秀和システムトレーディング，1991. 

%\bibitem{nodera2}
%野寺隆志，今度こそ\AmSLaTeX{}，
%共立出版，東京，1991. 

\bibitem{ryokka-sigos}
外間政尊, 河野真治, GearsOSのAgdaによる記述と検証，
\\システムソフトウェアとオペレーティング・システム研究会, 2018.

%% \bibtem{agda-alfa}
%% \url{http://ocvs.cfv.jp/Agda/}

%% \bibtem{agda2-hoare}
%% \url{https://github.com/IKEGAMIDaisuke/HoareLogic}


\end{thebibliography}

\end{document}