{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":286755310,"defaultBranch":"master","name":"VerifiableP4","ownerLogin":"verified-network-toolchain","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2020-08-11T13:42:52.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/79861588?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1676935209.810849","currentOid":""},"activityList":{"items":[{"before":"652e2508723f27a266daa466a5d9cebf08845090","after":"e5c63a5f081f174e5cd99876d3dfb780675702c4","ref":"refs/heads/master","pushedAt":"2024-07-15T20:41:05.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"txyyss","name":"Shengyi Wang","path":"/txyyss","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/761426?s=80&v=4"},"commit":{"message":"refactor: rename traffic_manager to replication_engine.","shortMessageHtmlLink":"refactor: rename traffic_manager to replication_engine."}},{"before":"2753873a07a1af389e51997e455d9d3b22e103f5","after":"652e2508723f27a266daa466a5d9cebf08845090","ref":"refs/heads/master","pushedAt":"2024-07-09T20:26:29.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"txyyss","name":"Shengyi Wang","path":"/txyyss","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/761426?s=80&v=4"},"commit":{"message":"feat: add lemma hoare_stmt_post_perm as an ad hoc fixing.","shortMessageHtmlLink":"feat: add lemma hoare_stmt_post_perm as an ad hoc fixing."}},{"before":"312dd6ccc6119f881762ccab4a4a7bd86638877e","after":"2753873a07a1af389e51997e455d9d3b22e103f5","ref":"refs/heads/master","pushedAt":"2024-06-11T12:41:21.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"txyyss","name":"Shengyi Wang","path":"/txyyss","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/761426?s=80&v=4"},"commit":{"message":"feat: change the content of sbf_gen and generate the P4light file.","shortMessageHtmlLink":"feat: change the content of sbf_gen and generate the P4light file."}},{"before":"2cb686dececd38f14c150ed49c72febeefb3d0dd","after":"312dd6ccc6119f881762ccab4a4a7bd86638877e","ref":"refs/heads/master","pushedAt":"2024-06-10T13:02:06.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"txyyss","name":"Shengyi Wang","path":"/txyyss","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/761426?s=80&v=4"},"commit":{"message":"feat: define another property relying only on no packet duplication.","shortMessageHtmlLink":"feat: define another property relying only on no packet duplication."}},{"before":"343d2abe71595c67f466e243f9629575d27d4e48","after":"2cb686dececd38f14c150ed49c72febeefb3d0dd","ref":"refs/heads/master","pushedAt":"2024-06-10T11:37:09.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"txyyss","name":"Shengyi Wang","path":"/txyyss","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/761426?s=80&v=4"},"commit":{"message":"feat: define and proved just another weaker property.","shortMessageHtmlLink":"feat: define and proved just another weaker property."}},{"before":"00afae84c5c6a4d532ccee03bad8cf7c2f444011","after":"343d2abe71595c67f466e243f9629575d27d4e48","ref":"refs/heads/master","pushedAt":"2024-06-05T14:20:56.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"txyyss","name":"Shengyi Wang","path":"/txyyss","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/761426?s=80&v=4"},"commit":{"message":"feat: proved another derived weaker property.","shortMessageHtmlLink":"feat: proved another derived weaker property."}},{"before":"c2ee4478d7a282503953c395db1bcd3374e3dc3e","after":"00afae84c5c6a4d532ccee03bad8cf7c2f444011","ref":"refs/heads/master","pushedAt":"2024-05-16T03:31:20.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"txyyss","name":"Shengyi Wang","path":"/txyyss","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/761426?s=80&v=4"},"commit":{"message":"feat: prove pout is unique for special switch packet relation.","shortMessageHtmlLink":"feat: prove pout is unique for special switch packet relation."}},{"before":"84f466f291bfda0f5e924db1bc9724fb7a6e7530","after":"c2ee4478d7a282503953c395db1bcd3374e3dc3e","ref":"refs/heads/master","pushedAt":"2024-05-15T12:01:00.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"txyyss","name":"Shengyi Wang","path":"/txyyss","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/761426?s=80&v=4"},"commit":{"message":"feat: enhanced packet_ingress_relation.","shortMessageHtmlLink":"feat: enhanced packet_ingress_relation."}},{"before":"0ec5302cbc2ef09c16e1d70d8b9f9bdd755e4e4c","after":"84f466f291bfda0f5e924db1bc9724fb7a6e7530","ref":"refs/heads/master","pushedAt":"2024-05-15T11:44:57.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"txyyss","name":"Shengyi Wang","path":"/txyyss","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/761426?s=80&v=4"},"commit":{"message":"feat: enhanced the lemma ethernet_extract_result_hdr","shortMessageHtmlLink":"feat: enhanced the lemma ethernet_extract_result_hdr"}},{"before":"312a47c5e1a52639d360036e94b3a9c16bf54247","after":"0ec5302cbc2ef09c16e1d70d8b9f9bdd755e4e4c","ref":"refs/heads/master","pushedAt":"2024-05-15T11:13:36.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"txyyss","name":"Shengyi Wang","path":"/txyyss","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/761426?s=80&v=4"},"commit":{"message":"feat: proved the pout is unique for normal packet relation.","shortMessageHtmlLink":"feat: proved the pout is unique for normal packet relation."}},{"before":"d3d8403e918dfb34048183c6ddd3b0814f505333","after":"312a47c5e1a52639d360036e94b3a9c16bf54247","ref":"refs/heads/master","pushedAt":"2024-05-12T08:24:24.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"txyyss","name":"Shengyi Wang","path":"/txyyss","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/761426?s=80&v=4"},"commit":{"message":"feat: define and prove two more weaker properties from the ideal one.","shortMessageHtmlLink":"feat: define and prove two more weaker properties from the ideal one."}},{"before":"373b1ab29a3b05718ffb7f9bc06bba9d38148fb1","after":"d3d8403e918dfb34048183c6ddd3b0814f505333","ref":"refs/heads/master","pushedAt":"2024-05-12T03:48:27.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"txyyss","name":"Shengyi Wang","path":"/txyyss","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/761426?s=80&v=4"},"commit":{"message":"feat: derived the queue length property from the ideal property.","shortMessageHtmlLink":"feat: derived the queue length property from the ideal property."}},{"before":"bf25cc87ea790d6aa30348d6bb98f6c421804c0e","after":"373b1ab29a3b05718ffb7f9bc06bba9d38148fb1","ref":"refs/heads/master","pushedAt":"2024-05-11T14:11:41.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"txyyss","name":"Shengyi Wang","path":"/txyyss","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/761426?s=80&v=4"},"commit":{"message":"feat: proved the precise property is strong enough to derive others.","shortMessageHtmlLink":"feat: proved the precise property is strong enough to derive others."}},{"before":"9065a0201af61c1cfc679ad6d1a51c0ef1b294a6","after":"bf25cc87ea790d6aa30348d6bb98f6c421804c0e","ref":"refs/heads/master","pushedAt":"2024-05-10T12:40:15.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"txyyss","name":"Shengyi Wang","path":"/txyyss","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/761426?s=80&v=4"},"commit":{"message":"feat: define and proved the precise property of switch queues.","shortMessageHtmlLink":"feat: define and proved the precise property of switch queues."}},{"before":"306383faf971c3b0d01128ad0f1d776ce02e2ea5","after":"9065a0201af61c1cfc679ad6d1a51c0ef1b294a6","ref":"refs/heads/master","pushedAt":"2024-04-27T04:22:25.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"txyyss","name":"Shengyi Wang","path":"/txyyss","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/761426?s=80&v=4"},"commit":{"message":"feat: prove another queue property of the whole switch.","shortMessageHtmlLink":"feat: prove another queue property of the whole switch."}},{"before":"ce3a6374b640afe8e6f6a84a1e337b73ffc26866","after":"306383faf971c3b0d01128ad0f1d776ce02e2ea5","ref":"refs/heads/master","pushedAt":"2024-04-27T03:06:47.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"txyyss","name":"Shengyi Wang","path":"/txyyss","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/761426?s=80&v=4"},"commit":{"message":"feat: proved normal packet property for the whole switch.","shortMessageHtmlLink":"feat: proved normal packet property for the whole switch."}},{"before":"322f7edd5eab50577c1e71f6544fe01f3eda53d9","after":"ce3a6374b640afe8e6f6a84a1e337b73ffc26866","ref":"refs/heads/master","pushedAt":"2024-04-23T20:44:55.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"txyyss","name":"Shengyi Wang","path":"/txyyss","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/761426?s=80&v=4"},"commit":{"message":"feat: proved two content related properties of packet queues.","shortMessageHtmlLink":"feat: proved two content related properties of packet queues."}},{"before":"79fc126fe1935ee142a075180d67d7b15df5830b","after":"322f7edd5eab50577c1e71f6544fe01f3eda53d9","ref":"refs/heads/master","pushedAt":"2024-04-19T18:44:27.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"txyyss","name":"Shengyi Wang","path":"/txyyss","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/761426?s=80&v=4"},"commit":{"message":"feat: improve packet_ingress_relation and proofs by an auto tactic.","shortMessageHtmlLink":"feat: improve packet_ingress_relation and proofs by an auto tactic."}},{"before":"5aaab71f43586582c97fe43744ea728892a317de","after":"79fc126fe1935ee142a075180d67d7b15df5830b","ref":"refs/heads/master","pushedAt":"2024-04-18T23:24:03.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"txyyss","name":"Shengyi Wang","path":"/txyyss","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/761426?s=80&v=4"},"commit":{"message":"feat: turn egress pipeline lemmas into explicit form.","shortMessageHtmlLink":"feat: turn egress pipeline lemmas into explicit form."}},{"before":"e5ea530b7a352d218083ac496ac12655ead23e20","after":"5aaab71f43586582c97fe43744ea728892a317de","ref":"refs/heads/master","pushedAt":"2024-04-17T20:45:56.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"txyyss","name":"Shengyi Wang","path":"/txyyss","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/761426?s=80&v=4"},"commit":{"message":"feat: turn some implicit existential lemmas into explicit forms.","shortMessageHtmlLink":"feat: turn some implicit existential lemmas into explicit forms."}},{"before":"768a45abc2483a1973528dd0f384c3c98152a4a4","after":"e5ea530b7a352d218083ac496ac12655ead23e20","ref":"refs/heads/master","pushedAt":"2024-04-15T14:50:16.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"txyyss","name":"Shengyi Wang","path":"/txyyss","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/761426?s=80&v=4"},"commit":{"message":"feat: more tactic, improved theorem statement for ingress pipeline.","shortMessageHtmlLink":"feat: more tactic, improved theorem statement for ingress pipeline."}},{"before":"8db0241b8f30e92ad2d56dee8416071205fffa9c","after":"768a45abc2483a1973528dd0f384c3c98152a4a4","ref":"refs/heads/master","pushedAt":"2024-04-12T02:26:38.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"txyyss","name":"Shengyi Wang","path":"/txyyss","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/761426?s=80&v=4"},"commit":{"message":"feat: Improve parser verification by new tactics.","shortMessageHtmlLink":"feat: Improve parser verification by new tactics."}},{"before":"1c1b5320aa3ad36c583605ef973aa13125c207eb","after":"8db0241b8f30e92ad2d56dee8416071205fffa9c","ref":"refs/heads/master","pushedAt":"2024-01-22T17:02:39.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"MollyDream","name":"Molly Pan","path":"/MollyDream","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32046020?s=80&v=4"},"commit":{"message":"add the pkt generator code","shortMessageHtmlLink":"add the pkt generator code"}},{"before":"2d96a92451b8844bf9fe55d8e17887b3b7779a8d","after":"1c1b5320aa3ad36c583605ef973aa13125c207eb","ref":"refs/heads/master","pushedAt":"2023-12-22T20:36:20.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"txyyss","name":"Shengyi Wang","path":"/txyyss","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/761426?s=80&v=4"},"commit":{"message":"feat: verified the ingress parser of sbf.","shortMessageHtmlLink":"feat: verified the ingress parser of sbf."}},{"before":"8311d4eb409687277fc671f68369be37fff82f1b","after":"2d96a92451b8844bf9fe55d8e17887b3b7779a8d","ref":"refs/heads/master","pushedAt":"2023-11-16T21:38:36.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"txyyss","name":"Shengyi Wang","path":"/txyyss","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/761426?s=80&v=4"},"commit":{"message":"comment out the test case.","shortMessageHtmlLink":"comment out the test case."}},{"before":"89b650a27c7fe403de10a46c883197bd849888a0","after":"8311d4eb409687277fc671f68369be37fff82f1b","ref":"refs/heads/master","pushedAt":"2023-11-16T16:01:43.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"txyyss","name":"Shengyi Wang","path":"/txyyss","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/761426?s=80&v=4"},"commit":{"message":"One more helper about mask.","shortMessageHtmlLink":"One more helper about mask."}},{"before":"d16380b1a1e655195ca59581003c2cba1195974c","after":"89b650a27c7fe403de10a46c883197bd849888a0","ref":"refs/heads/master","pushedAt":"2023-11-15T19:51:42.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"txyyss","name":"Shengyi Wang","path":"/txyyss","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/761426?s=80&v=4"},"commit":{"message":"Reprove the queue length theorem.","shortMessageHtmlLink":"Reprove the queue length theorem."}},{"before":"bdcdeef1d1d68aa6cddb5639e90aa10d3e93d9ba","after":"d16380b1a1e655195ca59581003c2cba1195974c","ref":"refs/heads/master","pushedAt":"2023-11-14T19:10:59.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"txyyss","name":"Shengyi Wang","path":"/txyyss","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/761426?s=80&v=4"},"commit":{"message":"Proved the queue theorem","shortMessageHtmlLink":"Proved the queue theorem"}},{"before":"c8ad34259c4fa7571d86706e17dacb568b86c982","after":"bdcdeef1d1d68aa6cddb5639e90aa10d3e93d9ba","ref":"refs/heads/master","pushedAt":"2023-11-13T21:19:27.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"txyyss","name":"Shengyi Wang","path":"/txyyss","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/761426?s=80&v=4"},"commit":{"message":"Some progress in proving the final theorem.","shortMessageHtmlLink":"Some progress in proving the final theorem."}},{"before":"797a6d072aa2b93ab7ad3fbc7c983c9c39e515e5","after":"c8ad34259c4fa7571d86706e17dacb568b86c982","ref":"refs/heads/master","pushedAt":"2023-11-07T21:44:42.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"txyyss","name":"Shengyi Wang","path":"/txyyss","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/761426?s=80&v=4"},"commit":{"message":"finished the proof of output format spec\n\nof the whole ingress pipeline.","shortMessageHtmlLink":"finished the proof of output format spec"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEgBv_UwA","startCursor":null,"endCursor":null}},"title":"Activity · verified-network-toolchain/VerifiableP4"}