31 lines
696 B
Coq
31 lines
696 B
Coq
|
From Coq Require Extraction.
|
||
|
|
Require Import Strings.String.
|
||
|
|
|
||
|
|
(*
|
||
|
|
Abstract cryptographic primitives.
|
||
|
|
|
||
|
|
For proof-checking, this will resolve to a set of axioms, but when
|
||
|
|
extracting to ocaml, this should be replaced with the real implementation
|
||
|
|
of the cryptographic primitives.
|
||
|
|
*)
|
||
|
|
Module Type AbsCryptoPrims.
|
||
|
|
Definition principal : Type := string.
|
||
|
|
|
||
|
|
Inductive label : Set :=
|
||
|
|
Public : label
|
||
|
|
.
|
||
|
|
End AbsCryptoPrims.
|
||
|
|
|
||
|
|
Module NullCryptoPrims : AbsCryptoPrims.
|
||
|
|
Definition principal : Type := string.
|
||
|
|
|
||
|
|
Inductive label : Set :=
|
||
|
|
Public : label
|
||
|
|
.
|
||
|
|
End NullCryptoPrims.
|
||
|
|
|
||
|
|
Extraction Language OCaml.
|
||
|
|
Set Extraction Optimize.
|
||
|
|
Set Extraction AccessOpaque.
|
||
|
|
Extraction "CryptoPrims" NullCryptoPrims.
|