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

\usepackage[dvipdfmx]{graphicx}
\usepackage{graphicx}
\usepackage{lmodern}
\usepackage{textcomp}
\usepackage{latexsym}
\usepackage{ascmac}
\usepackage[fleqn]{amsmath}
\usepackage{amssymb}
\usepackage[deluxe, multi]{otf}
\usepackage{url}
\usepackage{cite}
\usepackage[portuguese]{babel}
\usepackage[utf8]{inputenc}
\usepackage{listingsutf8}
\usepackage{listings}
\usepackage{colonequals}
\usepackage{inconsolata}
\lstset{
  frame=single,
  keepspaces=true,
  stringstyle={\ttfamily},
  commentstyle={\ttfamily},
  identifierstyle={\ttfamily},
  keywordstyle={\ttfamily},
%  basicstyle=\footnotesize,
  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,
  stringstyle={\ttfamily},
  escapechar={@},
  %% mathescape=true,
}

  %% literate=
  %% {⟨}{{\langle}}1
  %% {⟩}{{\rangle}}1
  %% {ℕ}{{$\mathbb{N}$}}1
  %% {^^e2^^84^^95}{{$\mathbb{N}$}}1

% basicstyle={\ttfamily},
\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{まえがき}
OS やアプリケーションの信頼性は重要である。
信頼性を上げるには仕様を満たしていることを検証する必要がある。
プログラムの検証手法として、Floyd–Hoare logic (以下 Hoare Logic)が存在している。
HoareLogic は事前条件が成り立っているときにある
関数を実行して、それが停止する際に事後条件を満た
すことを確認することで、検証を行う。
HoareLogic はシンプルなアプローチだが通常のプログラミング言語で使用することができず、
広まっているとはいえない。

当研究室では信頼性の高い OS として GearsOS を開発している。
現在 GearsOS ではCodeGear、DataGearという単位を用いてプログラムを記述する手法を用いており、
仕様の確認には定理証明系である Agda を用いている。

CodeGearは Agda 上では継続渡しの記述を用いた関数として
記述する。
また、継続にある関数を実行するための事前条件や
事後条件などをもたせることが可能である。

そのため Hoare Logic と CodeGear、DataGear という単位を用いたプログラミング手法
記述と相性が良く、既存の言語とは異なり HoareLogic を使ったプログラミングができると考えている。

本研究では Agda 上での HoareLogic の記述を使い、簡単なwhile Loop のプログラムを作成し、証明を行った。
また、GearsOS の仕様確認のために CodeGear、DataGear という単位を用いた記述で Hoare Logic をベースと
したwhile Loop プログラムを記述、その証明を行なった。


\section{現状}
現在の OS やアプリケーションの検証では、実装と別に検証用の言語で記述された実装と証明を持つのが一般的である。
kernel 検証\cite{Klein:2010:SFV:1743546.1743574},\cite{Nelson:2017:HPV:3132747.3132748}の例では C で記述された Kernel に対して。
また、別のアプローチとしては ATS や Rust などの低レベル記述向けの関数型言語を実装に用いる手法が存在している。

証明支援向けのプログラミング言語としては Agda、 Coq などが存在しているが、これらの言語は実行速度が期待できるものではない。

この現状から、証明の記述とプログラムの記述が別になっていることがネックになっているのではないかと考えている

\section{Agda}
Adga \cite{agda} とは証明支援系言語である。
Agdaにおける型指定は : を用いて行う。例えば、 変数 x が型 A を持つ、ということを表すには x : A と記述する。
データ型は、代数的なデータ構造で、その定義には data キーワードを用いる。
data キーワードの後に data の名前と、型、 where 句を書きインデントを深 くした後、
値にコンストラクタとその型を列挙する。 Code \ref{agda-data} はこの data 型の例である。
Comm では Skip、Abort、PComm などのコンストラクタを持ち、: の後に型が書かれている。

