Skip to content

Add Parity loop analysis showcase #85

@Maokami

Description

@Maokami

Goal

Add an end-to-end loop showcase for the Parity domain, mirroring the existing Sign (LoopShowcase) and Interval (WidenShowcase) patterns.

Scope

  • Create Examples/IMP/Programs/ParityLoopShowcase.lean
  • Demonstrate: loop + widening + post-fixpoint soundness with Parity domain
  • Shows that generic analysis code works across domains without modification

Acceptance Criteria

  • Parity loop showcase compiles and proves a concrete property
  • Demonstrates generic domain reuse (same analysis pipeline, different domain)
  • lake build && lake build Tests && lake test pass

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions