Reflect backend changes: Separation of model from analysis

hax-driver.py

@@ -116,7 +116,7 @@ def shell(command, expect=0, cwd=None, env={}):
 elif options.sub == "typecheck-proverif":
     # Typecheck subcommand.
     custom_env = {}
-    shell(["proverif", "-lib", "proofs/proverif/extraction/lib", "proofs/proverif/extraction/output.pv"], env=custom_env)
+    shell(["proverif", "-lib", "proofs/proverif/extraction/handwritten_lib", "-lib", "proofs/proverif/extraction/lib", "proofs/proverif/extraction/analysis.pv"], env=custom_env)
     exit(0)
 else:
     parser.print_help()

proofs/proverif/extraction/analysis.pv

@@ -0,0 +1,8 @@
+(*****************************************)
+(* Top-level process *)
+(*****************************************)
+
+process
+    0
+
+

proofs/proverif/extraction/handwritten_lib.pvl

@@ -0,0 +1,61 @@
+type bertie__tls13formats__handshake_data__t_HandshakeData.
+
+(* Constants *)
+const bertie__tls13formats__v_LABEL_KEY: bitstring.
+const bertie__tls13formats__v_LABEL_IV: bitstring.
+const bertie__tls13formats__v_LABEL_FINISHED: bitstring.
+const bertie__tls13formats__v_LABEL_DERIVED: bitstring.
+const bertie__tls13formats__v_LABEL_C_HS_TRAFFIC: bitstring.
+const bertie__tls13formats__v_LABEL_S_HS_TRAFFIC: bitstring.
+
+(* Bytes *)
+type bertie__tls13utils__t_Bytes.
+fun bertie__tls13utils__impl__Bytes__new(bitstring):  bertie__tls13utils__t_Bytes.
+fun bertie__tls13utils__bytes(bitstring):  bertie__tls13utils__t_Bytes.
+
+(* Option<Bytes> *)
+type core__option__t_Option_of_bertie__tls13utils__t_Bytes.
+fun core__option__Option_Option_Some_c(bertie__tls13utils__t_Bytes): core__option__t_Option_of_bertie__tls13utils__t_Bytes [data].
+fun core__option__Option_Option_None_c(): core__option__t_Option_of_bertie__tls13utils__t_Bytes.
+
+(* Transcript *)
+type bertie__tls13formats__t_Transcript.
+fun bertie__tls13formats__impl__Transcript__add(bertie__tls13formats__t_Transcript, bertie__tls13formats__handshake_data__t_HandshakeData): bertie__tls13formats__t_Transcript.
+fun bertie__tls13formats__impl__Transcript__transcript_hash(bertie__tls13formats__t_Transcript): bertie__tls13utils__t_Bytes.
+
+(* Hash Algorithm *)
+type bertie__tls13crypto__t_HashAlgorithm.
+fun bertie__tls13crypto__impl__HashAlgorithm__hash(bertie__tls13crypto__t_HashAlgorithm,  bertie__tls13utils__t_Bytes): bertie__tls13utils__t_Bytes.
+fun bertie__tls13crypto__impl__HashAlgorithm__hash_len(bertie__tls13crypto__t_HashAlgorithm): bitstring.
+fun bertie__tls13crypto__impl__HashAlgorithm__hmac_tag_len(bertie__tls13crypto__t_HashAlgorithm): bitstring.
+
+(* AEAD Algorithm *)
+type bertie__tls13crypto__t_AeadAlgorithm.
+fun bertie__tls13crypto__impl__AeadAlgorithm__key_len(bertie__tls13crypto__t_AeadAlgorithm): bitstring.
+fun bertie__tls13crypto__impl__AeadAlgorithm__iv_len(bertie__tls13crypto__t_AeadAlgorithm):bitstring.
+
+type bertie__tls13crypto__t_AeadKeyIV.
+fun bertie__tls13crypto__impl__AeadKeyIV__new(bitstring, bertie__tls13utils__t_Bytes): bitstring.
+fun bertie__tls13crypto__impl__AeadKey__new(bertie__tls13utils__t_Bytes, bertie__tls13crypto__t_AeadAlgorithm): bitstring.
+
+(* Algorithms pack *)
+type bertie__tls13crypto__t_Algorithms.
+fun accessor_bertie__tls13crypto__Algorithms_f_kem(bertie__tls13crypto__t_Algorithms): bitstring.
+fun accessor_bertie__tls13crypto__Algorithms_f_aead(bertie__tls13crypto__t_Algorithms): bertie__tls13crypto__t_AeadAlgorithm.
+fun accessor_bertie__tls13crypto__Algorithms_f_hash(bertie__tls13crypto__t_Algorithms):bertie__tls13crypto__t_HashAlgorithm.
+
+(* Parsing *)
+fun bertie__tls13formats__parse_server_hello(bertie__tls13crypto__t_Algorithms, bertie__tls13formats__handshake_data__t_HandshakeData): bitstring.
+
+(* HKDF *)
+fun bertie__tls13handshake__hkdf_expand_label(bertie__tls13crypto__t_HashAlgorithm, bertie__tls13utils__t_Bytes, bertie__tls13utils__t_Bytes,  bertie__tls13utils__t_Bytes, bitstring): bertie__tls13utils__t_Bytes.
+fun bertie__tls13crypto__hkdf_extract(bertie__tls13crypto__t_HashAlgorithm, bertie__tls13utils__t_Bytes, bertie__tls13utils__t_Bytes): bertie__tls13utils__t_Bytes.
+
+(* Other *)
+fun bertie__tls13crypto__kem_decap(bitstring, bertie__tls13utils__t_Bytes, bertie__tls13utils__t_Bytes): bertie__tls13utils__t_Bytes.
+
+fun bertie__tls13crypto__zero_key(bertie__tls13crypto__t_HashAlgorithm): bertie__tls13utils__t_Bytes.
+
+(* this clone is too narrow of course; really want to treat as copy*)
+fun core__clone__Clone_f_clone(bertie__tls13utils__t_Bytes): bertie__tls13utils__t_Bytes.
+fun rust_primitives__unsize(bitstring): bitstring.