PolCert

PolCert provides two user-facing tools:

• polcert: validate a Pluto/OpenScop scheduling result.
• polopt: run a verified polyhedral optimization pipeline on a structured loop fragment.

If you care about the optimizer, start with POLOPT.md. If you already have OpenScop files and only want validation, start with POLCERT.md.

Quick start

Inside the project container, build with:

make clean
opam exec -- make depend
opam exec -- make proof
opam exec -- make -s check-admitted
opam exec -- make extraction
opam exec -- make polopt
opam exec -- make polcert.ini
opam exec -- make polcert
make test

This produces:

• ./polcert <before.scop> <after.scop>
• ./polopt <file.loop>

Two usage stories

1. I already have Pluto before.scop / after.scop

Use polcert. It checks whether the schedule change preserves the polyhedral dependence semantics.

2. I have a loop nest and want the optimizer to do the full pipeline

Use polopt. It parses a .loop file, extracts a polyhedral model, validates the Pluto schedule, generates optimized loop code, and applies verified post-codegen cleanup.

Status

• The verified optimization core lives in driver/PolOpt.v.
• The final optimizer definition is Opt = Opt_prepared.
• The final end-to-end theorem is Opt_correct.
• polcert remains the original validator-only executable and is intentionally unaffected by the polopt work.
• The strict proved-path polopt regression suite currently succeeds on all generated benchmark inputs:
  • total inputs: 62
  • succeeded: 62
  • changed: 52
  • unchanged: 10

CI

GitHub Actions runs the Docker-based clean build and regression flow on every push and pull request. The CI job builds the image from Dockerfile and then runs tools/ci/run_ci.sh, which executes:

• the full Coq proof build
• check-admitted
• extraction
• polcert / polopt builds
• make test
• the strict polopt benchmark suite

Documentation map

• POLCERT.md: validator-only executable, user workflow, and examples.
• POLOPT.md: optimizer pipeline, examples, proof boundary, benchmark behavior, and testing workflow.
• syntax/README.md: textual .loop syntax reference and authoring notes.
• tests/polopt-generated/README.md: generated strict-suite inputs, outputs, and how to inspect changes.
• doc/: additional design notes and analysis.

Project structure

Main mechanized development is in:

• src: extractor, validator, polyhedral semantics, strengthening, prepare-codegen bridge
• polygen: verified code generation and verified cleanup passes
• driver: top-level optimizer definitions and wrappers
• syntax: loop frontend used by polopt
• tests: Pluto suite, generated polopt suite, scripts

Paper

The paper of this mechanization is published at Springer: https://link.springer.com/chapter/10.1007/978-3-031-64626-3_17

BibTeX

@inproceedings{li2024verified,
  title={Verified Validation for Affine Scheduling in Polyhedral Compilation},
  author={Li, Xuyang and Liang, Hongjin and Feng, Xinyu},
  booktitle={Theoretical Aspects of Software Engineering},
  pages={287--305},
  year={2024},
  publisher={Springer}
}

License

See LICENSE.