ada/SPARKlib
0
0
Fork 0
mirror of https://github.com/AdaCore/SPARKlib.git synced 2026-02-12 13:11:36 -08:00
Code Issues Packages Projects Releases Wiki Activity
Files
master
SPARKlib/proof/sessions
History
Piotr Trojanek 6645568407 Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
..
0bcf23240135a11a0142-ithmetic__lemma_mult_is_monotonic
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
0f17f8b62cd8a7bffeab-etic__lemma_mult_then_mod_is_zero
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
1d92f96e5f6364a76bbf-etic__lemma_div_left_is_monotonic
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
1d097feae45f3c421f00-thmetic__lemma_exp_is_monotonic_2
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
1f5e0d3da8c8589e0ae7-lemmas__test_transitive_order_int
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
2b7c2a3e36b04c0b818f-a_div_right_negative_is_monotonic
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
2c733bcadfe12ab1a413-er_arithmetic__lemma_mod_symmetry
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
2d7ed4e040e983cd97fd-mas__test_transitive_order_int__2
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
2e95af902829fefe30c3-rithmetic__lemma_add_is_monotonic
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
4af2f1bc2403e3a9887d-tic__lemma_mult_then_div_is_ident
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
4b5ad85005df2c8812a5-rithmetic__lemma_div_is_monotonic
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
4b65b283f33a3d6f6199-thmetic__lemma_rounding_error_div
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
5cd1b6b65b1ae5a81d70-thmetic__lemma_rounding_error_sub
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
6b31d298c662a4559d33-etic__lemma_mult_then_mod_is_zero
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
7b84aa1983ffcbcd1841-rithmetic__lemma_exp_is_monotonic
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
7d4b0fdbcc0de7baeb4d-st_ufloat__lemma_transitive_order
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
7e2775a8fae201cb26fa-ithmetic__lemma_mult_is_monotonic
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
7f714a4a3e04d0588f52-eger_arithmetic__lemma_mult_scale
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
8bc676b4938878351679-metic__lemma_div_then_mult_bounds
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
9a38ab0a2aa14d02861b-rithmetic__lemma_sub_is_monotonic
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
06ffec3f591f343740b2-eger_arithmetic__lemma_mult_scale
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
14d819b9d90a2f24021c-__long_float_arithmetic__is_float
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
16a938375bd5e13cb61a-mmas__test_transitive_order_float
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
17d9dafb4b2b3f31e15f-ithmetic__lemma_integer_mul_exact
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
42fec7509b4626e50fa3-__float_arithmetic__is_integer_64
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
46c887da646e7c1e7984-thmetic__lemma_rounding_error_div
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
56a7f0baf56e9de3c0b3-mas__float_arithmetic__is_integer
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
64aa8cda378577e9a1d9-tic__lemma_div_right_is_monotonic
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
76ec97213b0900829a05-constant_strings__to_chars_ptr__3
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
80ec461ebdb26b04d3c6-64_arithmetic__lemma_mult_protect
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
84e5e4f9a3e38055f87f-tic__lemma_mult_then_div_is_ident
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
87e988e63a55185c3842-_lemma_mult_is_strictly_monotonic
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
89c902ba6c5033c74f51-tic__lemma_mult_then_div_is_ident
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
97c0b29bafb323d62578-ithmetic__lemma_integer_sub_exact
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
97c6e3ca67dad42bc909-etic__lemma_mult_by_less_than_one
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
97fac78bd72ed73dc55a-_lemma_mult_is_strictly_monotonic
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
003d5099756f44440ead-thmetic__lemma_rounding_error_mul
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
130e250c2fd5cdf74347-etic__lemma_div_left_is_monotonic
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
186a327cb4b864da080b-rithmetic__lemma_div_is_monotonic
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
196bb4be56e3ed2a2109-thmetic__lemma_exp_is_monotonic_2
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
202ec312f08173cc28f3-thmetic__lemma_rounding_error_add
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
382c86ac20187fb5ac4d-ithmetic__lemma_integer_add_exact
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
401cd56632b241fc5812-a_div_right_negative_is_monotonic
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
519eea1a8fd38ca67cc5-metic__lemma_div_then_mult_bounds
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
618ad12bf1b01dba5e0d-thmetic__lemma_rounding_error_sub
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
760a096962f38ebb1b29-s__test_transitive_order_float__2
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
922c5b1323f2fc559fd8-as__float_arithmetic__is_float__2
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
938f242ec7e9eb9e1279-long_float_arithmetic__is_integer
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
1587aa0712142623d31f-er_arithmetic__lemma_mult_protect
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
3666e050ebfcf1e23a7a-_mult_right_negative_is_monotonic
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
6594bb5f6ea05237f2af-_lemma_mult_is_strictly_monotonic
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
12584ea9d338c8ef5e90-tic__lemma_mult_then_div_is_ident
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
13653aa826f557fe213b-ithmetic__lemma_integer_mul_exact
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
55097f71d3983ad619d6-g_float_arithmetic__is_integer_64
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
56417d37d00cde9404b9-ithmetic__lemma_mult_is_monotonic
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
62892e033bbc392d6ea8-tic__lemma_div_right_is_monotonic
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
72076e9f65534867198f-teger_arithmetic__lemma_mod_range
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
309094fba5cf2e267ec5-thmetic__lemma_rounding_error_add
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
844251543d76a95ec08c-etic__lemma_mult_then_mod_is_zero
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
918787142d8c51d89d54-ithmetic__lemma_mult_is_monotonic
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
1153507328a6336538e0-thmetic__lemma_rounding_error_mul
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
a0f15d54f1f535f9ef2e-rithmetic__lemma_sub_is_monotonic
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
a5b32f8dec9ac5614d00-rithmetic__lemma_div_is_monotonic
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
a8e2e1737e9231ad4d57-rithmetic__lemma_exp_is_monotonic
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
a01fbf05e26bd92ede96-er_arithmetic__lemma_mod_symmetry
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
ac105cb128f299a4f6f4-ong_float_arithmetic__is_float__2
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
ada___ada___spark__c__constant_strings__value__3
Fixes to sparklib proofs
2026-01-20 10:53:48 +09:00
ada___ada___spark__c__constant_strings__value__4
Fixes to sparklib proofs
2026-01-20 10:53:48 +09:00
ada___ada___spark__c__strings__update
Fixes to sparklib proofs
2026-01-20 10:53:48 +09:00
ada___ada___spark__c__strings__update__2
Fixes to sparklib proofs
2026-01-20 10:53:48 +09:00
ada___ada___spark__c__strings__value__3
Fixes to sparklib proofs
2026-01-20 10:53:48 +09:00
ada___ada___spark__c__strings__value__4
Fixes to sparklib proofs
2026-01-20 10:53:48 +09:00
ada___ada___spark__lemmas__float_arithmetic__is_float
Fixes to sparklib proofs
2026-01-20 10:53:48 +09:00
ada___spark__big_intervals__in_range
Fix generate_session.py
2026-01-07 08:19:57 +00:00
ada___spark__big_intervals__interval
Fix generate_session.py
2026-01-07 08:19:57 +00:00
ada___spark__big_intervals__next
Fix generate_session.py
2026-01-07 08:19:57 +00:00
b89f407e9fdfd75dfc07-er_arithmetic__lemma_mult_protect
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
b491ad98cbdad88d52f0-etic__lemma_mult_then_mod_is_zero
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
bada34272ab2b8fe8051-g_float_arithmetic__is_integer_32
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
bc836d7b5ab4f77a68f9-__float_arithmetic__is_integer_32
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
bd3fff484e28c2c89337-32_arithmetic__lemma_mult_protect
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
bd83e8c54968758aa2db-rithmetic__lemma_div_is_monotonic
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
bf4f52c54d4d3435c035-ithmetic__lemma_integer_sub_exact
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
c5e7f142592403ec30a7-ithmetic__lemma_integer_add_exact
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
c48f30ab6d9faf8da964-rithmetic__lemma_div_is_monotonic
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
cdd843567552e5325ee8-teger_arithmetic__lemma_mod_range
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
ce9b0648315bc680116c-rithmetic__lemma_add_is_monotonic
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
d40d5404ce0dddcc0346-od64_arithmetic__lemma_mult_scale
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
d83c8bdd14646b213148-rithmetic__lemma_div_is_monotonic
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
da0e97b4b94bc85040be-ithmetic__lemma_mult_is_monotonic
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
de66ff03593788f3256a-_mult_right_negative_is_monotonic
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
e7ddc9cfa09b3d1fd048-ithmetic__lemma_mult_is_monotonic
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
eb7efa8ab1eaa5bd9a03-_lemma_mult_is_strictly_monotonic
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
eebd3d8fb524a7a811dd-test_uint__lemma_transitive_order
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
eed4f33a8902eb728fe3-od32_arithmetic__lemma_mult_scale
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00
efcf5833b7284726b633-etic__lemma_mult_by_less_than_one
Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1)
2026-01-27 01:32:34 +01:00