Update CakeML AM with latest CVM and appraisal functionality from Coq.

ku-sldg / attestation-testbed

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

0 stars 0 forks source link

Update CakeML AM with latest CVM and appraisal functionality from Coq. #33

Open ampetz opened 2 years ago

ampetz commented 2 years ago

Have cakeml AM use latest Copland Virtual Machine and generalized appraisal functions from here.

Best option is to extract them via Coq --> CakeML synthesis (see @barclata for latest status on this). Alternatively, or as a first pass, do manually.

This issue depends on #32 being implemented first.