# CStar Examples

**Repository Path**: cstarlang/cstar_examples

## Basic Information

- **Project Name**: CStar Examples
- **Description**: No description available
- **Primary Language**: Unknown
- **License**: MIT
- **Default Branch**: main
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 0
- **Forks**: 0
- **Created**: 2025-08-07
- **Last Updated**: 2026-08-02

## Categories & Tags

**Categories**: Uncategorized

**Tags**: None

## README

# CStar examples and user-side proof libraries

This repository contains executable verification examples together with the
user-side proof libraries they share. The directories are organized by role:

- `proof/` is the `cstar_stdlib` submodule and contains the stable foundational
  proof API.
- `userlib/` contains recoverable proof probes, QCP adapters, and operational
  symbolic-state transformations. Examples may depend on it; it never depends
  on an example.
- `array/` contains the canonical `data_at` array library, reusable array PSI
  units, and verified algorithms. The older `array_at` model remains in the
  same directory under explicit `_legacy` names; see `array/LEGACY.md`.
- `tutorial/` is the numbered introductory corpus; `bst/` and `psi_examples/`
  are program galleries.
- `tests/` contains positive, negative, and obligation-producing regression
  fixtures rather than tutorial material.
- `migrations/` groups case studies by their source verifier: LiveVerif,
  VeriFast, and VST, including the VST `memmgr` allocator.
- `docs/` records cross-cutting proof and toolchain behavior.

The intended dependency direction is:

```text
proof -> userlib -> domain libraries / PSI units -> examples and migrations
```

Examples, migrations, and tutorials are leaves and must not be required by a
public library. A model or helper remains example-private until it has at least
two independent clients.

- Run `cstarc init` to initialize the workspace!
- Run `cstarc server` before doing any verification!
- Run `cstarc verify path/to/file.c` to verify a single file.
- Run `./verify_all.sh` to verify every `*.c` in the project, or
  `./verify_all.sh array bst` to verify only the given directories/files.
  It passes when every file reports no outstanding verification conditions,
  except for examples carrying an explicit `verify_all: expect-vcs=N` teaching
  expectation.

CStar standard proof libraries live in `proof/`, which is a git submodule of
[`cstar_stdlib`](https://gitee.com/cstarlang/cstar_stdlib.git) (branch
`main`). Clone with `git clone --recurse-submodules`, or after a plain
clone run `git submodule update --init --recursive`.

Recoverable HOL probes live in `userlib/proof/`; the QCP assertion adapter
lives in `userlib/qcp/`. The operational proof library and shared proof-pattern
helpers live in `userlib/operational/`; see
the [API specification](userlib/operational/README.md) and the
[operational-reasoning guide](docs/OPERATIONAL_REASONING.md). Known tool and
proof-engineering pitfalls are indexed in
[`docs/QUIRKS_AND_PITFALLS.md`](docs/QUIRKS_AND_PITFALLS.md). Run
`./tests/test_operational_patterns.sh` to check malformed-pattern diagnostics.

## Notes

Things that are easy to trip over, learned the hard way.

### Verification runs must be sequential

`cstarc verify` talks to a single HOL server, so two verifications cannot run at
the same time to the same server. `verify_all.sh` is sequential by design.
If you want parallel runs, start multiple servers at different ports and use
`cstarc verify --port <N>` to specify the port number.

### A header-only edit does not trigger a recompile

`cstarc verify` reuses the compiled object for a `*.c` file whose timestamp has
not changed. Edit a header, and the dependent `*.c` files are verified against
the *old* header, so a green run can be reporting on code that no longer exists
(and a spurious failure can outlive the fix). After changing a `*.h`, `touch`
the `*.c` files that include it before verifying.

### Library layout: the header declares, the client requires

The `userlib`, domain, and migration libraries follow one convention:

- the header (`array.h`, `bst.h`) `#include`s its dependency's header and
  `#require`s that dependency's `.c`, then declares `extern` theorems, `PROOF`
  prototypes, C structs, and function contracts;
- the implementation (`array.c`, `bst.c`) `#include`s its *own* header;
- the client `#include`s the header **and** `#require`s the implementation;
- a header must not `#require` its own `.c`.

```c
#include "bst/lib/bst.h"
#require "bst/lib/bst.c"
```

### Nix usage

The whole cstar toolchain is available via Nix. Due to the inflexibility of
cstarc configuration, after firstly running `nix develop` (or any update on flake files),
`initCFlags` must be executed once to provide the necessary flags. Then all cstar
functionalities should work as expected. (Hint: add `cstar_old.toml` to `.git/info/exclude`
and use `git update-index --skip-worktree cstar.toml` to avoid committing them.)