• RustBeltのlambdarustを拡張して、より現実に即した操作的意味論を与えている(Radium)

    • borrow/reborrowが扱える

    • MIRとの対応からCFGベースの形式言語Radiumを形式化

  • trait/trait objectなどにはまだ明示的に対応していないが検証時にLayoutを与えることで、ポリモーフィックな関数も扱える

  • 定理証明ベースでありながら、自動化のためのrefinement type systemがある

    • Coq上の型との対応関係を一部自動証明してくれる

    • cf. refinedc

検証ツールについて

  • RustのMIRをCoq/Irisを使って構築した言語に変換して、性質の証明を行う

  • Rustのコードを変換するフロントエンドが、かなり未成熟で対応していないシンタックスがおおい

  • サンプルは概ね動かせた

  • nixのdevshell内で、duneにCOQPATHがうまく渡っていない

    • workaround: shellHookに以下を追記

      • export COQPATH=${packages.theories.outPath}/lib/coq/${coq.version}/user-contrib:''$COQPATH

  • 標準ライブラリの形式化

    • 現状ほぼされていないが、枠組みはありVecやOption,Resultなどの空の実装にspecをつけている

    • プリミティブ型とその操作に関する形式仕様を作っていきたいが、そのための枠組みがあるかは不明

Allocator APIの形式化

  • shims.v に alloc / dealloc の関数・仕様定義がある

  • alloc: 事後条件として freeable ghost stateを作り、開放可能な領域をマークする

  • caesium/ghost_state.v に freeable / alloc_* などのアロケーションの状態を表す述語が定義されている

  • RustのAllocator APIやGlobalAllocの形式化ではなく、mallocっぽいAPIのアロケータの定義(alloc_alloc)について caesium/ghost_state.v の述語で与えた仕様を証明している

    • alloc::Layout を取るようなshimが定義されている

tupleの扱い

  • shims.v / tuple{n}_{ty|rt}

  • hlist に place_rfn {Coqの型} とすれば良いことがわかった

array workaround

  • option 1: フロントエンドで array_t の表現に変換する

  • option 2: Radiumにarrayに関する型付要素アクセス操作を追加する

    • *mut T ベースの配列(array_t)に関する型付要素アクセスはできそう cf. typed_array_access ( rust_typing/arrays.v )

  • op_type に要素アクセスを追加するには

    • type.v / _ty_has_op_type で操作後のメモリ表現の変化を表現

    • syntactic type: ArraySynType

  • MIRにおけるarray https://rustc-dev-guide.rust-lang.org/mir/index.html#valtrees

raw pointer dereferenceのための事前条件

  • ptr::read では(コメントアウトされている強い条件)

    • (l ◁ₗ[π, Owned false] PlaceIn vs @ (◁ value_t (st_of T_ty)) ∗ vs ◁ᵥ{π} r @ T_ty

Definition type_of_ptr_read `{!typeGS Σ} (T_rt : Type) (T_st : syn_type) :=
  fn(∀ () : 0 | ( *[T_ty]) : [(T_rt, T_st)] | (l, r) : (loc * T_rt), (λ ϝ, []);
      l :@: alias_ptr_t; λ π,
      (l ◁ₗ[π, Owned false] PlaceIn vs @ (◁ value_t (T_ty.(ty_syn_type)))) ∗
      vs ◁ᵥ{π} r @ T_ty
  )
    → ∃ vs : val, vs @ value_t (T_ty.(ty_syn_type)); λ π,
      (l ◁ₗ[π, Owned false] PlaceIn vs @ (◁ value_t (T_ty.(ty_syn_type)))) ∗
      vs ◁ᵥ{π} r @ T_ty
.

記法

  • l ◁ₗ[π, Owned false] v @ (◁ T_ty)

  • vs ◁ᵥ{π} r @ T_ty