ATS で組み込みドライバを実装してみる

暇なのか
暇じゃないのか
暇なのか

というわけで、ATS言語の勉強も兼ねて、組み込みのドライバを書いてみます。
目標は、できるだけ安全なドライバを作ること。ATSの表現能力や、課題があるとしたら何なのかという事を探ってみることも目的です。
実用性とか、実際に動作するかどうかは、ぶっちゃけ余り気にしません。
まあ、動くようには作るつもりですが、実機も持ってないので……。

ATSとはなんじゃ？　という人は

ATSは、証明プログラミングに対応したプログラミング言語です。
同様の言語は他にもありますが、その中でも「実際に動作するプログラムを記述することを前提にしている」「線形型の仕組みを採用することで、安全なリソース管理手法を提供している」のがATSの特徴です。……の、はずです。
詳しいことは、↓を参照してください。

そもそも、証明プログラミングがわかっていないという人は、↓を見ると良いでしょう。

わからなくても泣かない。

目標

今回はRX-110のドライバ実装を目指してみます。
なんでRXなのかと言うと　→　仕事で使ったので扱いやすいから。
なんで110なのかと言うと　→　一番単純で実装しやすそうだから。
とりあえずは端子ドライバを実装して、Lチカ/デジタル入力読み込みができるところを目指して行きます。

ビット演算ライブラリ

さて、CPU（正確にはMCUだけど）のレジスタを証明された形で扱うためには、ビット演算を行うための、これまた証明された関数が必要です。
レジスタを扱う関数宣言を一通り定義してみた感じでは、以下の定義が必要なようです。

受け取った数値の、指定されたビットをセットする関数
受け取った数値の、指定されたビットをクリアする関数
ビットの書き込み許可をエンコードするための命題

前の2つは普通に実装するだけなら3秒（誇張）でできる関数ですが、証明を入れながら作るとなるとなかなか大変です。
最後の命題は、ほぼ定義だけなのでそんなに大変ではない（なかった）です。
また、ここに書いてあるコードは、github（https://github.com/fujiik102/ats-rx-drivers）に公開してあります。今回の内容に関係するのは、Bit.satsです。

ビット、ビット列

まずは、ビットの定義から。

datasort bit = | O | I

datasort bits = BitsNil of () | BitsCons of (bits,bit)

bit種は0か1です。識別子の先頭に数字は使えないので、大文字のOとIで代用しています。
bits種は複数ビットをまとめた定義です。この後、非常に良く使う定義です。

BitsConsの引数がビット列→ビットの順番なのは、複数ビットの定義を行った時に下位ビットを右側にするためです。

要するに、この定義で例えば「0011」を定義すると

BitsCons (BitsCons (BitsCons (BitsCons (BitsNil,O),O),I),I)

のようになります。これが逆に定義されていると、

BitsCons (I,BitsCons (I,BitsCons (O,BitsCons (O,BitsNil))))

となってしまい、非常に分かりづらい事になります。
リトルエンディアンは人類の直感に反する悪夢のような表記（誇張表現）なので、ビット順が逆になっている事に気付かずに定義してしまい、後で慌てて直すハメに陥ったりするのです（1敗）

ビット長

dataprop BITSLEN (bits,int) =
 | BITSLENNIL (BitsNil,0) of ()
 | {n:int}{b:bit}{bs:bits}
   BITSLENCONS (BitsCons (bs,b),n+1) of BITSLEN (bs,n)

praxi bitslen_nat {n:int}{bs:bits} (BITSLEN (bs,n)):[0 <= n] void

ビット長に関する証明型の定義です。後述するBITSEQINTが長さに関する定義も含んでいるので、単体では余り使いません。
定義の内容は自明だと思うので、解説は省略します。わからない場合は、↑の方で挙げたページをなんか適当に読んで下さい（適当）
bitslen_natは、「0<=ビット長」という公理を導入しています。自明なように見える事実ですが、やってみた範囲では証明できなかったので、公理にしています。
2017-09-21追記　証明できました。「ビット長＜０」のケースが証明できなかったのですが、帰納法を使って矛盾を作れば良いだけだったようです。

ビット⇔整数の対応

dataprop BITEQINT (bit, int) =
 | B0EQ0 (O, 0) of ()
 | B1EQ1 (I, 1) of ()

typedef bit_uint_t (b:bit) = [v:int] (BITEQINT (b,v) | uint v)

dataprop BITSEQINT (int, bits, int) =
 | BEQNIL (0,BitsNil,0) of ()
 | {n:int}{b:bit}{bs:bits}{v,bitv:int | v <= INTMAX_HALF}
   BEQCONS (n+1,BitsCons (bs,b),v+v+bitv)
   of (BITSEQINT (n,bs,v),BITEQINT (b,bitv))

