← Policy gallery

ipl_cert_model_valid

fix-certification conformance pure_temporal iplimandrafixfix-certificationformal-model

The IPL model must type-check and be free of errors before it is used to generate tests or simulators — only a valid model is guaranteed to produce a functioning implementation.

Formula

G(GenerateTests → P(ipl_model_valid))

Hover any operator or symbol for what it means.

Why it matters

ROE Formalization in IPL. IPL's guarantee is that an error-free model can generate a functioning implementation, simulator and test suite. Generating from a model that still has type or validity errors produces artefacts that do not faithfully represent the ROE.

Examples

passes IPL model type-checks clean → GenerateTests

fails GenerateTests run against an IPL model that still has unresolved type errors

Use it

ponens policies add ipl_cert_model_valid --into ./trace.json
ponens trace check ./trace.json