\begin{lstlisting}[caption=data の例,label=agda-data]
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 には C における構造体に相当するレコード型というデータも存在する、
record キーワード後の内部に field キーワードを記述し、その下に Name = value の形で値を列挙していく。
複数の値を列挙する際は ; で区切る必要がある。
 Code \ref{agda-record} はレコード型の例であり、Env では varn と vari の二つの field を持ち、
それぞれの型が Agda 上で自然数を表す Nat になっている。

\lstinputlisting[caption=record の例,label=agda-record]{src/record.agda.replaced}
%% \begin{lstlisting}[caption=record の例,label=agda-record]
%% record Env : Set where
%%   field
%%     varn : ℕ
%%     vari : ℕ
%% \end{lstlisting}

関数の定義は、関数名と型を記述した後に関数の本体を = の後に記述する。関数の型には → 、または$->$ を用いる。
例えば引数が型 A で返り値が型 B の関数は A $->$ B のように書ける。また、複数の引数を取る関数の型は A $->$ A $->$ B のように書ける。この時の型は A $->$ (A $->$ B) のように考えられる。
ここでは Code \ref{agda-function}を例にとる。これは引き算の演算子で、Agda の Nat を二つ引数に受けて Nat を返す
関数である。　

\lstinputlisting[caption=関数の例,label=agda-function]{src/function.agda.replaced}
%% \begin{lstlisting}[caption=関数の例,label=agda-function]
%% _-_ : ℕ →ℕ →ℕ
%% x - zero  = x
%% zero - _  = zero
%% (suc x) - (suc y)  = x - y
%% \end{lstlisting}  

Agda での証明では型部分に証明すべき論理式、 $\lambda$ 項部分にそれを満たす証明を書くことで証明が完成する。
証明の例として Code \ref{proof} を見る。
ここでの $+zero$ は右から zero を足しても $\equiv$ の両辺は等しいことを証明している。
これは、引数として受けている y が Nat なので、 zero の時と suc y の二つの場合を証明する必要がある。

$y = zero$ の時は両辺が zero とできて、左右の項が等しいということを表す refl で証明することができる。
$y = suc y$ の時は x == y の時 fx == fy が成り立つという cong を使って、y の値を 1 減らしたのちに再帰的に $+zero y$
を用いて証明している。
\lstinputlisting[caption=等式変形の例,label=proof]{src/zero.agda.replaced}
%% \begin{lstlisting}[caption=等式変形の例,label=proof]
%% +zero : { y : ℕ } → y + zero  ≡ y
%% +zero {zero} = refl
%% +zero {suc y} = cong ( λ x → suc x ) ( +zero {y} )
%% \end{lstlisting}

また、他にも $\lambda$ 項部分で等式を変形する構文が存在している。
 Code \ref{agda-term-pre}、 \ref{agda-term-post} は等式変形の例である。
始めに等式変形を始めたいところで $let open \equiv-Reasoning  in begin$と記述する。
Agda 上では分からないところを ? と置いておくことができるので、残りを ? としておく。
$--$ は Agda 上ではコメントである。

\lstinputlisting[caption=等式変形の例1/2,label=agda-term-pre]{src/term1.agda.replaced}
%% \begin{lstlisting}[caption=等式変形の例1/3,label=agda-term-pre]
%% stmt2Cond : {c10 : ℕ} → Cond
%% stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0)

%% lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c\
%% 10})
%% lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning  in
%%   begin
%%     ?      -- ?0
%%   ≡⟨ ? ⟩  -- ?1
%%     ?      -- ?2
%%   ∎ )

%% -- ?0 : Bool
%% -- ?1 : stmt2Cond (record { varn = varn env ; vari = 0 }) ≡ true
%% -- ?2 : Bool
%% \end{lstlisting}  

この状態で Compile すると ? 部分に入る型を Agda が示してくれるため、始めに変形する等式を ?0 に
記述し、?1 の中に $x == y$ のような変形規則を入れることで等式を変形して証明することができる。

