{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":651567039,"defaultBranch":"main","name":"cbmc-examples","ownerLogin":"rod-chapman","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2023-06-09T14:24:21.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/22537733?v=4","public":true,"private":false,"isOrgOwned":false},"refInfo":{"name":"","listCacheKey":"v0:1686320662.474732","currentOid":""},"activityList":{"items":[{"before":"426f81b8cc7220a355cfa28efe688ab2a2d1b2cd","after":"86395d9cdb5f3b4902f4611e0bae201cf990e7c9","ref":"refs/heads/main","pushedAt":"2024-09-13T15:14:21.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rod-chapman","name":"Roderick Chapman","path":"/rod-chapman","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22537733?s=80&v=4"},"commit":{"message":"Add this example code to demonstrate this issue\n\nSigned-off-by: Rod Chapman <rodchap@amazon.com>","shortMessageHtmlLink":"Add this example code to demonstrate this issue"}},{"before":"358a27a96259236987845b981cac06801fc3d343","after":"426f81b8cc7220a355cfa28efe688ab2a2d1b2cd","ref":"refs/heads/main","pushedAt":"2024-09-03T09:27:09.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rod-chapman","name":"Roderick Chapman","path":"/rod-chapman","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22537733?s=80&v=4"},"commit":{"message":"Add implementation of Kyber Montgomery reduce\n\nSigned-off-by: Rod Chapman <rodchap@amazon.com>","shortMessageHtmlLink":"Add implementation of Kyber Montgomery reduce"}},{"before":"4dfea6925f0698cb8ad03ca12a0da41db19f3093","after":"358a27a96259236987845b981cac06801fc3d343","ref":"refs/heads/main","pushedAt":"2024-09-03T09:25:12.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rod-chapman","name":"Roderick Chapman","path":"/rod-chapman","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22537733?s=80&v=4"},"commit":{"message":"Add implementations of the Montgomery reduction from Kyber\n\nSigned-off-by: Rod Chapman <rodchap@amazon.com>","shortMessageHtmlLink":"Add implementations of the Montgomery reduction from Kyber"}},{"before":"bc9509d262ca02228c724b6758065fba48cb0f28","after":"4dfea6925f0698cb8ad03ca12a0da41db19f3093","ref":"refs/heads/main","pushedAt":"2024-08-29T10:46:42.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rod-chapman","name":"Roderick Chapman","path":"/rod-chapman","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22537733?s=80&v=4"},"commit":{"message":"Add second version mul2() with intermediate assertions\n\nSigned-off-by: Rod Chapman <rodchap@amazon.com>","shortMessageHtmlLink":"Add second version mul2() with intermediate assertions"}},{"before":"4136c7c652b53ed3f07c6ca9b1e17421b92d0da9","after":"bc9509d262ca02228c724b6758065fba48cb0f28","ref":"refs/heads/main","pushedAt":"2024-08-29T10:03:53.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rod-chapman","name":"Roderick Chapman","path":"/rod-chapman","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22537733?s=80&v=4"},"commit":{"message":"Add new example proof of constant time multiplication mod Q from MLKEM\n\nSigned-off-by: Rod Chapman <rodchap@amazon.com>","shortMessageHtmlLink":"Add new example proof of constant time multiplication mod Q from MLKEM"}},{"before":"06dc5d576b47344465b0cf1857b172a263eafa5d","after":"4136c7c652b53ed3f07c6ca9b1e17421b92d0da9","ref":"refs/heads/main","pushedAt":"2024-08-06T19:47:58.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rod-chapman","name":"Roderick Chapman","path":"/rod-chapman","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22537733?s=80&v=4"},"commit":{"message":"Add example showing pre-condition involving alignof() function\n\nSigned-off-by: Rod Chapman <rodchap@amazon.com>","shortMessageHtmlLink":"Add example showing pre-condition involving alignof() function"}},{"before":"7e1048b236ca2fb5f4a4240f48ce55073a4c5d5c","after":"06dc5d576b47344465b0cf1857b172a263eafa5d","ref":"refs/heads/main","pushedAt":"2024-07-26T01:45:09.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rod-chapman","name":"Roderick Chapman","path":"/rod-chapman","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22537733?s=80&v=4"},"commit":{"message":"Add decreases contract to all loops and verify them\n\nSigned-off-by: Rod Chapman <rodchap@amazon.com>","shortMessageHtmlLink":"Add decreases contract to all loops and verify them"}},{"before":"66fa9d50549ea14f16f55b2b847dd2e44cc36bee","after":"7e1048b236ca2fb5f4a4240f48ce55073a4c5d5c","ref":"refs/heads/main","pushedAt":"2024-07-18T13:41:10.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rod-chapman","name":"Roderick Chapman","path":"/rod-chapman","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22537733?s=80&v=4"},"commit":{"message":"Add GOTO file generated by PR 8363 branch of CBMC\n\nSigned-off-by: Rod Chapman <rodchap@amazon.com>","shortMessageHtmlLink":"Add GOTO file generated by PR 8363 branch of CBMC"}},{"before":"0f4c4029f5de1e77176f4ca7d77046f5179a449b","after":"66fa9d50549ea14f16f55b2b847dd2e44cc36bee","ref":"refs/heads/main","pushedAt":"2024-07-18T10:32:51.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rod-chapman","name":"Roderick Chapman","path":"/rod-chapman","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22537733?s=80&v=4"},"commit":{"message":"Add test case artefacts for this issue report\n\nSigned-off-by: Rod Chapman <rodchap@amazon.com>","shortMessageHtmlLink":"Add test case artefacts for this issue report"}},{"before":"4c695106f42c93e448b81c2bb83e0574e447d4af","after":"0f4c4029f5de1e77176f4ca7d77046f5179a449b","ref":"refs/heads/main","pushedAt":"2024-07-16T20:10:41.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rod-chapman","name":"Roderick Chapman","path":"/rod-chapman","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22537733?s=80&v=4"},"commit":{"message":"Updates to choose Z3, cadical or bitwuzla for each function.\n\nSigned-off-by: Rod Chapman <rodchap@amazon.com>","shortMessageHtmlLink":"Updates to choose Z3, cadical or bitwuzla for each function."}},{"before":"3c13393468bea5a9b7587986e5e692d6cf274d8d","after":"4c695106f42c93e448b81c2bb83e0574e447d4af","ref":"refs/heads/main","pushedAt":"2024-07-12T13:03:42.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rod-chapman","name":"Roderick Chapman","path":"/rod-chapman","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22537733?s=80&v=4"},"commit":{"message":"Isolate and add test case for this issue\n\nSigned-off-by: Rod Chapman <rodchap@amazon.com>","shortMessageHtmlLink":"Isolate and add test case for this issue"}},{"before":"8f88c125c2963d57846764179564626e8b17c41a","after":"3c13393468bea5a9b7587986e5e692d6cf274d8d","ref":"refs/heads/main","pushedAt":"2024-07-03T14:26:24.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rod-chapman","name":"Roderick Chapman","path":"/rod-chapman","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22537733?s=80&v=4"},"commit":{"message":"Use Kissat for these proofs.\n\nAdd README to explain these examples.\n\nMake all function contracts visible in crypto.h\nand add explanatory comments in crypto.c\n\nSigned-off-by: Rod Chapman <rodchap@amazon.com>","shortMessageHtmlLink":"Use Kissat for these proofs."}},{"before":"fd66618b8096c19671000e88a08d320f14ef4905","after":"8f88c125c2963d57846764179564626e8b17c41a","ref":"refs/heads/main","pushedAt":"2024-07-03T13:51:19.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rod-chapman","name":"Roderick Chapman","path":"/rod-chapman","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22537733?s=80&v=4"},"commit":{"message":"Add README for this directory\n\nSigned-off-by: Rod Chapman <rodchap@amazon.com>","shortMessageHtmlLink":"Add README for this directory"}},{"before":"7beb28eba3a817e856993455cc3761441ed0cb88","after":"fd66618b8096c19671000e88a08d320f14ef4905","ref":"refs/heads/main","pushedAt":"2024-07-03T13:43:08.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rod-chapman","name":"Roderick Chapman","path":"/rod-chapman","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22537733?s=80&v=4"},"commit":{"message":"Add required --replace-call-with-contract flag for goto-instrument.\n\nSigned-off-by: Rod Chapman <rodchap@amazon.com>","shortMessageHtmlLink":"Add required --replace-call-with-contract flag for goto-instrument."}},{"before":"8df7dd71719e8c5dc29c1800e9c6f29b345dead3","after":"7beb28eba3a817e856993455cc3761441ed0cb88","ref":"refs/heads/main","pushedAt":"2024-07-03T11:06:41.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rod-chapman","name":"Roderick Chapman","path":"/rod-chapman","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22537733?s=80&v=4"},"commit":{"message":"Add simple example of modular reasoning\n\nSigned-off-by: Rod Chapman <rodchap@amazon.com>","shortMessageHtmlLink":"Add simple example of modular reasoning"}},{"before":"15731a0885da30498a2de369b9965914735a5433","after":"8df7dd71719e8c5dc29c1800e9c6f29b345dead3","ref":"refs/heads/main","pushedAt":"2024-07-01T09:55:16.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rod-chapman","name":"Roderick Chapman","path":"/rod-chapman","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22537733?s=80&v=4"},"commit":{"message":"Rename again correctly this time\n\nSigned-off-by: Rod Chapman <rodchap@amazon.com>","shortMessageHtmlLink":"Rename again correctly this time"}},{"before":"3e68b38386b8789c44b7a9bfc88e0c6f5993fb46","after":"15731a0885da30498a2de369b9965914735a5433","ref":"refs/heads/main","pushedAt":"2024-07-01T09:52:48.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rod-chapman","name":"Roderick Chapman","path":"/rod-chapman","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22537733?s=80&v=4"},"commit":{"message":"Rename directory to match actual issue number\n\nSigned-off-by: Rod Chapman <rodchap@amazon.com>","shortMessageHtmlLink":"Rename directory to match actual issue number"}},{"before":"4535f9a8295f84d99b0d1c79eae17ec195487b1e","after":"3e68b38386b8789c44b7a9bfc88e0c6f5993fb46","ref":"refs/heads/main","pushedAt":"2024-07-01T09:40:05.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rod-chapman","name":"Roderick Chapman","path":"/rod-chapman","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22537733?s=80&v=4"},"commit":{"message":"Add test case for this issue\n\nSigned-off-by: Rod Chapman <rodchap@amazon.com>","shortMessageHtmlLink":"Add test case for this issue"}},{"before":"823a7094e9dfa3426b1892aa364bdc5febbdf28b","after":"4535f9a8295f84d99b0d1c79eae17ec195487b1e","ref":"refs/heads/main","pushedAt":"2024-06-28T09:53:29.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rod-chapman","name":"Roderick Chapman","path":"/rod-chapman","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22537733?s=80&v=4"},"commit":{"message":"Change to disjunctive form ensures clause for constant_time_equals_total()\n\nSigned-off-by: Rod Chapman <rodchap@amazon.com>","shortMessageHtmlLink":"Change to disjunctive form ensures clause for constant_time_equals_to…"}},{"before":"b8d5caf4fb39148084511200e1676615e91aefea","after":"823a7094e9dfa3426b1892aa364bdc5febbdf28b","ref":"refs/heads/main","pushedAt":"2024-06-26T10:49:23.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rod-chapman","name":"Roderick Chapman","path":"/rod-chapman","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22537733?s=80&v=4"},"commit":{"message":"Add zero_slice() functions and its proof\n\nSigned-off-by: Rod Chapman <rodchap@amazon.com>","shortMessageHtmlLink":"Add zero_slice() functions and its proof"}},{"before":"6d605d95e8771deb9091a7eaaaf0ea640eaa02f7","after":"b8d5caf4fb39148084511200e1676615e91aefea","ref":"refs/heads/main","pushedAt":"2024-06-26T10:40:05.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rod-chapman","name":"Roderick Chapman","path":"/rod-chapman","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22537733?s=80&v=4"},"commit":{"message":"Update quantified variable name to be compatible with CBMC 6.0.0\n\nSigned-off-by: Rod Chapman <rodchap@amazon.com>","shortMessageHtmlLink":"Update quantified variable name to be compatible with CBMC 6.0.0"}},{"before":"237838ffd188c31326445234df05c52e585eca07","after":"6d605d95e8771deb9091a7eaaaf0ea640eaa02f7","ref":"refs/heads/main","pushedAt":"2024-06-17T18:55:24.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rod-chapman","name":"Roderick Chapman","path":"/rod-chapman","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22537733?s=80&v=4"},"commit":{"message":"Add init_st() function and its proof. Demonstrates bug.\n\nSigned-off-by: Rod Chapman <rodchap@amazon.com>","shortMessageHtmlLink":"Add init_st() function and its proof. Demonstrates bug."}},{"before":"b412c3f879d9c9a14ca3e110c6019973112b78a7","after":"237838ffd188c31326445234df05c52e585eca07","ref":"refs/heads/main","pushedAt":"2024-06-14T11:36:19.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rod-chapman","name":"Roderick Chapman","path":"/rod-chapman","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22537733?s=80&v=4"},"commit":{"message":"Corrections to ctunpad() to return a value. Adds correct calls flag in Makefile. Proof now OK\n\nSigned-off-by: Rod Chapman <rodchap@amazon.com>","shortMessageHtmlLink":"Corrections to ctunpad() to return a value. Adds correct calls flag i…"}},{"before":"830584b0862e108c489da5232756c7da755ac8c3","after":"b412c3f879d9c9a14ca3e110c6019973112b78a7","ref":"refs/heads/main","pushedAt":"2024-06-14T11:20:28.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"rod-chapman","name":"Roderick Chapman","path":"/rod-chapman","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22537733?s=80&v=4"},"commit":{"message":"Correct assigns contract for lopp in ctcc() function. Proof now OK.\n\nSigned-off-by: Rod Chapman <rodchap@amazon.com>","shortMessageHtmlLink":"Correct assigns contract for lopp in ctcc() function. Proof now OK."}},{"before":"6db129311078608297e10edb310cf6d8a091fbca","after":"830584b0862e108c489da5232756c7da755ac8c3","ref":"refs/heads/main","pushedAt":"2024-06-07T13:02:09.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rod-chapman","name":"Roderick Chapman","path":"/rod-chapman","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22537733?s=80&v=4"},"commit":{"message":"Add CBMC on-screen logs for reference.","shortMessageHtmlLink":"Add CBMC on-screen logs for reference."}},{"before":"88e53a7f2700a8dca24e7b14435fa52e528c5428","after":"6db129311078608297e10edb310cf6d8a091fbca","ref":"refs/heads/main","pushedAt":"2024-06-07T12:07:09.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"rod-chapman","name":"Roderick Chapman","path":"/rod-chapman","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22537733?s=80&v=4"},"commit":{"message":"Add Simple example to contrast CBMC with SPARK Pro","shortMessageHtmlLink":"Add Simple example to contrast CBMC with SPARK Pro"}},{"before":"46b25301e01d8e51d6e8803a2a2454b1f5062421","after":"88e53a7f2700a8dca24e7b14435fa52e528c5428","ref":"refs/heads/main","pushedAt":"2024-05-24T16:14:31.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rod-chapman","name":"Roderick Chapman","path":"/rod-chapman","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22537733?s=80&v=4"},"commit":{"message":"Add constant time conditional copy ctcc() function and harness","shortMessageHtmlLink":"Add constant time conditional copy ctcc() function and harness"}},{"before":"756b95a1c1c9a01a9e7291694f8f791f34dea9a9","after":"46b25301e01d8e51d6e8803a2a2454b1f5062421","ref":"refs/heads/main","pushedAt":"2024-05-24T12:48:23.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rod-chapman","name":"Roderick Chapman","path":"/rod-chapman","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22537733?s=80&v=4"},"commit":{"message":"Add constant_time_equals_total","shortMessageHtmlLink":"Add constant_time_equals_total"}},{"before":"52d6ddeb15a23ed75802b15f69611dc735b6fe78","after":"756b95a1c1c9a01a9e7291694f8f791f34dea9a9","ref":"refs/heads/main","pushedAt":"2024-05-24T12:09:45.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rod-chapman","name":"Roderick Chapman","path":"/rod-chapman","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22537733?s=80&v=4"},"commit":{"message":"Revert to original and achieves full proof with newest CBMC 6.0.0 on 24th May","shortMessageHtmlLink":"Revert to original and achieves full proof with newest CBMC 6.0.0 on …"}},{"before":"20a559b99287945ab8a390689b14fb35316ea882","after":"52d6ddeb15a23ed75802b15f69611dc735b6fe78","ref":"refs/heads/main","pushedAt":"2024-05-21T06:40:53.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"rod-chapman","name":"Roderick Chapman","path":"/rod-chapman","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22537733?s=80&v=4"},"commit":{"message":"Switch to negative logic to avoid == operator on Boolean, and introduce decreases clause for the loop.","shortMessageHtmlLink":"Switch to negative logic to avoid == operator on Boolean, and introdu…"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEtZ_bgQA","startCursor":null,"endCursor":null}},"title":"Activity · rod-chapman/cbmc-examples"}