Update CakeML AM Copland-related datatypes

ku-sldg / attestation-testbed

BSD 3-Clause "New" or "Revised" License

0 stars 0 forks source link

Update CakeML AM Copland-related datatypes #32

Closed ampetz closed 1 month ago

ampetz commented 2 years ago

Update cakeml Copland-related datatypes (phrases, evidence, etc.) to be consistent with the Coq datatypes defined here.

Verification-only artifacts like event traces (Ev type in Coq) not needed in cakeml.

Durbatuluk1701 commented 1 month ago

This has been completed as we have over time managed to hoist a great deal of functionality into Coq and these types are no longer in CakeML but extracted