ここでは \ref{agda-term-mid} の Bool 値 x を受け取って $x \wedge true$ の時必ず x であるという証明 $\wedge$true と 値と Env を受け取って Bool 値を返す stmt1Cond を使って等式変形を行う。
\lstinputlisting[caption=使っている等式変形規則,label=agda-term-mid]{src/term2.agda.replaced}
%% \begin{lstlisting}[caption=等式変形の例2/3,label=agda-term-mid]
%% ∧true : { x : Bool } →  x  ∧  true  ≡ x
%% ∧true {x} with x
%% ∧true {x} | false = refl
%% ∧true {x} | true = refl

%% stmt1Cond : {c10 : ℕ} → Cond
%% stmt1Cond {c10} env = Equal (varn env) c10
%% \end{lstlisting}

最終的な証明は\ref{agda-term-post} のようになる。
\lstinputlisting[caption=等式変形の例2/2,label=agda-term-post]{src/term3.agda.replaced}
%% \begin{lstlisting}[caption=等式変形の例2/2,label=agda-term-post]
%% lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c\
%% 10})
%% lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning  in
%%   begin
%%     (Equal (varn env) c10 ) ∧ true
%%   ≡⟨ ∧true ⟩
%%     Equal (varn env) c10
%%   ≡⟨ cond ⟩
%%     true
%%   ∎ )
%% \end{lstlisting}


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

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

\section{CodeGearとDataGear}
Gears OS ではプログラムとデータの単位として CodeGear、 DataGear を用いる。 Gear
 は並列実行の単位、データ分割、 Gear 間の接続等になる。
CodeGear はプログラムの処理そのもので、図 Code \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.425}{\includegraphics{pic/meta_cg_dg.pdf}}
 \end{center}
 \caption{CodeGear と DataGear の関係}
 \label{fig:cgdg}
\end{figure}

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

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

CodeGear は Agda では継続渡しで書かれた関数と等価である。
継続は不定の型 (\verb+t+) を返す関数で表される。
CodeGear 自体も同じ型 \verb+t+ を返す関数となる。
 Code \ref{agda-cg}は Agda で書いた CodeGear の型の例である。

\lstinputlisting[caption= whileTest の型,label=agda-cg]{src/while-test.agda.replaced}
%% \begin{lstlisting}[caption= whileTest の型,label=agda-cg]
%% whileTest : {l : Level} {t : Set l} -> (c10 : ℕ) → (Code : Env -> t) -> t
%% whileTest c10 next = next (record {varn = c10 ; vari = 0} )
%% \end{lstlisting}


GearsOS で CodeGear の性質を証明するには、 Agda で記述された CodeGear と
DataGear に対して証明を行う。証明すべき性質は、不定の型を持つ継続
\verb+t+ に記述することができる。
例えば、 Code \ref{gears-proof} では $(vari e) ≡ 10 $ が証明したい命題で、whileTest
から、whileLoop の CodeGear に継続した後、この命題が正しければよい。
この証明は proof1 の型に対応する$\lambda$項を与えると証明が完了したことになる。
ここで与えている refl は x==x で、命題が正しいことが証明できている。

% \begin{verbatim}
\begin{lstlisting}[caption=Agda での証明の例,label=gears-proof]
proof1 : whileTest 10 (λ env → whileLoop env (λ e → (vari e) ≡ 10 ))
proof1 = refl
\end{lstlisting}
% \end{verbatim}

%% \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 についての記述と検証を行う。

今回は、 Code \ref{agda-while} のような while Loop に対しての検証を行う。

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

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

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

現在 Agda 上での HoareLogic は初期の Agda で実装されたもの \cite{agda-alpa}とそれを現在のAgdaに対応させたもの \cite{agda2-hoare}が存在している。

今回は現在のAgdaに対応させたもの \cite{agda2-hoare}の Command と証明のためのルールを使って HoareLogic を実装した。
 Code \ref{agda-hoare} は Agda上での HoareLogic の構築子である。
ここでの Comm は Agda2 に対応した Command の定義をそのまま使っている。

