31 Commits

Author	SHA1	Message	Date
MARCHE Claude	174c9a01f5	do not allow implicit inference of partial	2024-10-31 15:27:09 +01:00
Cláudio Belo Lourenço	c05d96a102	minor cosmetic fix base64 example	2020-07-28 15:05:45 +02:00
Cláudio Belo Lourenço	1317661fda	Documentation for Base64 encoding	2020-03-04 15:11:38 +01:00
Cláudio Belo Lourenço	bc5c535643	Minor cosmetics fixes in Base64	2020-02-26 09:57:55 +01:00
Cláudio Belo Lourenço	d8b9a4b3d5	Base64 example with encode and decode unique proofs	2020-02-26 09:34:34 +01:00
Cláudio Belo Lourenço	2224f6a1e3	Base64 encode unique (wip)	2020-02-26 08:34:49 +01:00
Cláudio Belo Lourenço	bccc23fd9f	base64 encode unique proof (wip)	2020-02-25 16:06:37 +01:00
Cláudio Belo Lourenço	affea82b75	Fixes in base64 ane hex encoding	2020-02-24 16:16:39 +01:00
Cláudio Belo Lourenço	9282bf6a10	base64 proof completed	2020-02-24 08:58:44 +01:00
Cláudio Belo Lourenço	5a16cc5891	fix base64 encoding for new ocaml string theory	2020-02-21 18:20:08 +01:00
Jean-Christophe Filliatre	9e033eaa77	strings: make OCaml.length a partial function	2020-02-21 10:33:52 +01:00
Jean-Christophe Filliatre	b13bca590c	updated proof sessions using strings	2020-02-20 15:28:46 +01:00
Jean-Christophe Filliatre	97247b2a68	string_base64_encoding: cleaning up	2020-02-20 14:57:01 +01:00
Jean-Christophe Filliatre	5f3098b962	OCaml strings are now an abstract data type ... this is to ensure that OCaml strings have a length no greater than max_int; actually, no greater than max_string_length, which is smaller	2020-02-20 14:46:09 +01:00
Jean-Christophe Filliatre	f987edf5fe	string_base64_encoding: absurd instead of assert false	2020-02-20 14:10:06 +01:00
Jean-Christophe Filliatre	502bf55e5c	string_base64_encoding now using StringBuffer ... and extracted OCaml code is tested	2020-02-20 14:07:29 +01:00
Cláudio Belo Lourenço	c751f44b5a	More simplifications in Base64 encoding	2020-02-18 21:30:55 +01:00
Cláudio Belo Lourenço	e382f80bba	Remove more intermediate assertions and cosmetics fixes in Base64 encoding	2020-02-18 16:23:09 +01:00
Cláudio Belo Lourenço	47411d4ff9	Removing unnecessary intermediate assertions Base64 encoding example	2020-02-18 15:58:59 +01:00
Cláudio Belo Lourenço	64fdcf8344	Minor simplifications in Base64 example	2020-02-18 14:50:08 +01:00
Cláudio Belo Lourenço	5b4301f0f9	Base64 encoding. All VCs proved.	2020-02-18 14:34:39 +01:00
Cláudio Belo Lourenço	347b0e4a46	Proof Base64 (wip)	2020-02-18 14:06:50 +01:00
Cláudio Belo Lourenço	be706f8156	Replace div and mod by ghost multiplication	2020-02-17 21:53:43 +01:00
Cláudio Belo Lourenço	ec7a35be36	replace divisions by ghost multiplication	2020-02-17 16:36:09 +01:00
Cláudio Belo Lourenço	6d5f49c01a	Proof base64 (wip)	2020-02-17 14:51:35 +01:00