microsoft/FStarDataSet

---
license: cdla-permissive-2.0
task_categories:
- text-generation
- text2text-generation
- "other"
tags:
- code
- fstar
- popai
pretty_name: PoPAI-FStarDataSet
size_categories:
- 10K<n<100K
language:
- code
- fst
---

# 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}
}
```