%  Code \ref{agda-alfa} \cite{agda2-hoare}
$Env$ は Code \ref{agda-while}の n、 i といった変数をまとめたものであり、型として Agda 上での自然数の型である Nat を持つ。

PrimComm は Primitive Command で、 n、i といった変数に 代入するときに使用される関数である。

Cond は HoareLogic の Condition で、 Env を受け取って　Bool 値を返す関数となっている。


Agda のデータで定義されている Comm は HoareLogic での Command を表す。

Skip は何も変更しない Command で、 Abort はプログラムを中断する Command である。

PComm は PrimComm を受けて Command を返す型で定義されており、 変数を代入するときに使われる。

Seq は Sequence で Command を2つ受けて Command を返す型で定義されている。
これは、ある Command から Command に移り、その結果を次の Command に渡す型になっている。

If は Cond と Comm を2つ受け取り、 Cond が true か false かで 実行する Comm を変える Command である。

While は Cond と Comm を受け取り、 Cond の中身が True である間、 Comm を繰り返す Command である。

\begin{lstlisting}[caption=Agda での HoareLogic の構成,label=agda-hoare]
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 でつないでいき、最終的な状態にたどり着くと値を返して止まる。
%%  Code \ref{agda-hoare-simpl} は 変数 $i$、 $n$ に代入を行うプログラムである。
%% これは Seq で PComm を2つ繋げた形になる。
 Code \ref{agda-hoare-prog}は Code \ref{agda-while}で書いた While Loop を HoareLogic での Comm で記述したものである。
ここでの $\$$は $()$の対応を合わせる Agda の糖衣構文で、行頭から行末までを $()$で囲っていることと同義である。

\begin{lstlisting}[caption= HoareLogic のプログラム ,label=agda-hoare-prog,mathescape=false]
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 をならべているだけである。
この Comm を Agda 上で実行するため、  Code \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}

 Code \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 } ) program
\end{lstlisting}

 Code \ref{agda-hoare-run}のように interpret に $vari = 0 , varn = 0$ の record を渡し、 実行する Comm を渡して 評価してやると$record { varn = 0 ; vari = 10 }$ のような Env が返ってくる。

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

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

PrimRule は Code \ref{axiom-taut} の Axiom という関数を使い、事前条件が成り立っている時、
実行後に事後条件が成り立つならば、 PComm で変数に値を代入できることを保証している。

SkipRule は Condition を受け取ってそのままの Condition を返すことを保証する。

AbortRule は PreContition を受け取って、Abort を実行して終わるルールである。

WeakeningRule は \ref{axiom-taut} の Tautology という関数を使って通常の逐次処理から、
WhileRule のみに適応されるループ不変変数に移行する際のルールである。

SeqRule は3つの Condition と 2つの Command を受け取り、これらのプログラムの逐次的な実行を保証する。

IfRule は分岐に用いられ、3つの Condition と 2つの Command を受け取り、判定の Condition が成り立っているかいないかで実行する Command を変えるルールである。
この時、どちらかの Command が実行されることを保証している。

WhileRule はループに用いられ、1つの Command と２つの Condition を受け取り、事前条件が成り立っている間、 Command を繰り返すことを保証している。

\begin{lstlisting}[caption=Axiom と Tautology,label=axiom-taut]
_⇒_ : Bool → Bool → Bool
false  ⇒  _ = true
true  ⇒  true = true
true  ⇒  false = false

Axiom : Cond -> PrimComm -> Cond -> Set
Axiom pre comm post = ∀ (env : Env) →  (pre env) ⇒ ( post (comm env)) ≡ true

Tautology : Cond -> Cond -> Set
Tautology pre post = ∀ (env : Env) →  (pre env)  ⇒ (post env) ≡ true
\end{lstlisting}

\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}

Code \ref{agda-hoare-rule}を使って Code \ref{agda-while}の whileProgram を証明する。

