Commit Graph

Select branches

Hide Pull Requests

main

Mono Color

• ff1fd68eb1 feat(mpz_swap): Proved correctness of mpz_swap. Proved some previously admitted lemmas. main xiaoh105 2025-06-22 21:00:50 +08:00
• 77ccdd3e50 Merge remote-tracking branch 'origin/main' into mpz_sgn xiaoh105 2025-06-22 19:14:56 +08:00
• 3a102d0d65 feat(mpz_sgn): Proved correctness of function mpz_sgn. xiaoh105 2025-06-22 19:10:35 +08:00
• 4c13bd6648 Merge pull request #3 from xiaoh105/remove_compact happyZYM 2025-06-22 17:30:14 +08:00
• 8a14eab669 finish refactoring ZhuangYumin 2025-06-22 09:29:22 +00:00
• 029e79b252 Merge pull request #2 from xiaoh105/mpn_add_n happyZYM 2025-06-22 16:44:24 +08:00
• 7876f2ecbf finish proof_of_mpn_add_n_which_implies_wit_4 ZhuangYumin 2025-06-22 08:41:55 +00:00
• d88a2acd6d ready to prove proof_of_mpn_add_n_which_implies_wit_4 ZhuangYumin 2025-06-22 08:32:38 +00:00
• e4317a303f finish proof_of_mpn_add_n_return_wit_1 ZhuangYumin 2025-06-22 08:28:31 +00:00
• fd26d9669e finish all adder proof for mpn_add_n ZhuangYumin 2025-06-22 07:37:10 +00:00
• 0fdf4fc328 finish proof_of_mpn_add_n_entail_wit_3_1 ZhuangYumin 2025-06-22 07:25:46 +00:00
• 6167816613 ready to prove the correctness of 3-carry ZhuangYumin 2025-06-22 06:58:57 +00:00
• 1e3c1ea7ec ready to prove four carry and uncarry in mpn_add_n ZhuangYumin 2025-06-22 05:12:16 +00:00
• 94581ea60d first version annotation for mpn_add_n ZhuangYumin 2025-06-21 16:03:04 +00:00
• f4db688a30 fix(mpz_realloc): fix minor bugs in proof of mpz_realloc. xiaoh105 2025-06-21 22:23:37 +08:00
• 1e627cdb84 Merge remote-tracking branch 'origin/main' into mpz_realloc xiaoh105 2025-06-21 22:08:51 +08:00
• f8af2cf004 feat(mpz_clear & mpz_realloc): Proved correctness of mpz_clear and mpz_realloc xiaoh105 2025-06-21 21:51:00 +08:00
• 77e1460ebc Merge pull request #1 from xiaoh105/mpn_add_1 happyZYM 2025-06-21 19:49:18 +08:00
• 5c69a81a44 finish mpn_add_1 ZhuangYumin 2025-06-21 11:47:52 +00:00
• bb22511fef only last wh ich implies left ZhuangYumin 2025-06-21 08:17:32 +00:00
• 9ccea05835 finish uncarry ZhuangYumin 2025-06-21 08:00:17 +00:00
• 0656f30a16 finish carry proof ZhuangYumin 2025-06-21 07:50:20 +00:00
• f462570ccd ready to finalize proof_of_mpn_add_1_entail_wit_2_1 ZhuangYumin 2025-06-21 05:45:27 +00:00
• 49848bd048 finish proof_of_mpn_add_1_return_wit_1 ZhuangYumin 2025-06-20 16:57:26 +00:00
• c206e4165f finish symexec ZhuangYumin 2025-06-20 13:57:21 +00:00
• 8c52269a5e first version for annotations of mpn_add_1 ZhuangYumin 2025-06-20 13:24:36 +00:00
• cce2450cd7 Merge branch 'main' of https://github.com/xiaoh105/MiniGmp-Verification ZhuangYumin 2025-06-13 12:50:34 +00:00
• 257241df90 feat(normalized_size): Proved correctness of mpd_normalized_size. Fix minor bugs in previous proves. xiaoh105 2025-06-12 22:11:54 +08:00
• f7432dca84 feat(cmp4): modied certain annotations for mpn_cmp and proved correctness of mpn_cmp4. xiaoh105 2025-06-12 12:37:01 +08:00
• 36204b8877 feat(cmp): Proved correctness of mpn_cmp. xiaoh105 2025-06-11 16:54:36 +08:00
• 4c0b0e98fa feat(mpn_copyi): Proved correctness of mpn_copyi and other simple util functions. xiaoh105 2025-06-10 17:54:33 +08:00
• 1873d949ce Add annotations to gmp.c xiaoh105 2025-06-07 15:23:11 +08:00
• e7bc194ec7 feat: Add list_store_Z_nth lemma. xiaoh105 2025-06-03 17:52:15 +08:00
• 596f66206e chore: add devcontainer to gitignore ZhuangYumin 2025-06-03 09:31:20 +00:00
• f6bb7e9a66 feat: rewrite certain definitions of internal structures to make proof easier. xiaoh105 2025-05-30 00:41:29 +08:00
• 47ca3e72bd feat: Add definitions for basic structures. xiaoh105 2025-05-27 16:09:30 +08:00
• 940b85ac80 initial commit xiaoh105 2025-05-21 16:56:46 +08:00