Files

 master

/

aes

/

Copy path

Directory actions

More options

Directory actions

More options

Latest commit

andrew-appel

Update VST to CompCert 3.8

Nov 30, 2020

35cb26c · Nov 30, 2020

History

History

This branch is 913 commits behind PrincetonUniversity/VST:master.

/

aes

/

Top

Folders and files

Name		Name	Last commit message	Last commit date
parent directory ..
extracted		extracted	confirm that extracted high-level AES spec produces the same output a…	Jan 19, 2017
mbedtls		mbedtls	updated to latest master	Mar 7, 2017
module_based		module_based	reorganize/cleanup AES	Mar 24, 2017
testing		testing	confirm that extracted high-level AES spec produces the same output a…	Jan 19, 2017
unused		unused	reorganize/cleanup AES	Mar 24, 2017
GF_ops_LL.v		GF_ops_LL.v	Compatibility with Coq 8.12beta1, fixed many deprecated things, mostl…	Jun 19, 2020
aes.v		aes.v	Update VST to CompCert 3.8	Nov 30, 2020
aes_encryption_loop_body.v		aes_encryption_loop_body.v	factor out AES encryption loop body into verif_encryption_LL_loop_bod…	Apr 5, 2017
api_specs.v		api_specs.v	Port to Coq 8.11	Mar 27, 2020
bitfiddling.v		bitfiddling.v	Change Znth so that the "default" argument is implicit, filled in	Mar 11, 2018
conv_HL_to_LL.v		conv_HL_to_LL.v	move admitted lemmas into separate files	Mar 30, 2017
encryption_LL_round_step_eqs.v		encryption_LL_round_step_eqs.v	Change Znth so that the "default" argument is implicit, filled in	Mar 11, 2018
equiv_GF_ops.v		equiv_GF_ops.v	move admitted lemmas into separate files	Mar 30, 2017
equiv_encryption.v		equiv_encryption.v	Compatibility with Coq 8.12beta1, fixed many deprecated things, mostl…	Jun 19, 2020
find_slow_Qed.py		find_slow_Qed.py	python script to find what causes Qed slowness	Apr 10, 2017
grab_mbedtls_aes.sh		grab_mbedtls_aes.sh	add script to grab original mbedtls AES sources	Oct 3, 2016
invoke_clightgen.sh		invoke_clightgen.sh	clightgen command	Oct 4, 2016
invoke_clightgen_preprocessor.sh		invoke_clightgen_preprocessor.sh	clightgen preprocessor command	Oct 20, 2016
list_lemmas.v		list_lemmas.v	Change Znth so that the "default" argument is implicit, filled in	Mar 11, 2018
list_utils.v		list_utils.v	Compatibility with Coq 8.12beta1, fixed many deprecated things, mostl…	Jun 19, 2020
partially_filled.v		partially_filled.v	Change Znth so that the "default" argument is implicit, filled in	Mar 11, 2018
sbox.v		sbox.v	msl ported + cleaning trailing spaces	Jan 13, 2017
simplify_Delta_SlowQed.v		simplify_Delta_SlowQed.v	Improved the efficiency (execute and Qed) of simplify_Delta, abbrevia…	Apr 9, 2017
spec_AES256_HL.v		spec_AES256_HL.v	Got aes to build again (probably broken for a week or two).	Aug 29, 2018
spec_encryption_LL.v		spec_encryption_LL.v	Change Znth so that the "default" argument is implicit, filled in	Mar 11, 2018
spec_utils_LL.v		spec_utils_LL.v	Got aes to build again (probably broken for a week or two).	Aug 29, 2018
tablesLL.v		tablesLL.v	Compatibility with Coq 8.12beta1, fixed many deprecated things, mostl…	Jun 19, 2020
verif_encryption_LL.v		verif_encryption_LL.v	Compatibility with Coq 8.12beta1, fixed many deprecated things, mostl…	Jun 19, 2020
verif_encryption_LL_after_loop.v		verif_encryption_LL_after_loop.v	Compatibility with Coq 8.12beta1, fixed many deprecated things, mostl…	Jun 19, 2020
verif_encryption_LL_loop_body.v		verif_encryption_LL_loop_body.v	Compatibility with Coq 8.12beta1, fixed many deprecated things, mostl…	Jun 19, 2020
verif_encryption_one_column.v		verif_encryption_one_column.v	Compatibility with Coq 8.12beta1, fixed many deprecated things, mostl…	Jun 19, 2020
verif_gen_tables_LL.v		verif_gen_tables_LL.v	Compatibility with Coq 8.12beta1, fixed many deprecated things, mostl…	Jun 19, 2020
verif_setkey_enc_LL.v		verif_setkey_enc_LL.v	Compatibility with Coq 8.12beta1, fixed many deprecated things, mostl…	Jun 19, 2020
verif_setkey_enc_LL_loop_body.v		verif_setkey_enc_LL_loop_body.v	Compatibility with Coq 8.12beta1, fixed many deprecated things, mostl…	Jun 19, 2020
View all files