全体の証明は  Code \ref{agda-hoare-while}の proof1 の様になる。
proof1 では型で initCond、  Code \ref{agda-hoare-prog}のprogram、 termCond を記述しており、
initCond から program を実行し termCond に行き着く HoareLogic の証明になっている。

それぞれの Condition は Rule の後に記述されている {} に囲まれた部分で、
initCondのみ無条件で true を返す Condition になっている。

それぞれの Rule の中にそこで証明する必要のある補題が lemma で埋められている。
lemma1 から lemma5 の証明は長く、
論文のページ上限を超えてしまうため 当研究室レポジトリ \cite{cr-ryukyu} のプログラムを参照していただきたい。

これらの lemma は HTProof の Rule に沿って必要なものを記述されており、
lemma1 では PreCondition と PostCondition が存在するときの代入の保証、
lemma2 では While Loop に入る前の Condition からループ不変条件への変換の証明、
lemma3 では While Loop 内での PComm の代入の証明、
lemma4 では While Loop を抜けたときの Condition の整合性、
lemma5 では While Loop を抜けた後のループ不変条件からCondition への変換と termCond への移行の整合性を保証している。

\begin{lstlisting}[caption=Agda 上での WhileLoop の検証,label=agda-hoare-while]  
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}

%% \begin{lstlisting}[caption=whileProgram Condition, label=while-cond]
%% initCond : Cond
%% initCond env = true

%% stmt1Cond : {c10 : ℕ} → Cond
%% stmt1Cond {c10} env = Equal (varn env) c10

%% init-case : {c10 : ℕ} → (env : Env) → (( λ e → true  ⇒ stmt1Cond {c10} e ) (record { varn = c10 ; vari \
%% = vari env }) ) ≡ true
%% init-case {c10} _ = impl⇒ ( λ cond → ≡→Equal refl )

%% init-type : {c10 : ℕ} → Axiom (λ env → true) (λ env → record { varn = c10 ; vari = vari env }) (stmt1Co\
%% nd {c10})
%% init-type {c10} env = init-case env

%% stmt2Cond : {c10 : ℕ} → Cond
%% stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0)

%% whileInv : {c10 : ℕ} → Cond
%% whileInv {c10} env = Equal ((varn env) + (vari env)) c10

%% whileInv' : {c10 : ℕ} → Cond
%% whileInv' {c10}  env = Equal ((varn env) + (vari env)) (suc c10) ∧ lt zero (varn env)

%% termCond : {c10 : ℕ} → Cond
%% termCond {c10} env = Equal (vari env) c10
%% \end{lstlisting}

%% \begin{lstlisting}[caption=proof1 の lemma ,label=agda-hoare-while-lemma]
%% lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10})
%%     (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10})
%% lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning  in
%%   begin
%%     (Equal (varn env) c10 ) ∧ true
%%   ≡⟨ ∧true ⟩
%%     Equal (varn env) c10
%%   ≡⟨ cond ⟩
%%     true
%%   ∎ )

