[WIP] Remove sorry warnings via Kiro-generated proofs#452

Draft

tautschnig wants to merge 14 commits intomainfrom

tautschnig/no-sorry

Commits on Feb 19, 2026

Prove EvalBlockRefinesContract and EvalStmtRefinesContract via strong induction
tautschnig
committed
Partially prove Procedure.typeCheckWF (5 of 9 fields)
tautschnig
committed
Prove EvalCommandRefinesContract by adding modifies well-formedness premise
tautschnig
committed
Prove EvalExpressionIsDefined by adding definedness propagation to WellFormedCoreEvalCong
tautschnig
committed
Refactor WF properties: remove unused wfloclnd, move glob to WFProgramProp
tautschnig
committed
Remove unprovable WF fields that require identifier resolution
tautschnig
committed
Remove globVars from WFProgramProp, making Program.typeCheckWF sorry-free
tautschnig
committed
Document proof strategy for EvalCallBodyRefinesContract
tautschnig
committed
Expand EvalCallBodyRefinesContract proof structure
tautschnig
committed
Prove EvalBlockFrameCondition (frame condition for block evaluation)
tautschnig
committed
Restructure EvalCallBodyRefinesContract with custom contract store
tautschnig
committed
Prove EvalBlockFrameConditionDefined and use in main theorem
tautschnig
committed
Prove ReadValues transfer and reduce to 2 sorry's
tautschnig
committed
Eliminate all sorry's from EvalCallBodyRefinesContract
tautschnig
committed