search

ku-sldg / am-cakeml

Delivery repo for the KU CakeML Attestation Manager
GNU General Public License v3.0
1 stars 0 forks source link

streamline provisioning of manifest generator/compiler demo scripts (Copland protocol/evidence term provisioning) #46

Closed ampetz closed 1 month ago

ampetz commented 1 month ago

Resolved this by adding adding (and extracting) a Coq datatype called: ManGenConfigData.

Used this new datatype in the am-cakeml repo in "stubs/ManGenConfig.sml" by adding a new value field called "manGenConfigData". This instantiates a ManGenConfigData record that is used for provisioning in both the ManifestGenerator and Client main source files. Examples of these records for each demo scenario are defined above in ManGenConfig.sml.