%% lemma21 : {env : Env } → {c10 : ℕ} → stmt2Cond env ≡ true → varn env ≡ c10
%% lemma21 eq = Equal→≡ (∧-pi1 eq)
%% lemma22 : {env : Env } → {c10 : ℕ} → stmt2Cond {c10} env ≡ true → vari env ≡ 0
%% lemma22 eq = Equal→≡ (∧-pi2 eq)
%% lemma23 :  {env : Env } → {c10 : ℕ} → stmt2Cond env ≡ true → varn env + vari env ≡ c10
%% lemma23 {env} {c10} eq = let open ≡-Reasoning  in
%%    begin
%%      varn env + vari env
%%    ≡⟨ cong ( \ x -> x + vari env ) (lemma21 eq  ) ⟩
%%      c10 + vari env
%%    ≡⟨ cong ( \ x -> c10 + x) (lemma22 {env} {c10} eq ) ⟩
%%      c10 + 0
%%    ≡⟨ +-sym {c10} {0} ⟩
%%      0 + c10 
%%    ≡⟨⟩
%%      c10 
%%    ∎
%% lemma2 :  {c10 : ℕ} → Tautology stmt2Cond whileInv
%% lemma2 {c10} env = bool-case (stmt2Cond env) (
%%    λ eq → let open ≡-Reasoning  in
%%      begin
%%        (stmt2Cond env)  ⇒  (whileInv env)
%%      ≡⟨⟩
%%        (stmt2Cond env)  ⇒ ( Equal (varn env + vari env) c10 )
%%      ≡⟨  cong ( \ x -> (stmt2Cond  {c10} env)  ⇒ ( Equal x c10 ) ) ( lemma23 {env} eq ) ⟩
%%        (stmt2Cond env)  ⇒ (Equal c10 c10)
%%      ≡⟨ cong ( \ x -> (stmt2Cond {c10} env) ⇒ x ) (≡→Equal refl )  ⟩
%%        (stmt2Cond {c10} env)  ⇒  true
%%      ≡⟨ ⇒t ⟩
%%        true
%%    ∎
%%    ) (
%%      λ ne → let open ≡-Reasoning  in
%%    begin
%%    (stmt2Cond env)  ⇒  (whileInv env)
%%    ≡⟨ cong ( \ x -> x  ⇒  (whileInv env) ) ne ⟩
%%              false  ⇒  (whileInv {c10} env)
%%           ≡⟨ f⇒ {whileInv {c10} env} ⟩
%%             true
%%           ∎
%%         ) 
%%      lemma3 :   Axiom (λ e → whileInv e ∧ lt zero (varn e)) (λ env → record { varn = varn env ; vari = vari env + 1 }) whileInv'
%%      lemma3 env = impl⇒ ( λ cond →  let open ≡-Reasoning  in
%%           begin
%%             whileInv' (record { varn = varn env ; vari = vari env + 1 }) 
%%           ≡⟨⟩
%%              Equal (varn env + (vari env + 1)) (suc c10) ∧ (lt 0 (varn env) )
%%           ≡⟨ cong ( λ z → Equal (varn env + (vari env + 1)) (suc c10) ∧ z ) (∧-pi2 cond )  ⟩
%%              Equal (varn env + (vari env + 1)) (suc c10) ∧ true
%%           ≡⟨ ∧true ⟩
%%             Equal (varn env + (vari env + 1)) (suc c10)
%%           ≡⟨ cong ( \ x -> Equal x (suc c10) ) (sym (+-assoc (varn env) (vari env) 1)) ⟩
%%             Equal ((varn env + vari env) + 1) (suc c10)
%%           ≡⟨ cong ( \ x -> Equal x (suc c10) ) +1≡suc ⟩
%%             Equal (suc (varn env + vari env)) (suc c10)
%%           ≡⟨ sym Equal+1 ⟩
%%             Equal ((varn env + vari env) ) c10
%%           ≡⟨ ∧-pi1  cond ⟩
%%             true
%%           ∎ )
%%      lemma41 : (env : Env ) → {c10 : ℕ} → (varn env + vari env) ≡ (suc c10) → lt 0 (varn env) ≡ true  → Equal ((varn env - 1) + vari env) c10 ≡ true
%%      lemma41 env {c10} c1 c2 =  let open ≡-Reasoning  in
%%           begin
%%             Equal ((varn env - 1) + vari env) c10
%%           ≡⟨ cong ( λ z → Equal ((z - 1 ) +  vari env ) c10 ) (sym (suc-pred*ℕ*=n c2) )  ⟩
%%             Equal ((suc (pred*ℕ* {varn env} c2 ) - 1) + vari env) c10
%%           ≡⟨⟩
%%             Equal ((pred*ℕ* {varn env} c2 ) + vari env) c10
%%           ≡⟨  Equal+1 ⟩
%%             Equal ((suc (pred*ℕ* {varn env} c2 )) + vari env) (suc c10)
%%           ≡⟨ cong ( λ z → Equal (z  +  vari env ) (suc c10) ) (suc-pred*ℕ*=n c2 )  ⟩
%%             Equal (varn env + vari env) (suc c10)
%%           ≡⟨ cong ( λ z → (Equal z (suc c10) )) c1 ⟩
%%             Equal (suc c10) (suc c10)
%%           ≡⟨ ≡→Equal refl ⟩
%%             true
%%           ∎
%%      lemma4 :  {c10 : ℕ} → Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv
%%      lemma4 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning  in
%%           begin
%%             whileInv (record { varn = varn env - 1 ; vari = vari env })
%%           ≡⟨⟩
%%             Equal ((varn env - 1) + vari env) c10
%%           ≡⟨ lemma41 env (Equal→≡ (∧-pi1  cond)) (∧-pi2  cond) ⟩
%%             true
%%           ∎
%%         )
%%      lemma51 : (z : Env ) → neg (λ z → lt zero (varn z)) z ≡ true → varn z ≡ zero
%%      lemma51 z cond with lt zero (varn z) | (suc zero) ≤? (varn z)
%%      lemma51 z () | false | yes p
%%      lemma51 z () | true | yes p
%%      lemma51 z refl | _ | no ¬p with varn z
%%      lemma51 z refl | _ | no ¬p | zero = refl
%%      lemma51 z refl | _ | no ¬p | suc x = ⊥-elim ( ¬p (s≤s z≤n ) )
%%      lemma5 : {c10 : ℕ} →  Tautology ((λ e → Equal (varn e + vari e) c10) and (neg (λ z → lt zero (varn z)))) termCond
%%      lemma5 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning  in
%%          begin
%%             termCond env
%%           ≡⟨⟩
%%              Equal (vari env) c10 
%%           ≡⟨⟩
%%              Equal (zero + vari env) c10 
%%           ≡⟨ cong ( λ z →  Equal (z + vari env) c10 )  (sym ( lemma51 env ( ∧-pi2  cond ) )) ⟩
%%              Equal (varn env + vari env) c10 
%%           ≡⟨ ∧-pi1  cond  ⟩
%%              true
%%           ∎
%%         )
%% \end{lstlisting}
proof1 は Code \ref{agda-hoare-prog}の program と似た形をとっている。
HoareLogic では Comannd に対応する証明規則があるため、証明はプログラムに対応する形になる。

