Changelog

• ca20ac8 Merge pull request #19 from Kuniwak/shorten-isabelle-livelock-proof
• b215e04 Structural: shorten the Isabelle livelock proof with a measure
• e2ad4ad Merge pull request #18 from Kuniwak/livelockfree-obligation-ir
• 3592792 Docs: prove the Lean obligation for the same example
• cefba34 Structural: tidy the Livelock_Obligation predicate bodies
• 55aa0a5 Structural: align the inductive layout with the other declarations
• 4be2214 STRUCTUAL: Prove Livelock_Obligation example
• 9f16be7 Docs: regenerate the example obligation with reachability
• b427840 Docs: describe the reachability restriction
• d4b6b2d Structural: drop the now-identity predicate filter
• f6bb8f4 Behavioral: restrict the lean obligation to reachable states
• 4ec0fb5 Behavioral: restrict the isabelle obligation to reachable states
• dea6101 Structural: parameterise the transition-relation writer by name
• d86db66 Behavioral: order derived states deterministically
• 9c51fa6 Behavioral: refresh the csdfparse goldens
• e7824f1 Docs: describe the hash-named predicates the backends emit
• 2c7e954 Behavioral: follow the current IR in the command tests
• ae37435 Behavioral: rebuild the lean backend on the current IR
• 71e6ae4 Behavioral: pin the ir-json wire form and stop escaping predicate text
• 5588e27 Behavioral: give the init predicate the start state's variables
• 4b1c364 Behavioral: follow the csdf type changes in animation
• 77eb2dc Structural: lift the predicate-ID spelling into obligationir
• add05da Structural: follow the renamed csdf and obligationir API
• 86392cd Structural: drop dead code in obligationir
• 2b12326 Behavioral: Fix isabelle theorem
• 2c1c947 tmp
• 8cd8e51 Behavior: make ir/target clean
• 649b98d Behavioral: omit the proof obligation when structurally livelock free
• e9a556f Docs: note JSON value typing in the obligation skeletons
• bed2c45 Behavioral: type isabelle state vars with a JSON datatype
• a7e9f61 Behavioral: type lean state vars with a JSON datatype
• 9523df0 Docs: make csdflivelockfree -target the primary path for prover output
• 83d038e Behavioral: add -target to csdflivelockfree
• da4081b Structural: extract csdf/obligationir/target dispatcher
• ad7d2d4 Docs: document the obligationirc IR compiler
• e793238 Behavioral: add obligationirc command
• d36de67 Behavioral: emit a placeholder type for untyped state variables
• bc6f8ce Behavioral: add csdf/obligationir/isabelle compiler backend
• c730714 Behavioral: add csdf/obligationir/lean compiler backend
• 44809fd Behavioral: add csdf/obligationir/json compiler backend
• fb6dadb Structural: move obligation IR into csdf/obligationir package
• 4e00f0a Docs: describe csdflivelockfree's proof-obligation IR output
• 5d3cd5f Structural: remove unused RenderLivelock witness renderer
• 41e7f4c Behavioral: csdflivelockfree emits the obligation IR and exits 0
• 416fbda Behavioral: add livelock proof-obligation IR builder
• a8dafd9 Structural: record source line numbers on Edge and StartEdge