FHIR-Fly

Requirements

• Ply (https://www.dabeaz.com/ply/ply.html)

• PVS (https://github.com/SRI-CSL/pvs)

  • SBCL (https://github.com/sbcl/sbcl)
  • Yices2 (https://github.com/SRI-CSL/yices2)

Installation

The following install script installs all dependencies (listed above):

make install

This install process is designed to be run on a Mac with Homebrew installed. On other systems, the Docker version of FHIR-Fly (see "Docker Container" below) is preferred.

Components/Directory Structure

• ./jslt_parser/ defines a Python/Ply parser for JSLT and a walker to emit PVS specifications.
• ./jslt_pvs/ defines PVS embeddings of JSON datatypes and JSLT.

Documentation

See doc/architecture.pdf for a broad overview of the FHIR-Fly system and its design goals.

Tutorial

Verification Oracle

For given formats $A$ and $B$ and a transform $f : A \rightarrow B$, we can verify that $f(a) : B$ for any $a : A$.

The typechecking judgement $e : \tau$ is quite strong, in that constraints can be arbitrarily complex, requiring rich decision procedures reasoning in the combination of datatypes, strings, booleans, and arithmetic.

For example, let $A$ be the following schema (examples/ex1/A_schema.json):

{
  ...
  "properties": {
    "first_name": {
      "description": "Human First Name",
      "type": "string"
    },
    "last_name": {
      "description": "Human Last Name",
      "type": "string"
    }
  }
}

Let $B$ be the following schema (examples/ex1/B_schema.json):

{
  ...
  "properties": {
    "full_name": {
      "description": "Human Full Name (`First Name` followed by `Last Name`)",
      "type": "string"
    }
  }
}

and let $a$ be the following JSON object (examples/ex1/foo_bar_a.json):

{
  "first_name": "foo",
  "last_name": "bar"
}

Our JSLT transform would look like the following (examples/ex1/A_B.jslt):

  {
    "full_name": join([.first_name, " ", .last_name], "")
  }

python3 main.py --input_schema examples/ex1/A_schema.json   \
                --transform examples/ex1/A_B.jslt           \
                --output_schema examples/ex1/B_schema.json  \
                --instance_name AB                          \
                --pvs_location ./local-pvs/                    

This generates all the necessary verification conditions and saves it in [instance_name].pvs (here, AB.pvs), alongside a verification strategy that tells PVS how to discharge the conditions.

At the moment, we utilize a custom decision procedure jslt-verify-interpret that expands hard-coded forms and applies PVS's internal grind procedure. Eventually, this would be swapped out with the Yices2 SMT solver and specialized decision procedures for strings/regular expressions.

To run the verifier,

cd ./test/ && ./PVS/pvs -batch -q -l AB.el

Now, the verification script will either print out Verification succeeded! or Verification failed! depending on whether the decision procedures were able to establish validity of the verification conditions.

To wrap both steps into a single command, run the tool with the extra flag --verify:

python3 main.py --input_schema examples/ex1/A_schema.json  \
                --transform examples/ex1/A_B.jslt          \
                --output_schema examples/ex1/B_schema.json \
                --instance_name AB                         \
                --pvs_location ./local-pvs/                \
                --verify                                   \

Docker Container

Alternately, you can run FHIR-Fly in a Docker container. To build the container, use:

./build_docker.sh

and to run it:

./run_docker.sh --input_schema workspace/ex1/A_schema.json \
                --transform workspace/ex1/A_B.jslt \
                --output_schema workspace/ex1/B_schema.json \
                --instance_name AB \
                --verify

The run_docker.sh script automatically mounts ./workspace as ./workspace inside the container, examples/ex1 as workspace/ex1, and ./results as ./results. It also handles the PVS location, leaving you to specify only the command line arguments that differ from run to run.

Direct PVS Verification (pvs_main.py)

In addition to the JSLT-based workflow described above, FHIR-Fly provides a direct PVS verification tool (pvs_main.py) that works directly with hand-written PVS theories without requiring JSLT as an intermediate language.

Overview

• pvs_main.py: Command-line tool for direct PVS verification
  • prompt-transform subcommand: Generate LLM prompt for synthesizing PVS transform functions
  • prompt-constraints subcommand: Generate LLM prompt for synthesizing PVS constraint functions
  • generate subcommand: Generate verification files (dry-run)
  • verify subcommand: Generate and run PVS verification
• run_tests.py: Automated test runner for all examples
• Docker scripts: Containerized versions of the above tools

Usage

LLM-Assisted Transform and Constraints Synthesis

The prompt-transform and prompt-constraints subcommands generate comprehensive prompts for an LLM to synthesize PVS transform and constraint functions. This is useful for automatically generating PVS theories from schema specifications.

Transform Synthesis:

# Generate transform prompt to stdout
python3 pvs_main.py prompt-transform \
  --input-schema examples/ex2/A_schema.json \
  --output-schema examples/ex2/B_schema.json

# Save transform prompt to a file with example
python3 pvs_main.py prompt-transform \
  --input-schema examples/ex5/Drug_schema.json \
  --output-schema examples/ex5/Prescription_schema.json \
  --example-dir examples/ex3 \
  --output-file drug_transform_prompt.txt

The transform prompt includes:

• Input and output JSON schemas
• PVS jsondata API documentation
• Transform structure template with correct syntax
• Optional example transform for reference
• Detailed instructions for the LLM

Constraints Synthesis:

# Generate constraints prompt to stdout
python3 pvs_main.py prompt-constraints \
  --input-schema examples/ex2/A_schema.json \
  --output-schema examples/ex2/B_schema.json \
  --theory-name A_B_constraints

# Save constraints prompt to a file with example
python3 pvs_main.py prompt-constraints \
  --input-schema examples/ex5/Drug_schema.json \
  --output-schema examples/ex5/Prescription_schema.json \
  --theory-name Drug_Prescription_constraints \
  --example-dir examples/ex3 \
  --output-file drug_constraints_prompt.txt

The constraints prompt includes:

• Input and output JSON schemas
• Explanation of requires (precondition) and ensures (postcondition) functions
• PVS logical operators and JSON predicates
• Complete scaffolding with function signatures
• Optional example constraints for reference
• LLM only needs to fill in function bodies

Basic Usage (Local)

# Generate verification files only
python3 pvs_main.py generate \
  --transform examples/ex2/A_B.pvs \
  --constraints examples/ex2/A_B_constraints.pvs \
  --input-schema examples/ex2/A_schema.json \
  --output-schema examples/ex2/B_schema.json \
  --pvs ~/git/PVS/pvs \
  --output results

# Generate and verify
python3 pvs_main.py verify \
  --transform examples/ex2/A_B.pvs \
  --constraints examples/ex2/A_B_constraints.pvs \
  --input-schema examples/ex2/A_schema.json \
  --output-schema examples/ex2/B_schema.json \
  --pvs ~/git/PVS/pvs \
  --output results

# Show full PVS log on failure
python3 pvs_main.py verify ... --verbose

Using Environment Variables

Set PVS_PATH to avoid specifying --pvs every time:

export PVS_PATH=~/git/PVS/pvs
python3 pvs_main.py verify \
  --transform examples/ex2/A_B.pvs \
  --constraints examples/ex2/A_B_constraints.pvs \
  --input-schema examples/ex2/A_schema.json \
  --output-schema examples/ex2/B_schema.json

Running Tests

Run all PVS-based examples at once:

# Local execution
python3 run_tests.py

# With custom PVS path
PVS_PATH=~/git/PVS/pvs python3 run_tests.py

The test runner automatically discovers all valid test cases in examples/ (excluding JSLT-based ex1) and reports pass/fail status with colored output.

Docker Usage

Building the Docker Image

# Normal build (uses cache)
./build_docker.sh

# Clean build (no cache, use after updating dependencies)
./build_docker.sh clean

Running pvs_main.py in Docker

./run_pvs_docker.sh verify \
  --transform examples/ex2/A_B.pvs \
  --constraints examples/ex2/A_B_constraints.pvs \
  --input-schema examples/ex2/A_schema.json \
  --output-schema examples/ex2/B_schema.json \
  --verbose

The run_pvs_docker.sh script automatically:

• Sets the correct PVS path for the container
• Mounts necessary directories (workspace/, examples/, results/)
• Handles platform requirements (amd64 for PVS/Yices)

Running Tests in Docker

./run_tests_docker.sh

File Structure for pvs_main.py

Each example directory should contain:

• A_B.pvs - Transform theory (theory name must match filename)
• A_B_constraints.pvs - Constraints theory with requires and ensures functions
• A_schema.json - Input JSON schema
• B_schema.json - Output JSON schema

Important: The theory name inside each .pvs file must match the filename (without extension). For example, A_B.pvs must contain A_B: THEORY, not A_B_transform: THEORY.

Helper Functions

The jsondata theory in jslt_pvs/jsltlib/ provides helper functions:

• json_get_key(obj, key) - Retrieve value from JSON object by key
• json_get_key_rec(obj, key, i) - Recursive implementation

Import with:

IMPORTING jsltlib@jsondata

Example: ex2

See examples/ex2/ for a complete working example that demonstrates:

• Simple string concatenation transform
• Schema validation
• Basic constraints (TRUE requires, jdict? ensures)