\section{Gears ベースの HoareLogic の証明}
次に Gears をベースにした HoareLogic の例を見ていく。
Gears を用いた記述では、 Input の DataGear 、 CodeGear、 Output の DataGearという
並びでプログラムを記述していく。
そのため、Input DataGear を PreCondition、 Command を CodeGear、 Output DataGear を PostCondition と
そのまま置き換えることができる。

こちらも通常の HoareLogic と同様に \ref{agda-while} のwhileプログラムと同様のものを記述する
Code \ref{Gears-hoare-while} は、 CodeGear、 DataGear を用いた Agda 上での while Program の記述であり、証明でもある。

\lstinputlisting[caption=Gears 上での WhileLoop の記述と検証,label=Gears-hoare-while]{src/gears.agda.replaced}
%% \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 ))))
%% \end{lstlisting}
Code \ref{Gears-hoare-while} で使われている CodeGear を見ていく

始めに Code \ref{gears-while} の whileTest では変数 i、n にそれぞれ 0 と 10 を代入している。
whileTest は最初のCodeGear なので initCondition は true で、
Code : の後ろに書かれた$(env : Env)  -> ((vari env) ≡ 0) /\ ((varn env) ≡ c10)$ が PostCondition である。
$\lambda$ 項の next には次のCodeGear が入り、継続される引数である env は whileTest の PostCondition であり、
次の CodeGear の PreCondition にあたる。
conversion1 は通常の Condition からループ不変条件に移行するためのもので前のCondition である $i == 0 and n == 10$ が
成り立っている時、$i + n == 10$ を返すCodeGear となっている。
whileLoop では conversion1 のループ不変条件を受け取ってWhile の条件である$0 < n$ が成り立っている間、 $i++;n++$
を行う。
そして、ループを抜けた後の termCondition は $i == 10$ となる。