typedef bits_uint_t (n:int,bs:bits) =
  [v:int] (BITSEQINT (n,bs,v) | uint v)

（これ、字下げとかはどうするのが正解なんですかね……？）
BITSEQINTは、bits種とint種をつなぐ、キーになる命題です。
1番目の引数でビット列の長さを受け取っています。これは、単純にintだけを指定しても対応するbitsが一意にならない（例えば、1という整数に対応するビット列は「01」、「001」など無数にある）ので、補助のためにつけています。

また、命題をいちいち書くのは煩わしいので、短縮して書くためにbit_uint_tとbits_uint_tを定義しています。bits_uint_tは、関数の定義などでは特に多用します。
ATSのビット演算ではuint型を使うので、int型ではなくuint型に結びつけてあります。

１バイトの簡易表現

stadef Bits8 (b7,b6,b5,b4,b3,b2,b1,b0:bit): bits =
  BitsCons (BitsCons (BitsCons (BitsCons (
  BitsCons (BitsCons (BitsCons (BitsCons (
  BitsNil,b7),b6),b5),b4),b3),b2),b1),b0)

bitsの値を表現する際、BitsConsやBitNilを使って書くのは冗長（というか、文字数が多過ぎ）なので、1バイト分のBitsを短く書くための定義です。
RX110のレジスタは基本的に8ビットなので、レジスタの定義では頻繁に使用します。

ビットの変更

dataprop CHANGE_BIT_BITS (int,bits,int,bit,bits) =
 | {n:int}{b,c:bit}{bs:bits} CHANGE_BIT_BITS_bas
     (n+1,BitsCons (bs,b),0,c,BitsCons (bs,c)) of (BITSLEN (bs,n))
 | {n,bn:int}{b,c:bit}{bs,cs:bits}
   CHANGE_BIT_BITS_ind(n+1,BitsCons (bs,c),bn+1,b,BitsCons (cs,c))
    of CHANGE_BIT_BITS (n,bs,bn,b,cs)

CHANGE_BIT_BITSという命題を定義します。(int,bits,int,bit,bits)と5つも引数がありますが、順番に「ビット列の長さ」「変更前のビット列」「変更するビットの番号（0オリジン）」「置き換えるビット」「変更後のビット列」になります。
大雑把に言うと、CHANGE_BIT_BITSは「"変更前のビット列"のどれか1つのビットを置き換えたものが"変更後のビット列"である」という意味の命題です。

"ビット列の長さ"の引数は要らないような……？
まあええわ（適当）

ビットの調査

dataprop TEST_BIT_BITS (bits,int,bit) =
 | {bn:int}{b:bit}{bs:bits} TEST_BIT_BITS_bas (BitsCons (bs,b),0,b)
     of (BITSLEN (bs,bn))
 | {b,c:bit}{bs:bits}{bn:int}
   TEST_BIT_BITS_ind (BitsCons (bs,c),bn+1,b) of TEST_BIT_BITS (bs,bn,b)

ビット列の何番目が立ってるとか、寝てるとかの状態を表現します。
例えばあるビット列の3番目のビットが立っていれば、TEST_BIT_BITS (bs,3,I)という証明を構成できる（はず）わけです。
逆に、その条件が満たされていてほしいという場合は、関数の引数にTEST_BIT_BITS (bs,3,I)の型を入れておけばよいわけです。

ビット操作関数

で、目的の関数の定義です。

