FStarDataSet

# Proof Oriented Programming with AI (PoPAI) - FStarDataSet

This dataset contains programs and proofs in [F* proof-oriented programming language](https://fstar-lang.org/).
The data, proposed in [Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming](https://arxiv.org/pdf/2405.01787),
is an archive of source code, build artifacts, and metadata assembled from eight different F⋆-based open source projects on GitHub.

## Primary-Objective
This dataset's primary objective is to train and evaluate Proof-oriented Programming with AI (PoPAI, in short). Given a specification of a program and proof in F*,
the objective of a AI model is to synthesize the implemantation (see [below](#usage) for details about the usage of this dataset, including the input and output).

## Data Format
Each of the examples in this dataset are organized as dictionaries with the following schema
```json
{
"file_name": <str: Name of the file>,
"name": <str: name of the example, can be used to uniquely identify the example>,
"original_source_type": <str: actual source type, to be used for type checking>,
"source_type": <str: modified source type, to be used to formulate prompt>,
"source_definition": <str: target definition>,
"source": <dict: contains metadata about the source of this example, including project_name, git url, git sha, etc.>,
"source_range": <dict: metadata containing start and end lines and columns of this definition in the source file>,
"file_context": <str: extracted file context upto the point of current definition>,
"dependencies": <dict: build dependencies for this file>,
"opens_and_abbrevs": <list[dict]: List of opened modules and abbreviated modules in the file, necessary for evaluation.>,
"vconfig": <dict: SMT solver flags for this definition>,
"interleaved": <bool: whether this definition is interleaved from the interface file>,
"verbose_type": <str: the verbose type of this definition as resolved by the type checker>,
"effect": <str: effect>,
"effect_flags": <list[str]: any effect flags>,
"mutual_with": <list: if this definition is mutually recursive with another, list of those names>,
"ideal_premises": <list[str]: Other definitions that are used in the ground truth definition>,
"proof_features": <list[str]>,
"is_simple_lemma": <bool/null>,
"is_div": <bool: if this definition has the divergent effect>,
"is_proof": <bool>,
"is_simply_typed": <bool>,
"is_type": <bool/null>,
"partial_definition": <str>,
"completed_definiton": <str>,
"isa_cross_project_example": <bool: if this example belongs to the cross-project evaluation set>
}
```

# Usage
To use this dataset with [`datasets`](https://pypi.org/project/datasets/),
```python
from datasets import load_dataset

data = load_dataset("microsoft/FStarDataSet")
train_data = data["train"]
eval_data = data["validation"]
test_data = data["test"]

intra_project_test = test_data.filter(lambda x: x["isa_cross_project_example"] == False)
cross_project_test = test_data.filter(lambda x: x["isa_cross_project_example"] == True)
```

## Input
The primary input for generating F* definition is **`source_type`**.
All other information in an example may be used directly or to derive an input except
**`source_definition`**, **`ideal_premises`**, and **`completed_definiton`**.

## Output
The primary output is **`source_definition`**, which is the ground truth definition, that can be evaluated with the [proof checker](#evaluation-on-this-dataset).
The **`completed_definiton`** may be used as ground truth when a model is used as a text completion setting (though the evaluator does not support evaluation in this setting).
In addition, **`ideal_premises`** may be used for evaluating premise selection models.

# Evaluation on this dataset
Generated F* definitions should be evaluated the proof checker tool from [https://github.com/FStarLang/fstar_dataset/releases/tag/eval-v1.0](https://github.com/FStarLang/fstar_dataset/releases/tag/eval-v1.0).
Download the source code and the `helpers.zip` file from the release.

## Troubleshooting
The attached binaries in the evaluator (i.e., `fstar.exe` and `z3`) are built on
**`Ubuntu 20.04.6 LTS (GNU/Linux 5.4.0-189-generic x86_64)`**, **`gcc (Ubuntu 9.4.0-1ubuntu1~20.04.2)`**, **`OCaml 4.12.0`**.
If any of the binaries do not work properly, build F* from [commit: f3b4db2ebce90020acbbbe1b4ea0d05d3e69ad6c](https://github.com/FStarLang/FStar/commit/f3b4db2ebce90020acbbbe1b4ea0d05d3e69ad6c)
from the [F* repository](https://github.com/FStarLang/FStar), using the [installation guide](https://github.com/FStarLang/FStar/blob/master/INSTALL.md).

# Data Source
The raw data in this project are collected from eight open-source F* repositories on GitHib
1. [FStar](https://github.com/FStarLang/FStar): The F⋆ compiler itself, including its standard library and examples.
2. [Karamel](https://github.com/FStarLang/karamel): A transpiler from a subset of F⋆ called Low* to C, including libraries to work with a model of C types and control structures, e.g., for- and while-loops.
3. [EverParse](https://github.com/project-everest/everparse): A parser generator for binary formats, used in various large scale systems, e.g., the Windows kernel.
4. [HACL*](https://github.com/hacl-star/hacl-star): A library of verified cryptographic algorithms, including ValeCrypt, a library of verified assembly code, as well as EverCrypt, a cryptographic provider, including code deployed in Linux, Firefox, and Python.
5. [Merkle-tree](https://github.com/hacl-star/merkle-tree): A verified, incremental Merkle tree, designed for use in Azure CCF, a confidential computing system.
6. [Steel](https://github.com/FStarLang/steel): A concurrent separation logic library, with proofs of data structures and concurrency primitives.
7. [miTLS-F*](https://github.com/project-everest/mitls-fstar): A partially verified reference implementation of the TLS protocol.
8. [EverQuic-Crypto](https://github.com/project-everest/everquic-crypto): A verified implementation of header and packet protection for the QUIC protocol.

# Limitations
**TDB**

# Citation
```
@inproceedings{chakraborty2024towards,
title={Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming},
author={Chakraborty, Saikat and Ebner, Gabriel and Bhat, Siddharth and Fakhoury, Sarah and Fatima, Sakina and Lahiri, Shuvendu and Swamy, Nikhil},
booktitle={Proceedings of the IEEE/ACM 47th International Conference on Software Engineering (To Appear)},
pages={1--12},
year={2025}
}
```

# 面向证明的人工智能编程（Proof Oriented Programming with AI，简称PoPAI）——F*数据集
本数据集包含基于[F*面向证明编程语言（F* proof-oriented programming language）](https://fstar-lang.org/)的程序与证明。该数据集由论文《Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming》（https://arxiv.org/pdf/2405.01787）提出，其内容是从GitHub上8个基于F*的开源项目中收集的源代码、构建产物与元数据的归档集合。

## 核心目标
本数据集的核心目标是训练与评估面向证明的人工智能编程（简称PoPAI）。给定F*语言中的程序与证明规范，人工智能模型的目标是合成对应的实现（关于该数据集的使用细节，包括输入与输出格式，请参见下文【使用方法】小节）。

## 数据格式
本数据集的每个示例均采用如下结构的字典组织：
json
{
"file_name": <str: 文件名>,
"name": <str: 示例名称，可用于唯一标识该示例>,
"original_source_type": <str: 用于类型检查的原始源类型>,
"source_type": <str: 用于构建提示词的修改后源类型>,
"source_definition": <str: 目标定义>,
"source": <dict: 包含该示例来源元数据的字典，包括项目名称、Git URL、Git SHA等>,
"source_range": <dict: 包含该定义在源文件中起始与终止行、列的元数据>,
"file_context": <str: 提取至当前定义位置的文件上下文>,
"dependencies": <dict: 该文件的构建依赖项>,
"opens_and_abbrevs": <list[dict]: 文件中已导入的模块与缩写模块列表，为评估所需>,
"vconfig": <dict: 该定义的SMT求解器标志>,
"interleaved": <bool: 该定义是否从接口文件中穿插提取>,
"verbose_type": <str: 类型检查器解析得到的该定义的详细类型>,
"effect": <str: 效应类型>,
"effect_flags": <list[str]: 效应标志列表>,
"mutual_with": <list: 若该定义与其他定义互为递归，则列出这些定义的名称>,
"ideal_premises": <list[str]: 真实定义中所使用的其他定义>,
"proof_features": <list[str]: 证明特征列表>,
"is_simple_lemma": <bool/null: 是否为简单引理，可为空>,
"is_div": <bool: 该定义是否包含发散效应>,
"is_proof": <bool: 是否为证明>,
"is_simply_typed": <bool: 是否为简单类型化>,
"is_type": <bool/null: 是否为类型定义，可为空>,
"partial_definition": <str: 部分定义>,
"completed_definiton": <str: 完整定义>,
"isa_cross_project_example": <bool: 该示例是否属于跨项目评估集>
}

## 使用方法
若要结合[`datasets`](https://pypi.org/project/datasets/)库使用本数据集，可参考如下代码：
python
from datasets import load_dataset

data = load_dataset("microsoft/FStarDataSet")
train_data = data["train"]
eval_data = data["validation"]
test_data = data["test"]

intra_project_test = test_data.filter(lambda x: x["isa_cross_project_example"] == False)
cross_project_test = test_data.filter(lambda x: x["isa_cross_project_example"] == True)

## 输入
生成F*定义的主要输入为**`source_type`**。示例中的所有其他信息均可直接使用或用于推导输入，但**`source_definition`**、**`ideal_premises`**与**`completed_definiton`**除外。

## 输出
主要输出为**`source_definition`**，即可通过[证明检查工具](#本数据集上的评估)进行验证的真实定义。当模型用于文本补全任务时，**`completed_definiton`**可作为真实标签（尽管评估器暂不支持该场景下的评估）。此外，**`ideal_premises`**可用于评估前提选择模型。

## 本数据集上的评估
生成的F*定义应使用来自https://github.com/FStarLang/fstar_dataset/releases/tag/eval-v1.0 的证明检查工具进行评估。请从该发布页下载源代码与`helpers.zip`文件。

## 故障排查
评估器中附带的二进制文件（即`fstar.exe`与`z3`）基于**`Ubuntu 20.04.6 LTS (GNU/Linux 5.4.0-189-generic x86_64)`**、**`gcc (Ubuntu 9.4.0-1ubuntu1~20.04.2)`**与**`OCaml 4.12.0`**构建。若二进制文件无法正常运行，请根据[F*仓库](https://github.com/FStarLang/FStar)的提交[f3b4db2ebce90020acbbbe1b4ea0d05d3e69ad6c](https://github.com/FStarLang/FStar/commit/f3b4db2ebce90020acbbbe1b4ea0d05d3e69ad6c)，并参考[安装指南](https://github.com/FStarLang/FStar/blob/master/INSTALL.md)自行编译F*。

## 数据来源
本项目的原始数据收集自GitHub上的8个开源F*仓库：
1. [FStar](https://github.com/FStarLang/FStar)：F*编译器本身，包括其标准库与示例。
2. [Karamel](https://github.com/FStarLang/karamel)：将F*子集Low*转换为C语言的转译器，包括用于处理C类型与控制结构（如for、while循环）模型的库。
3. [EverParse](https://github.com/project-everest/everparse)：面向二进制格式的解析器生成器，已应用于各类大规模系统，如Windows内核。
4. [HACL*](https://github.com/hacl-star/hacl-star)：经过验证的加密算法库，包括ValeCrypt（经过验证的汇编代码库）与EverCrypt（加密提供程序，其代码已部署于Linux、Firefox与Python中）。
5. [Merkle-tree](https://github.com/hacl-star/merkle-tree)：经过验证的增量Merkle树，专为Azure CCF（机密计算系统）设计。
6. [Steel](https://github.com/FStarLang/steel)：并发分离逻辑库，包含数据结构与并发原语的证明。
7. [miTLS-F*](https://github.com/project-everest/mitls-fstar)：部分经过验证的TLS协议参考实现。
8. [EverQuic-Crypto](https://github.com/project-everest/everquic-crypto)：经过验证的QUIC协议头部与数据包保护实现。

## 局限性
**待补充（TDB）**

## 引用

@inproceedings{chakraborty2024towards,
title={Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming},
author={Chakraborty, Saikat and Ebner, Gabriel and Bhat, Siddharth and Fakhoury, Sarah and Fatima, Sakina and Lahiri, Shuvendu and Swamy, Nikhil},
booktitle={Proceedings of the IEEE/ACM 47th International Conference on Software Engineering (To Appear)},
pages={1--12},
year={2025}
}