\lstinputlisting[caption=Gears whileProgram, label=gears-while]{src/gears-while.agda.replaced}
%% \begin{lstlisting}[caption=Gears whileProgram, label=gears-while]
%% whileTest : {l : Level} {t : Set l}  -> {c10 : ℕ } → (Code : (env : Env)  ->
%%             ((vari env) ≡ 0) /\ ((varn env) ≡ c10) -> t) -> t
%% whileTest {_} {_} {c10} next = next env proof2
%%   where
%%     env : Env
%%     env = record {vari = 0 ; varn = c10}
%%     proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10)
%%     proof2 = record {pi1 = refl ; pi2 = refl}    

%% conversion1 : {l : Level} {t : Set l } → (env : Env) -> {c10 : ℕ } → ((vari env) ≡ 0) /\ ((varn env) ≡ c\
%% 10)
%%                -> (Code : (env1 : Env) -> (varn env1 + vari env1 ≡ c10) -> t) -> t
%% conversion1 env {c10} p1 next = next env proof4
%%    where
%%       proof4 : varn env + vari env ≡ c10
%%       proof4 = let open ≡-Reasoning  in
%%           begin
%%             varn env + vari env
%%           ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩
%%             c10 + vari env
%%           ≡⟨ cong ( λ n → c10 + n ) (pi1 p1 ) ⟩
%%             c10 + 0
%%           ≡⟨ +-sym {c10} {0} ⟩
%%             c10
%%           ∎

%% {-# TERMINATING #-}
%% whileLoop : {l : Level} {t : Set l} -> (env : Env) -> {c10 : ℕ } → ((varn env) + (vari env) ≡ c10) -> (Co\
%% de : Env -> t) -> t
%% whileLoop env proof next with  ( suc zero  ≤? (varn  env) )
%% whileLoop env proof next | no p = next env
%% whileLoop env {c10} proof next | yes p = whileLoop env1 (proof3 p ) next
%%     where
%%       env1 = record {varn = (varn  env) - 1 ; vari = (vari env) + 1}
%%       1<0 : 1 ≤ zero → ⊥
%%       1<0 ()
%%       proof3 : (suc zero  ≤ (varn  env))  → varn env1 + vari env1 ≡ c10
%%       proof3 (s≤s lt) with varn  env
%%       proof3 (s≤s z≤n) | zero = ⊥-elim (1<0 p)
%%       proof3 (s≤s (z≤n {n'}) ) | suc n =  let open ≡-Reasoning  in
%%           begin
%%              n' + (vari env + 1)
%%           ≡⟨ cong ( λ z → n' + z ) ( +-sym  {vari env} {1} )  ⟩
%%              n' + (1 + vari env )
%%           ≡⟨ sym ( +-assoc (n')  1 (vari env) ) ⟩
%%              (n' + 1) + vari env
%%           ≡⟨ cong ( λ z → z + vari env )  +1≡suc  ⟩
%%              (suc n' ) + vari env
%%           ≡⟨⟩
%%              varn env + vari env
%%           ≡⟨ proof  ⟩
%%              c10
%%           ∎    
%% \end{lstlisting}


\section{まとめと今後の課題}
本研究では Agda 上で HoareLogic のwhileを使った例題を作成し、
証明を行なった。

また、 Gears を用いた HoareLogic を記述することができた。
さらに、Gears を用いてHoareLocic 記述で、
証明を引数として受け渡して記述し、証明とプログラムを一体化することができた。

今後の課題としては GearsOS の検証のために、
RedBlackTree や SynchronizedQueue などのデータ構造の検証をHoareLogic ベースで行うことなどが挙げられる。
%% 特に SynchronizedQueue の検証のために、 並列なプログラムを状態遷移に変換する。

\nocite{*}
\bibliography{tecrep}{}
\bibliographystyle{plain}

\end{document}