Formal big-step operational semantics for CBMC's GOTO IL#582

Open

tautschnig wants to merge 17 commits intomainfrom

tautschnig/goto-semantics

Commits on Mar 16, 2026

feat(Imperative): Add loop evaluation rules to EvalStmt

tautschnig
and
kiro-agent
committed
fix(DetToNondet): Restructure noFuncDecl_preserves_δ for loop rules

tautschnig
and
kiro-agent
committed
feat(Imperative): Add nondet loop semantics and prove DetToNondet loop cases

tautschnig
and
kiro-agent
committed
fix(DetToNondet): Remove all sorry's using unsafe+axiom for termination

tautschnig
and
kiro-agent
committed
feat(GOTO): Add formal big-step operational semantics for CBMC's GOTO IL

tautschnig
and
kiro-agent
committed
feat(GOTO): Add determinism proofs, concrete evaluator, and simulation relation

tautschnig
and
kiro-agent
committed
docs(GOTO): Update TODO list in Semantics.lean to reflect progress

tautschnig
and
kiro-agent
committed
feat(GOTO): Prove all command-level simulation lemmas (0 sorry's)

tautschnig
and
kiro-agent
committed
feat(GOTO): Prove ExecProg determinism for nondet-free programs

tautschnig
and
kiro-agent
committed
feat(GOTO): Add ExecRange, block simulation, and progress statement

tautschnig
and
kiro-agent
committed
feat(GOTO): Prove all progress lemmas and add old() two-state evaluator

tautschnig
and
kiro-agent
committed
feat(GOTO): Prove well-formed program progress (0 sorry's)

tautschnig
and
kiro-agent
committed
feat(GOTO): Add loop semantics via compiled GOTO pattern and old() evaluator

tautschnig
and
kiro-agent
committed
docs(GOTO): Update TODO — loop rules now in Imperative dialect

tautschnig
and
kiro-agent
committed
feat(GOTO): End-to-end simulation theorem (all TODO items complete)

tautschnig
and
kiro-agent
committed
fix: Address Copilot review comments

tautschnig
and
kiro-agent
committed
fix: Remove trailing whitespace in DetToNondetCorrect.lean

tautschnig
and
kiro-agent
committed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Formal big-step operational semantics for CBMC's GOTO IL#582

Formal big-step operational semantics for CBMC's GOTO IL#582
tautschnig wants to merge 17 commits intomainfrom
tautschnig/goto-semantics

Commits on Mar 16, 2026

feat(Imperative): Add loop evaluation rules to EvalStmt

fix(DetToNondet): Restructure noFuncDecl_preserves_δ for loop rules

feat(Imperative): Add nondet loop semantics and prove DetToNondet loop cases

fix(DetToNondet): Remove all sorry's using unsafe+axiom for termination

feat(GOTO): Add formal big-step operational semantics for CBMC's GOTO IL

feat(GOTO): Add determinism proofs, concrete evaluator, and simulation relation

docs(GOTO): Update TODO list in Semantics.lean to reflect progress

feat(GOTO): Prove all command-level simulation lemmas (0 sorry's)

feat(GOTO): Prove ExecProg determinism for nondet-free programs

feat(GOTO): Add ExecRange, block simulation, and progress statement

feat(GOTO): Prove all progress lemmas and add old() two-state evaluator

feat(GOTO): Prove well-formed program progress (0 sorry's)

feat(GOTO): Add loop semantics via compiled GOTO pattern and old() evaluator

docs(GOTO): Update TODO — loop rules now in Imperative dialect

feat(GOTO): End-to-end simulation theorem (all TODO items complete)

fix: Address Copilot review comments

fix: Remove trailing whitespace in DetToNondetCorrect.lean