Copilot-Language
`copilot-theorem`: support bisimulation proofs involving C99 code
Description
One of Copilot's new requirements is to produce proofs that the C code produced matches the semantics.
In order to produce such proofs, we must extend copilot-theorem to enable carrying out proofs by bisimulation.
Type
- Feature: new functionality required to comply with Copilot's requirements.
Additional context
None.
Requester
- Ryan Scott
- Rob Dockins
Method to check presence of bug
Not applicable (not a bug).
Expected result
copilot-theorem defines necessary types and functions to carry out proofs by bisimulation.
Desired result
copilot-theorem defines necessary types and functions to carry out proofs by bisimulation.
Proposed solution
Provide functions needed by proving effort, as well as any new or existing types required by those functions.
Further notes
The actual proofs are implemented as part of a different package, which is currently not released publicly.
Technical Lead: Issue scheduled for fixing in Copilot 3.12.
Fix assigned to @RyanGlScott .
Change Manager: Verified that:
- Solution is implemented:
-
[X] The code proposed compiles and passes all tests. Details: Build log: https://app.travis-ci.com/github/Copilot-Language/copilot/builds/256560808
-
[X] The solution proposed produces the expected result. Details: The code provides a new function and the new types needed by that function are exposed. Verified by manual inspection of the code.
-
- [X] Implementation is documented. Details:
- All new top-level definitions exposed are documented with haddock comments.
- [X] Change history is clear.
- [X] Commit messages are clear.
- [X] Changelogs are updated.
- [X] Examples are updated. Details: No updates needed.
- [X] Required version bumps are evaluated. Details: Bump not needed. API is extended by existing definitions do not change.