fn {b:bit}{bs:bits}
  changeBitBits {n,bn:nat | bn < n; n < INTBITS} (bits_uint_t (n,bs),uint bn,bit_uint_t b)
  : [bs':bits] (CHANGE_BIT_BITS (n,bs,bn,b,bs') | bits_uint_t (n,bs'))

fn {bs:bits}
  setBitBits {n,bn:nat | bn < n; n < INTBITS} (bits_uint_t (n,bs),uint bn)
  : [cs:bits] (CHANGE_BIT_BITS (n,bs,bn,I,cs) | bits_uint_t (n,cs))

fn {bs:bits}
  clearBitBits {n,bn:nat | bn < n; n < INTBITS} (bits_uint_t (n,bs),uint bn)
  : [bs':bits] (CHANGE_BIT_BITS (n,bs,bn,O,bs') | bits_uint_t (n,bs'))

fn {bs:bits}
  testBitBits {n,bn:nat | bn < n}{n < INTBITS} (bits_uint_t (n,bs),uint bn)
  : [b:bit] (TEST_BIT_BITS (bs,bn,b) | bool (b==I))

勢い余ってビット調査用の関数（testBitBits）も作ってます。

最初の方で書いた必要な関数との対応は、

受け取った数値の、指定されたビットをセットする関数

→ setBitBits

受け取った数値の、指定されたビットをクリアする関数

→ clearBitBits
です。
より汎用的な関数として、changeBitBitsを定義しています。CHANGE_BIT_BITS命題との対応としては、こちらの方が自然かも知れません。

intの最大値

あと、今までもチラチラ見えてた（BITSEQINTの定義とか）と思いますが、int種の最大値についての定義をしてあります。

#define INTBITS				32
#define	INTMAX     		2147483647
#define	INTMAX_HALF		1073741823
#define	UINTMAX_HALF	2147483647

ATSの処理系はint種を扱う時に上限について考慮していないらしく、32ビットで表現できる範囲を越えると簡単に（少なくとも僕が調べたバージョンでは）オーバーフローを起こしてしまいます。
32ビットというのは普通の数としては十分な範囲がありますが、ビット操作を行っていると簡単に越えてしまえる数値です。
悪用を防ぐ手段はないので仕方がないのですが、ケアレスミスで越えてしまった場合に困るかも知れないので、念の為に上記の上限値を使って値の範囲を制限しています。

書き込み許可

次で最後です。

datasort permission = Permit | Prohibit

datasort bit_permission = BitPermission of
  (permission(*of 0*),permission(*of 1*))

datasort bit_permissions = 
 | BitPermsNil of ()
 | BitPermsCons of (bit_permissions,bit_permission)

レジスタの仕様などでは、「このレジスタを書き込む時は必ず0を書き込むこと」など、制限が付いている事がよくあります。
bit_permissionとbit_permissionsは、そういった制限を表現するためのデータ種です。
ビット毎に「0の書き込みの可否」と「1の書き込みの可否」を指定します。ビット毎に4パターンなので、情報量としては4^n(=2^2n)になるわけです。いかにもマシンパワーが必要になりそうな数字ですね！（不安）

stadef BitPermissions8 (b7_0,b7_1,b6_0,b6_1,b5_0,b5_1,b4_0,b4_1,
                        b3_0,b3_1,b2_0,b2_1,b1_0,b1_1,b0_0,b0_1:permission): bit_permissions =
  BitPermsCons (BitPermsCons (BitPermsCons (BitPermsCons (
  BitPermsCons (BitPermsCons (BitPermsCons (BitPermsCons (BitPermsNil,
  BitPermission (b7_0,b7_1)),BitPermission (b6_0,b6_1)),
  BitPermission (b5_0,b5_1)),BitPermission (b4_0,b4_1)),
  BitPermission (b3_0,b3_1)),BitPermission (b2_0,b2_1)),
  BitPermission (b1_0,b1_1)),BitPermission (b0_0,b0_1))

で、１バイト分のbit_permissionsを（なるべく）簡単に宣言するための定義です。
bitsに対してのBits8 と同じようなものです。

書き込み許可→ビットの関係

書き込み許可を表現することはできるようになりましたが、それだけではなんの意味もありません。「その数値は書き込みを許可されているか」判定する仕組みが必要です。
「ビット⇔数値」の対応関係（BITSEQINT）は定義してあるので、あとは「書き込み許可⇔ビット」の関係を定義すれば、芋づる式に「書き込み許可⇔数値」の対応関係を表すことができるようになります。

dataprop BIT_PERMIT_CERTIFICATE (bit_permission,bit) =
 | {p1:permission} BITPERMCERT_0 (BitPermission (Permit,p1),O) of ()
 | {p0:permission} BITPERMCERT_1 (BitPermission (p0,Permit),I) of ()

dataprop BITS_PERMIT_CERTIFICATE (int,bit_permissions,bits) =
 | BITPERMCERTS_NIL (0, BitPermsNil, BitsNil) of ()
 | {n:int}{p:bit_permission}{ps:bit_permissions}{b:bit}{bs:bits}
   BITPERMCERTS_CONS (n+1,BitPermsCons (ps,p),BitsCons (bs,b))
    of (BITS_PERMIT_CERTIFICATE (n,ps,bs),BIT_PERMIT_CERTIFICATE (p,b))

BIT_PERMIT_CERTIFICATEとBITS_PERMIT_CERTIFICATEです。「ビットの許可の証明」みたいなニュアンスでしょうか……？（英語力✕）
対象のビットに応じて、0または1の対応する許可を参照します。例えばBIT_PERMIT_CERTIFICATE (p,b)の値があるという事は、「許可"p"は、ビット"b"を許可している」という意味になります。
BITS_PERMIT_CERTIFICATEは、それを1ビットずつ見ているだけです。

まとめ

疲れた（疲れた）

他にも細々した定義がありますが、端子ドライバの定義では使わない（はずです）ので、ここまでにします。
あとはソースを見て各自読み解いてください（丸投げ）

次回は端子ドライバ本体(Pin.satsとPin.dats)の解説を書く予定です。多分ですが、ここまでが大変だっただけで、すぐに書けるだろうと思います。

ではまた次回。

ATSとはなんじゃ？ という人は

目標