{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":485864071,"defaultBranch":"master","name":"VerifiedSCION","ownerLogin":"viperproject","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2022-04-26T16:25:37.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/19855605?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1726733522.0","currentOid":""},"activityList":{"items":[{"before":null,"after":"b34186e35ae2eb35309c977f45d8e9e78b53b77f","ref":"refs/heads/joao-crypto-weaken","pushedAt":"2024-09-19T08:12:02.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"jcp19","name":"João Pereira","path":"/jcp19","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6281876?s=80&v=4"},"commit":{"message":"backup","shortMessageHtmlLink":"backup"}},{"before":"32791d60a29fa817f4b3c768b21a5c4ef365b79f","after":null,"ref":"refs/heads/fix-missing-ghost","pushedAt":"2024-09-16T13:13:02.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"jcp19","name":"João Pereira","path":"/jcp19","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6281876?s=80&v=4"}},{"before":"b1055a945dcff16dcaf7d74f3d4cce661c1bc444","after":"2aebfb2511c2a927cd97c2cd89cc031b76ffc5c6","ref":"refs/heads/master","pushedAt":"2024-09-16T13:13:00.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"jcp19","name":"João Pereira","path":"/jcp19","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6281876?s=80&v=4"},"commit":{"message":"add missing 'ghost' (#377)","shortMessageHtmlLink":"add missing 'ghost' (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2519672600\" data-permission-text=\"Title is private\" data-url=\"https://github.com/viperproject/VerifiedSCION/issues/377\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/viperproject/VerifiedSCION/pull/377/hovercard\" href=\"https://github.com/viperproject/VerifiedSCION/pull/377\">#377</a>)"}},{"before":"ef446591b24670a5c37119c2224bedb955cf4a69","after":"32791d60a29fa817f4b3c768b21a5c4ef365b79f","ref":"refs/heads/fix-missing-ghost","pushedAt":"2024-09-16T08:25:29.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"jcp19","name":"João Pereira","path":"/jcp19","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6281876?s=80&v=4"},"commit":{"message":"Merge branch 'master' into fix-missing-ghost","shortMessageHtmlLink":"Merge branch 'master' into fix-missing-ghost"}},{"before":"5575874f093029269918776d00cd9a88fa7a335a","after":null,"ref":"refs/heads/fmtAS","pushedAt":"2024-09-16T08:20:10.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"jcp19","name":"João Pereira","path":"/jcp19","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6281876?s=80&v=4"}},{"before":"12552e86e7b6f81003fca7887b13fc57cf211764","after":"b1055a945dcff16dcaf7d74f3d4cce661c1bc444","ref":"refs/heads/master","pushedAt":"2024-09-16T08:20:08.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"jcp19","name":"João Pereira","path":"/jcp19","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6281876?s=80&v=4"},"commit":{"message":"Verify `fmtAS` (#378)\n\n* fmtAS\r\n\r\n* tiny changes\r\n\r\n* tiny changes\r\n\r\n* Apply suggestions from code review","shortMessageHtmlLink":"Verify <code>fmtAS</code> (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2527044676\" data-permission-text=\"Title is private\" data-url=\"https://github.com/viperproject/VerifiedSCION/issues/378\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/viperproject/VerifiedSCION/pull/378/hovercard\" href=\"https://github.com/viperproject/VerifiedSCION/pull/378\">#378</a>)"}},{"before":"70855bc26aa0e92cf9a2f209f93450bbc6f0692e","after":"5575874f093029269918776d00cd9a88fa7a335a","ref":"refs/heads/fmtAS","pushedAt":"2024-09-16T08:19:41.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jcp19","name":"João Pereira","path":"/jcp19","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6281876?s=80&v=4"},"commit":{"message":"Apply suggestions from code review","shortMessageHtmlLink":"Apply suggestions from code review"}},{"before":"2ec5a3bc1c8f4bf5539e081ae91d4b137fe15961","after":"70855bc26aa0e92cf9a2f209f93450bbc6f0692e","ref":"refs/heads/fmtAS","pushedAt":"2024-09-15T19:19:54.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jcp19","name":"João Pereira","path":"/jcp19","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6281876?s=80&v=4"},"commit":{"message":"tiny changes","shortMessageHtmlLink":"tiny changes"}},{"before":"925889d60d3039670daadb9c1a65c215c373df72","after":"2ec5a3bc1c8f4bf5539e081ae91d4b137fe15961","ref":"refs/heads/fmtAS","pushedAt":"2024-09-15T19:18:54.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jcp19","name":"João Pereira","path":"/jcp19","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6281876?s=80&v=4"},"commit":{"message":"tiny changes","shortMessageHtmlLink":"tiny changes"}},{"before":null,"after":"925889d60d3039670daadb9c1a65c215c373df72","ref":"refs/heads/fmtAS","pushedAt":"2024-09-15T17:15:53.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"jcp19","name":"João Pereira","path":"/jcp19","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6281876?s=80&v=4"},"commit":{"message":"fmtAS","shortMessageHtmlLink":"fmtAS"}},{"before":"3d041c4dacfd152caaa6a72f91eecd743c91f2fe","after":"b26935fabda33b5846e55c4bdce74e1900766706","ref":"refs/heads/remove-ubs","pushedAt":"2024-09-11T18:03:56.000Z","pushType":"push","commitsCount":8,"pusher":{"login":"jcp19","name":"João Pereira","path":"/jcp19","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6281876?s=80&v=4"},"commit":{"message":"Merge branch 'master' into remove-ubs","shortMessageHtmlLink":"Merge branch 'master' into remove-ubs"}},{"before":"471b4d777ba4a08024a35c94dfc4361536240487","after":"68e566c8526231b79e9d79fe04569f281795be31","ref":"refs/heads/temp","pushedAt":"2024-09-11T18:03:10.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"jcp19","name":"João Pereira","path":"/jcp19","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6281876?s=80&v=4"},"commit":{"message":"Merge branch 'master' into temp","shortMessageHtmlLink":"Merge branch 'master' into temp"}},{"before":"160794d88974dee94f464a2feae4d64f2b631dc9","after":"ef446591b24670a5c37119c2224bedb955cf4a69","ref":"refs/heads/fix-missing-ghost","pushedAt":"2024-09-11T18:03:00.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"jcp19","name":"João Pereira","path":"/jcp19","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6281876?s=80&v=4"},"commit":{"message":"Merge branch 'master' into fix-missing-ghost","shortMessageHtmlLink":"Merge branch 'master' into fix-missing-ghost"}},{"before":"d8284c189c07638ecbd81a657171715680badbb1","after":null,"ref":"refs/heads/jcp19-patch-upload-action","pushedAt":"2024-09-11T18:02:40.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"jcp19","name":"João Pereira","path":"/jcp19","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6281876?s=80&v=4"}},{"before":"68b984b42688c192338c3fdf3bad8da64576c3b5","after":"12552e86e7b6f81003fca7887b13fc57cf211764","ref":"refs/heads/master","pushedAt":"2024-09-11T18:02:38.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"jcp19","name":"João Pereira","path":"/jcp19","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6281876?s=80&v=4"},"commit":{"message":"Fix failing CI due to outdated upload action (#376)","shortMessageHtmlLink":"Fix failing CI due to outdated upload action (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2519640942\" data-permission-text=\"Title is private\" data-url=\"https://github.com/viperproject/VerifiedSCION/issues/376\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/viperproject/VerifiedSCION/pull/376/hovercard\" href=\"https://github.com/viperproject/VerifiedSCION/pull/376\">#376</a>)"}},{"before":null,"after":"160794d88974dee94f464a2feae4d64f2b631dc9","ref":"refs/heads/fix-missing-ghost","pushedAt":"2024-09-11T12:54:05.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"jcp19","name":"João Pereira","path":"/jcp19","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6281876?s=80&v=4"},"commit":{"message":"add missing 'ghost'","shortMessageHtmlLink":"add missing 'ghost'"}},{"before":null,"after":"d8284c189c07638ecbd81a657171715680badbb1","ref":"refs/heads/jcp19-patch-upload-action","pushedAt":"2024-09-11T12:40:47.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"jcp19","name":"João Pereira","path":"/jcp19","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6281876?s=80&v=4"},"commit":{"message":"Fix failing CI due to outdated upload action","shortMessageHtmlLink":"Fix failing CI due to outdated upload action"}},{"before":"9b2011ef175f5e680ea2c527b6acd755707d0960","after":"471b4d777ba4a08024a35c94dfc4361536240487","ref":"refs/heads/temp","pushedAt":"2024-09-11T12:35:13.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Dspil","name":"Dionysios Spiliopoulos","path":"/Dspil","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32896454?s=80&v=4"},"commit":{"message":"scripts","shortMessageHtmlLink":"scripts"}},{"before":null,"after":"9b2011ef175f5e680ea2c527b6acd755707d0960","ref":"refs/heads/temp","pushedAt":"2024-09-05T14:36:25.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"Dspil","name":"Dionysios Spiliopoulos","path":"/Dspil","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32896454?s=80&v=4"},"commit":{"message":"Merge branch 'master' into temp","shortMessageHtmlLink":"Merge branch 'master' into temp"}},{"before":"1a2cb298cee0411fdd12fcf3c5cb498ea3b45d26","after":null,"ref":"refs/heads/markus-epic","pushedAt":"2024-08-29T20:35:52.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"jcp19","name":"João Pereira","path":"/jcp19","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6281876?s=80&v=4"}},{"before":"c6f1d95c1057ba99a9a8b8ebc59f1795cceb2505","after":"f0da265639e0f093d9066f610c149244ef602ae8","ref":"refs/heads/joao-epic","pushedAt":"2024-08-29T20:35:50.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"jcp19","name":"João Pereira","path":"/jcp19","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6281876?s=80&v=4"},"commit":{"message":"processEpic Continued (#371)\n\n* Undo workaround with short-circuiting operations (#269)\r\n\r\n* redo short-circuiting operations\r\n\r\n* Undo change\r\n\r\n* Update router/dataplane.go\r\n\r\n* increase timeout for epic (#278)\r\n\r\n* experiment with disabling NL (#265)\r\n\r\n* experiment with disabling NL\r\n\r\n* enable the wildcard optimization for when NL is disabled\r\n\r\n* Apply suggestions from code review\r\n\r\n* Drop unnecessary annotations in `Run` (#279)\r\n\r\n* drop unnecessary annotations\r\n\r\n* fix precond error\r\n\r\n* fix verification error\r\n\r\n* cleanup\r\n\r\n* fix tiny error\r\n\r\n* bring changes to the io spec to speed things a little (#281)\r\n\r\n* Add config for overflow in the CI (#247)\r\n\r\n* start overflow checking\r\n\r\n* backup\r\n\r\n* fix flags\r\n\r\n* Apply suggestions from code review\r\n\r\n* disable checks in all packages for now\r\n\r\n* Update .github/workflows/gobra.yml\r\n\r\n* Reduce permission amount to buffer for decodeFromLayers (#285)\r\n\r\n* R40\r\n\r\n* epic\r\n\r\n* extn\r\n\r\n* onehop\r\n\r\n* reduce permission amount of decode layers\r\n\r\n* cosmetic changes (#286)\r\n\r\n* Fix warning in the CI (#288)\r\n\r\n* Update gobra.yml to disableNL (#289)\r\n\r\n* simplify Decoded.Reverse (#295)\r\n\r\n* Cherry-pick #4483 from `scionproto/scion` (#292)\r\n\r\n* cherry-pick 4483\r\n\r\n* undo change to test due to the use of (yet) undefined symbols\r\n\r\n* fix verification error\r\n\r\n---------\r\n\r\nCo-authored-by: jiceatscion <139873336+jiceatscion@users.noreply.github.com>\r\n\r\n* change permissions amount for decode SCMPTraceRoute (#299)\r\n\r\n* First batch of changes from PR #248 (#306)\r\n\r\n* first batch of changes from the IO spec\r\n\r\n* Apply suggestions from code review\r\n\r\n* adapt config options\r\n\r\n* Add checks for termination modulo blocking (#309)\r\n\r\n* add termination checking if we ignore locking\r\n\r\n* add termination checks modulo locking\r\n\r\n* backup\r\n\r\n* fix termination measure\r\n\r\n* fix verification errors\r\n\r\n* fix verification error\r\n\r\n* Verify the IO behavior (a.k.a., basis PR) (#248)\r\n\r\n* manually trigger workflow\r\n\r\n* manually trigger workflow\r\n\r\n* raw byte to spec for segments and hopfields\r\n\r\n* bugfix\r\n\r\n* import fix\r\n\r\n* bugfix after gobra update\r\n\r\n* spec to pkt (currSeg)\r\n\r\n* spec to pkt (left, mid, right)\r\n\r\n* spec to pkt (termination)\r\n\r\n* code clean up\r\n\r\n* clean up\r\n\r\n* improvements\r\n\r\n* instantiate abstract functions with bodies\r\n\r\n* progress io spec\r\n\r\n* formatting\r\n\r\n* specification fixes\r\n\r\n* IO-spec to pkt rewritten\r\n\r\n* clean up\r\n\r\n* improve readability\r\n\r\n* rename of function lengthOfCurrSeg\r\n\r\n* extract asid-seqence from raw pkt\r\n\r\n* missing trigger\r\n\r\n* quick fix\r\n\r\n* Update router/dataplane_spec.gobra\r\n\r\nCo-authored-by: Dionysios Spiliopoulos <32896454+Dspil@users.noreply.github.com>\r\n\r\n* Apply suggestions from code review\r\n\r\nCo-authored-by: João Pereira <joaopereira.19@gmail.com>\r\n\r\n* readability improvements\r\n\r\n* further improvements\r\n\r\n* replace 4 by its constant InfoLen\r\n\r\n* readability improvement\r\n\r\n* constant for metaLen in package path\r\n\r\n* Update router/io-spec.gobra\r\n\r\nCo-authored-by: João Pereira <joaopereira.19@gmail.com>\r\n\r\n* minor improvements\r\n\r\n* move validMetaLenInPath() to test file\r\n\r\n* io-spec in Run\r\n\r\n* add body to absIO_val\r\n\r\n* fix merge mistake\r\n\r\n* fix merge mistake\r\n\r\n* fix typo\r\n\r\n* io-spec skeleton for processPkt and processSCION\r\n\r\n* import fix\r\n\r\n* Update router/io-spec.gobra\r\n\r\n* unit\r\n\r\n* well formdness\r\n\r\n* relate dataplane with dataplaneSpec\r\n\r\n* various fixes\r\n\r\n* Update verification/io/values.gobra\r\n\r\n* permission fix for dpSpecWellConfigured\r\n\r\n* permission fix in rc\r\n\r\n* fix verification error\r\n\r\n* dp.Valid() as opaque\r\n\r\n* backup\r\n\r\n* format spacing\r\n\r\n* improve perf; drop assumption\r\n\r\n* fix formatting\r\n\r\n* Update router/dataplane.go\r\n\r\n* formatting postconditions of processPkt, processSCION\r\n\r\n* fix extra permission\r\n\r\n* typo\r\n\r\n* processSCION had the same issue\r\n\r\n* ingressID is preseved intead of sInit\r\n\r\n* Revert \"ingressID is preseved intead of sInit\"\r\n\r\nThis reverts commit 88db3fdf804c7dbd9252b5db8b485287b7ca0905.\r\n\r\n* Revert \"processSCION had the same issue\"\r\n\r\nThis reverts commit 71aadfe5e248c5640c816988f124b31841333d09.\r\n\r\n* Updated IO-Spec-Function to Correlate Bytes with Terms (#262)\r\n\r\n* fixes in the asid extraction functions\r\n\r\n* pre-/postconditions for process\r\n\r\n* fix formatting\r\n\r\n* fix same issue in processSCION\r\n\r\n* fix var names\r\n\r\n* precondition changes in hopfield and asidFromIfs\r\n\r\n* prostcondition fix in process and processSCION\r\n\r\n* update imports links\r\n\r\n* Apply suggestions from code review\r\n\r\n---------\r\n\r\nCo-authored-by: Dspil <dennisspiliopoylos@gmail.com>\r\nCo-authored-by: João Pereira <joaopereira.19@gmail.com>\r\n\r\n* made absIO_val opaque\r\n\r\n* use artificial triggers for quantifiers inside IO resources (#280)\r\n\r\n* AbsPkt improvements (#270)\r\n\r\n* absPkt opaque and other improvements\r\n\r\n* quick fixes\r\n\r\n* changed permission from R55 to R56\r\n\r\n* added missing permission amount in ReadBatch\r\n\r\n* fixed pre/postconditions of processPkt, processSCION and process\r\n\r\n* fixed opaque format\r\n\r\n---------\r\n\r\nCo-authored-by: João Pereira <joaopereira.19@gmail.com>\r\n\r\n* Verify send guard in Run (#263)\r\n\r\n* remove send operation\r\n\r\n* lemma for smaller buffer result in same abstract pkt\r\n\r\n* progress send guard\r\n\r\n* progress send guard\r\n\r\n* Fix incompleteness and continue with send guard (#273)\r\n\r\n* backup\r\n\r\n* backup\r\n\r\n* backup\r\n\r\n* backup\r\n\r\n* backup\r\n\r\n* drop space\r\n\r\n* pick better triggers\r\n\r\n* add necessary lemma and call to it; contains an assume false that needs to be dropped\r\n\r\n* backup\r\n\r\n* backup\r\n\r\n* add missing loop invariant about ingressID\r\n\r\n* backup\r\n\r\n* backup\r\n\r\n* fix verification error\r\n\r\n* try out a simpler trigger\r\n\r\n* widen lemma for absIO_val (#268)\r\n\r\n* widen lemma for abspkt (non termianting)\r\n\r\n* abspkt proven\r\n\r\n* renamed io-spec-lemmas\r\n\r\n* io val also proven\r\n\r\n* cleanup\r\n\r\n* merged markus' abspkt improvements\r\n\r\n* consdir lemma\r\n\r\n* proved\r\n\r\n* reinstate lemma4\r\n\r\n* fix verification error\r\n\r\n* Simplify widen lemma from #268 (#282)\r\n\r\n* start simplifying\r\n\r\n* continue simplifying\r\n\r\n* continue simplifying stuff\r\n\r\n* continue simplifying\r\n\r\n* continue simplifying\r\n\r\n* simplify further\r\n\r\n* finish for now\r\n\r\n* Update router/io-spec.gobra\r\n\r\n---------\r\n\r\nCo-authored-by: João Pereira <joaopereira.19@gmail.com>\r\n\r\n* Continue send (#283)\r\n\r\n* widen lemma for abspkt (non termianting)\r\n\r\n* abspkt proven\r\n\r\n* renamed io-spec-lemmas\r\n\r\n* io val also proven\r\n\r\n* cleanup\r\n\r\n* merged markus' abspkt improvements\r\n\r\n* consdir lemma\r\n\r\n* proved\r\n\r\n* reinstate lemma4\r\n\r\n* fix verification error\r\n\r\n* Simplify widen lemma from #268 (#282)\r\n\r\n* start simplifying\r\n\r\n* continue simplifying\r\n\r\n* continue simplifying stuff\r\n\r\n* continue simplifying\r\n\r\n* continue simplifying\r\n\r\n* simplify further\r\n\r\n* finish for now\r\n\r\n* Update router/io-spec.gobra\r\n\r\n* finish send in Run\r\n\r\n* propagate changes to processSCION\r\n\r\n---------\r\n\r\nCo-authored-by: Dspil <dennisspiliopoylos@gmail.com>\r\n\r\n* backup\r\n\r\n* adapt to the new syntax of backend annotations\r\n\r\n* clean-up\r\n\r\n* changes according to feedback\r\n\r\n---------\r\n\r\nCo-authored-by: João Pereira <joaopereira.19@gmail.com>\r\nCo-authored-by: Dionysios Spiliopoulos <32896454+Dspil@users.noreply.github.com>\r\nCo-authored-by: Dspil <dennisspiliopoylos@gmail.com>\r\n\r\n* IO specification skeleton in process (#284)\r\n\r\n* absPkt opaque and other improvements\r\n\r\n* tests for local enter guard\r\n\r\n* new approach for absPkt\r\n\r\n* tests with GetIngressIDNotZero()\r\n\r\n* fix verification error\r\n\r\n* progress io-skeleton in process\r\n\r\n* progress Xover\r\n\r\n* progress io-spec skeleton in process\r\n\r\n* removed dulicate of lemma\r\n\r\n* fix verification error\r\n\r\n* removed old concurrency test\r\n\r\n* refactored absPkt\r\n\r\n* continue refactoring of absPkt\r\n\r\n* fixed postcondition in process\r\n\r\n* progress lemmas for io-spec\r\n\r\n* addressed feedback\r\n\r\n* progress in updateNonConsDirIngressSegID\r\n\r\n* fix verification errors\r\n\r\n* Prove IO lemmas in `path/scion` (#290)\r\n\r\n* try to prove lemma\r\n\r\n* backup\r\n\r\n* fix incompletness via additional lemma\r\n\r\n* fix verification error\r\n\r\n* fix verification errors and clean up\r\n\r\n* fix verification errors introduced in the latest changes to the PR\r\n\r\n* fix consistency error\r\n\r\n* add lemmas for updateNonConsDirIngressSegID()\r\n\r\n* Change to EQAbsHeader (#293)\r\n\r\n* changed EQAbsHeader\r\n\r\n* readbility improvements\r\n\r\n* progress in handleRouterAlerts methods\r\n\r\n* Fix verification errors in dependencies (#291)\r\n\r\n* backup\r\n\r\n* backup\r\n\r\n* backup\r\n\r\n* simplify Decoded.Reverse\r\n\r\n* clean-up\r\n\r\n* add section header\r\n\r\n* drop comment\r\n\r\n* fix  verification errors in processEgress and DoXover\r\naddressing feedback\r\nclean up\r\n\r\n---------\r\n\r\nCo-authored-by: João Pereira <joaopereira.19@gmail.com>\r\n\r\n* Add functional spec to `InfoField.SerializeTo` (#300)\r\n\r\n* absPkt opaque and other improvements\r\n\r\n* tests for local enter guard\r\n\r\n* new approach for absPkt\r\n\r\n* tests with GetIngressIDNotZero()\r\n\r\n* fix verification error\r\n\r\n* progress io-skeleton in process\r\n\r\n* progress Xover\r\n\r\n* progress io-spec skeleton in process\r\n\r\n* removed dulicate of lemma\r\n\r\n* fix verification error\r\n\r\n* removed old concurrency test\r\n\r\n* refactored absPkt\r\n\r\n* continue refactoring of absPkt\r\n\r\n* fixed postcondition in process\r\n\r\n* progress lemmas for io-spec\r\n\r\n* addressed feedback\r\n\r\n* progress in updateNonConsDirIngressSegID\r\n\r\n* fix verification errors\r\n\r\n* Prove IO lemmas in `path/scion` (#290)\r\n\r\n* try to prove lemma\r\n\r\n* backup\r\n\r\n* fix incompletness via additional lemma\r\n\r\n* fix verification error\r\n\r\n* fix verification errors and clean up\r\n\r\n* fix verification errors introduced in the latest changes to the PR\r\n\r\n* fix consistency error\r\n\r\n* add lemmas for updateNonConsDirIngressSegID()\r\n\r\n* backup\r\n\r\n* Change to EQAbsHeader (#293)\r\n\r\n* changed EQAbsHeader\r\n\r\n* readbility improvements\r\n\r\n* backup\r\n\r\n* backup\r\n\r\n* simplify Decoded.Reverse\r\n\r\n* progress in handleRouterAlerts methods\r\n\r\n* clean-up\r\n\r\n* add section header\r\n\r\n* drop comment\r\n\r\n* Fix verification errors in dependencies (#291)\r\n\r\n* backup\r\n\r\n* backup\r\n\r\n* backup\r\n\r\n* simplify Decoded.Reverse\r\n\r\n* clean-up\r\n\r\n* add section header\r\n\r\n* drop comment\r\n\r\n* backup\r\n\r\n* backup\r\n\r\n* fix  verification errors in processEgress and DoXover\r\naddressing feedback\r\nclean up\r\n\r\n* backup\r\n\r\n* drop one assume\r\n\r\n* readability improvements\r\n\r\n* backup\r\n\r\n* backup\r\n\r\n* simplify proof\r\n\r\n* adapt lemmas\r\n\r\n* verify spec for SerializeTo of infofield\r\n\r\n* Missing Postcondition in Process (#301)\r\n\r\n* absPkt opaque and other improvements\r\n\r\n* tests for local enter guard\r\n\r\n* new approach for absPkt\r\n\r\n* tests with GetIngressIDNotZero()\r\n\r\n* fix verification error\r\n\r\n* progress io-skeleton in process\r\n\r\n* progress Xover\r\n\r\n* progress io-spec skeleton in process\r\n\r\n* removed dulicate of lemma\r\n\r\n* fix verification error\r\n\r\n* removed old concurrency test\r\n\r\n* refactored absPkt\r\n\r\n* continue refactoring of absPkt\r\n\r\n* fixed postcondition in process\r\n\r\n* progress lemmas for io-spec\r\n\r\n* addressed feedback\r\n\r\n* progress in updateNonConsDirIngressSegID\r\n\r\n* fix verification errors\r\n\r\n* Prove IO lemmas in `path/scion` (#290)\r\n\r\n* try to prove lemma\r\n\r\n* backup\r\n\r\n* fix incompletness via additional lemma\r\n\r\n* fix verification error\r\n\r\n* fix verification errors and clean up\r\n\r\n* fix verification errors introduced in the latest changes to the PR\r\n\r\n* fix consistency error\r\n\r\n* add lemmas for updateNonConsDirIngressSegID()\r\n\r\n* Change to EQAbsHeader (#293)\r\n\r\n* changed EQAbsHeader\r\n\r\n* readbility improvements\r\n\r\n* Revert \"Update gobra.yml to disableNL (#289)\"\r\n\r\nThis reverts commit 1e608307ba609fff78c3304f58accd996a4b1dbc.\r\n\r\n* progress in handleRouterAlerts methods\r\n\r\n* Fix verification errors in dependencies (#291)\r\n\r\n* backup\r\n\r\n* backup\r\n\r\n* backup\r\n\r\n* simplify Decoded.Reverse\r\n\r\n* clean-up\r\n\r\n* add section header\r\n\r\n* drop comment\r\n\r\n* fix  verification errors in processEgress and DoXover\r\naddressing feedback\r\nclean up\r\n\r\n* fix verification error\r\n\r\n* changed postcondition in process\r\n\r\n* fix verification error\r\n\r\n* fix verification error\r\n\r\n* Update gobra.yml\r\n\r\n* added postcondition to packSCMP\r\n\r\n---------\r\n\r\nCo-authored-by: João Pereira <joaopereira.19@gmail.com>\r\n\r\n* Drop unnecessary function `hopFieldsNotConsDir` (#303)\r\n\r\n* reverse hopFieldsNotConsDir once\r\n\r\n* remove hopfieldsNotConsDir\r\n\r\n* hopFieldsConsDir => hopFields\r\n\r\n---------\r\n\r\nCo-authored-by: João Pereira <joaopereira.19@gmail.com>\r\n\r\n* Update IO-spec to drop the `xover_core` event (#302)\r\n\r\n* progress updating the IO-spec\r\n\r\n* finish updating new IO-spec\r\n\r\n* Fix precondition of `processSCION` (#307)\r\n\r\n* start fixing pres of processSCION\r\n\r\n* backup\r\n\r\n* backup\r\n\r\n* Drop unnecessary assertions\r\n\r\n* tiny fmt\r\n\r\n* streamline msgterm assumptions (#308)\r\n\r\n* improve verification time of processPkt\r\n\r\n* IO-spec update for link check logic (#310)\r\n\r\n* io-spec update\r\n\r\n* proof of link logic\r\n\r\n* fix verification errors\r\n\r\n* drop assumption in validateSrcDstIA()\r\n\r\n* fix verification error\r\n\r\n* Update pkg/slayers/path/scion/raw.go\r\n\r\n* Pre/Post conditions of processPkt (#312)\r\n\r\n* progress with pre and post conditions for io-spec in processPkt\r\n\r\n* fix verification error\r\n\r\n* changes in process\r\n\r\n* additional temporary assumptions in process()\r\n\r\n* cleanup\r\n\r\n---------\r\n\r\nCo-authored-by: João Pereira <joaopereira.19@gmail.com>\r\n\r\n* fmt\r\n\r\n---------\r\n\r\nCo-authored-by: MLETHZ <mlimbeck@student.ethz.ch>\r\nCo-authored-by: Markus Limbeck <92801626+mlimbeck@users.noreply.github.com>\r\nCo-authored-by: João Pereira <joaopereira.19@gmail.com>\r\n\r\n* Update names of functions according to the changes in the IO-spec (#314)\r\n\r\n* minor renaming and merging of functions\r\n\r\n* further renaming\r\n\r\n* Cleanup unnecessary code in the stdlib formalization (#315)\r\n\r\n* cleanup unnecessary code in the stdlib formalization\r\n\r\n* replace occurrences of names with 'VerifiedSCION'\r\n\r\n* backup (#324)\r\n\r\n* Remove more names (#325)\r\n\r\n* backup\r\n\r\n* remove more\r\n\r\n* Disable conditionalizePermissions (#319)\r\n\r\n* Update gobra.yml\r\n\r\n* Update gobra.yml\r\n\r\n* fix verification error\r\n\r\n* fixed precondition of XoverEvent\r\n\r\n* enable moreJoins impure (#321)\r\n\r\n* invariant strengthening\r\n\r\n* undo change to the state consolidator\r\n\r\n---------\r\n\r\nCo-authored-by: mlimbeck <mlimbeck@student.ethz.ch>\r\nCo-authored-by: Dspil <dennisspiliopoylos@gmail.com>\r\n\r\n* Refactored Widen-lemma (#327)\r\n\r\n* Update gobra.yml\r\n\r\n* Update gobra.yml\r\n\r\n* fix verification error\r\n\r\n* fixed precondition of XoverEvent\r\n\r\n* enable moreJoins impure (#321)\r\n\r\n* invariant strengthening\r\n\r\n* progress widen-lemma proof\r\n\r\n* fix verification error\r\n\r\n* proven?\r\n\r\n* fix\r\n\r\n* bugfix\r\n\r\n* Update router/widen-lemma.gobra\r\n\r\nCo-authored-by: João Pereira <joaopereira.19@gmail.com>\r\n\r\n* Update router/widen-lemma.gobra\r\n\r\nCo-authored-by: João Pereira <joaopereira.19@gmail.com>\r\n\r\n* joao\r\n\r\n* indent\r\n\r\n---------\r\n\r\nCo-authored-by: João Pereira <joaopereira.19@gmail.com>\r\nCo-authored-by: Dspil <dennisspiliopoylos@gmail.com>\r\nCo-authored-by: Dionysios Spiliopoulos <32896454+Dspil@users.noreply.github.com>\r\n\r\n* enable chop 10 in the CI (#328)\r\n\r\n* drop assumption in processPkt (#318)\r\n\r\nCo-authored-by: João Pereira <joaopereira.19@gmail.com>\r\n\r\n* fix termination measuer (#329)\r\n\r\n* change triggers in absPktWidenLemma (#330)\r\n\r\n* change triggers in abspktwidenlemma\r\n\r\n* triggers\r\n\r\n* remove quantifiers\r\n\r\n* Drop Assumption in validateEgressID (#326)\r\n\r\n* Update gobra.yml\r\n\r\n* Update gobra.yml\r\n\r\n* fix verification error\r\n\r\n* fixed precondition of XoverEvent\r\n\r\n* enable moreJoins impure (#321)\r\n\r\n* drop assumption in validateEgressID and process\r\n\r\n* clean up\r\n\r\n* invariant strengthening\r\n\r\n* undo change to the state consolidator\r\n\r\n* refactored wellConfigured assumptions\r\n\r\n* finish proof of EgressIDNotZeroLemma\r\n\r\n* Apply suggestions from code review\r\n\r\n* removed TopologySpec\r\n\r\n* minor fmt\r\n\r\n* fix verification error\r\n\r\n* removed comments\r\n\r\nCo-authored-by: João Pereira <joaopereira.19@gmail.com>\r\n\r\n---------\r\n\r\nCo-authored-by: João Pereira <joaopereira.19@gmail.com>\r\nCo-authored-by: Dspil <dennisspiliopoylos@gmail.com>\r\nCo-authored-by: Dionysios Spiliopoulos <32896454+Dspil@users.noreply.github.com>\r\n\r\n* router: forbid bouncing packets internally (#4502) (#332)\r\n\r\nBrings changes from scion pr 4502\r\n\r\nCo-authored-by: Matthias Frei <matzf@scion.org>\r\n\r\n* Proof of Internal Packet Bouncing fix (#4502) (#333)\r\n\r\n* proof of scionfix #4502\r\n\r\n* feedback\r\n\r\n* drop assume in processOHP()\r\n\r\n* change getDomExternal()   to opaque\r\n\r\n* fix comment\r\n\r\n* verification fix and simplification\r\n\r\n* fix verification errors\r\n\r\n* feedback\r\n\r\n* bring changes from #243 (#335)\r\n\r\n* Drop `trusted` annotation in method (#339)\r\n\r\n* drop trusted from method\r\n\r\n* IO-spec lemmas (#334)\r\n\r\n* progress open io-lemmas\r\n\r\n* fix verification errors\r\n\r\n* refactoring\r\n\r\n* fix verification error\r\n\r\n* Enable `conditionalizePermissions` for the `router` (#340)\r\n\r\nMarco observed that a long time is spent on (sequential) pure function verification in the router package. He also suggested that using `conditionalizePermissions` might reduce the number of branches in these functions (`moreJoins 1` does not have any effect on pure functions), which might speed up verification.\r\n\r\n* Refactoring of absPkt (#341)\r\n\r\n* drop DataPlaneSpec param from absPkt\r\n\r\n* headerOffset change in absPkt\r\n\r\n* fix syntax error\r\n\r\n* fix verification errors\r\n\r\n* fix verification errors\r\n\r\n* fix LastHopLemma\r\n\r\n* Proof of incPath (#344)\r\n\r\n* progress incPath proof\r\n\r\n* Apply suggestions from code review\r\n\r\nCo-authored-by: João Pereira <joaopereira.19@gmail.com>\r\n\r\n* fmt of widen-lemma\r\n\r\n* further fmt\r\n\r\n* feedback\r\n\r\n* add comment\r\n\r\n* Update router/dataplane.go\r\n\r\n* Apply suggestions from code review\r\n\r\n---------\r\n\r\nCo-authored-by: João Pereira <joaopereira.19@gmail.com>\r\n\r\n* simplify path/scion (#346)\r\n\r\n* Verify assumptions in SCION.DecodeFromBytes (#345)\r\n\r\n* progress scion- decodeFromBytes\r\n\r\n* revert change of call s.Path.DecodeFromBytes()\r\n\r\n* fix verification error\r\n\r\n* fix permission in rawPath\r\n\r\n* establish validPktHeader in parsePath\r\n\r\n* fix verification errors\r\n\r\n* fixed permission and refactored EqAbsHeader\r\n\r\n* fixed syntax errors\r\n\r\n* fix verification error\r\n\r\n* fix permission\r\n\r\n* introduces additional spec to the Path interface\r\n\r\n* remove unnecessary preconditions\r\n\r\n* proof of parse path assumption\r\n\r\n* simplification in epic.DecodeFromBytes\r\n\r\n* feedback\r\n\r\n* Update pkg/slayers/path/scion/raw.go\r\n\r\nCo-authored-by: João Pereira <joaopereira.19@gmail.com>\r\n\r\n* add quantifier to GetCurrentHopField() and GetCurrentInfoField() to avoid code changes\r\n\r\n* Apply suggestions from code review\r\n\r\nCo-authored-by: João Pereira <joaopereira.19@gmail.com>\r\n\r\n* formatting\r\n\r\n* simplify onehop\r\n\r\n* improve io_msgterm_spec.gobra\r\n\r\n---------\r\n\r\nCo-authored-by: João Pereira <joaopereira.19@gmail.com>\r\n\r\n* Drop assumption in parsePath (#348)\r\n\r\n* drop assumption in parsePath\r\n\r\n* Update router/dataplane.go\r\n\r\nCo-authored-by: João Pereira <joaopereira.19@gmail.com>\r\n\r\n* rename arrayCongruence()  to AbsMacArrayCongruence()\r\n\r\n---------\r\n\r\nCo-authored-by: João Pereira <joaopereira.19@gmail.com>\r\n\r\n* Use Gobra's built-in ghost fields (#337)\r\n\r\n* add ghost fields\r\n\r\n* fix type errors so far\r\n\r\n* backup\r\n\r\n* clean-up\r\n\r\n* convert more adt types to structs\r\n\r\n* make read not trusted\r\n\r\n* Update router/dataplane_concurrency_model.gobra\r\n\r\n* cleanup\r\n\r\n* change equality\r\n\r\n* rever changes to ===\r\n\r\n* clean-up\r\n\r\n* Fix ghostness of output params (#349)\r\n\r\n* fix ghostness of a few outparams\r\n\r\n* backup\r\n\r\n* fix fmt (#351)\r\n\r\n* big clean-up (#354)\r\n\r\n* Drop Assumption in SetInfoField (#350)\r\n\r\n* proof setInfoField\r\n\r\n* fix verification errors\r\n\r\n* fix syntax error\r\n\r\n* fix verification errors\r\n\r\n* formatting\r\n\r\n* simplification attempt\r\n\r\n* Apply suggestions from code review\r\n\r\nCo-authored-by: João Pereira <joaopereira.19@gmail.com>\r\n\r\n* refactoring\r\n\r\n* fix verification error\r\n\r\n* fixed LeftSegEquality()\r\n\r\n* formatting\r\n\r\n* Apply suggestions from code review\r\n\r\nCo-authored-by: João Pereira <joaopereira.19@gmail.com>\r\n\r\n* feedback\r\n\r\n* renaming AbsSlice_Bytes to Bytes\r\n\r\n* adding documentation\r\n\r\n---------\r\n\r\nCo-authored-by: João Pereira <joaopereira.19@gmail.com>\r\n\r\n* small clean-up (#355)\r\n\r\n* Simplification of segLens (#356)\r\n\r\n* simplification of SegLens\r\n\r\n* remove preconditions on CombineSegLens\r\n\r\n* fix verification error\r\n\r\n* renaming\r\n\r\n* make Len impure and add LenSpec (#357)\r\n\r\n* Format `info_hop_setter_lemmas.gobra` (#359)\r\n\r\n* fmt\r\n\r\n* fmt\r\n\r\n* Simplify validity criteria of paths (#352)\r\n\r\n* backup\r\n\r\n* backup\r\n\r\n* continue refactor\r\n\r\n* backup\r\n\r\n* Update pkg/slayers/path/epic/epic_spec_test.gobra\r\n\r\n* backup\r\n\r\n* merge with master\r\n\r\n* backup\r\n\r\n* fix verification error\r\n\r\n* backup\r\n\r\n* simplify preconditions\r\n\r\n* drop unnecessary method\r\n\r\n* fix annotation\r\n\r\n* fix verification error\r\n\r\n* minor fixes in styling\r\n\r\n* fix verification errors\r\n\r\n* proof of IsSupportedPkt (#363)\r\n\r\n* Drop two assumptions and merge validity criteria `StronglyValid` and `FullyValid` (#366)\r\n\r\n* backup\r\n\r\n* backup\r\n\r\n* fix verification error\r\n\r\n* fix test\r\n\r\n* fix another verification error\r\n\r\n* fix verification error\r\n\r\n* drop StronglyValid criteria\r\n\r\n* cleanup\r\n\r\n* Update gobra.yml\r\n\r\n* Update .github/workflows/gobra.yml\r\n\r\n* Update .github/workflows/gobra.yml\r\n\r\n* Drop SetHopfield related assumptions (#368)\r\n\r\n* proof of sethopfield and io-assumptions\r\n\r\n* fix syntax errors\r\n\r\n* fix termination measure\r\n\r\n* fix verification errors\r\n\r\n* simplifications and comments\r\n\r\n* fix syntax error\r\n\r\n* feedback\r\n\r\n* fix verification error\r\n\r\n* renaming\r\n\r\n* space between arithmetic operands\r\n\r\n* increase timeout of path/scion\r\n\r\n* fix verification error\r\n\r\n* test: parallelizeBranches for dependencies\r\n\r\n* test: increase timeout for scion package to 20 min\r\n\r\n* test: increase timeout for scion package to 1h\r\n\r\n* use parallelizeBranches only for scion package\r\n\r\n* stronger precondition for setHopfield\r\n\r\n* Revert \"stronger precondition for setHopfield\"\r\n\r\n* test: scion pkg without parallelizeBranches\r\n\r\n* Revert \"test: scion pkg without parallelizeBranches\"\r\n\r\n* fix merging mistake\r\n\r\n* assume postconditions in setHopfield\r\n\r\n* add comment to IO assumptions\r\n\r\n* increase timeout for scion package\r\n\r\n* revert timeout increase\r\n\r\n* feedback\r\n\r\n* Drop IO-assumptions in processOHP (#369)\r\n\r\n* move assumption from processOHP to updateSCIONLayer\r\n\r\n* proof of assumptions in processOHP\r\n\r\n* test: moreJoins for SerializeTo in slayers\r\n\r\n* fix verification error\r\n\r\n* feedback\r\n\r\n* add moreJoins to SerializeTo()\r\n\r\n* fix sytnax errors\r\n\r\n* fix some verification errors\r\n\r\n* make `hf_valid` opaque (#372)\r\n\r\n* make hf_valid opaque\r\n\r\n* backup\r\n\r\n* backup\r\n\r\n* might have to reverse this\r\n\r\n* backup\r\n\r\n* backup\r\n\r\n* Update router/io-spec-abstract-transitions.gobra\r\n\r\n* Update README.md\r\n\r\n* progress with verification errors\r\n\r\n---------\r\n\r\nCo-authored-by: João Pereira <joaopereira.19@gmail.com>\r\nCo-authored-by: Dionysios Spiliopoulos <32896454+Dspil@users.noreply.github.com>\r\nCo-authored-by: jiceatscion <139873336+jiceatscion@users.noreply.github.com>\r\nCo-authored-by: Dspil <dennisspiliopoylos@gmail.com>\r\nCo-authored-by: Matthias Frei <matzf@scion.org>","shortMessageHtmlLink":"processEpic Continued (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2427502521\" data-permission-text=\"Title is private\" data-url=\"https://github.com/viperproject/VerifiedSCION/issues/371\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/viperproject/VerifiedSCION/pull/371/hovercard\" href=\"https://github.com/viperproject/VerifiedSCION/pull/371\">#371</a>)"}},{"before":"ed7b61d255ef7149fa4700ad28def9b778aa0987","after":null,"ref":"refs/heads/joao-uncomment-packSCMP","pushedAt":"2024-08-29T16:59:26.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"jcp19","name":"João Pereira","path":"/jcp19","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6281876?s=80&v=4"}},{"before":"445bbadaecc9da6c7bc9b702b5a2581957015a9f","after":"68b984b42688c192338c3fdf3bad8da64576c3b5","ref":"refs/heads/master","pushedAt":"2024-08-29T16:59:23.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"jcp19","name":"João Pereira","path":"/jcp19","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6281876?s=80&v=4"},"commit":{"message":"Verify `packSCMP` (#243)\n\n* start\r\n\r\n* make type-check\r\n\r\n* backup\r\n\r\n* fix syntax errors\r\n\r\n* establish necessary precondition of DecodeFromBytes\r\n\r\n* remove TODOs\r\n\r\n* backup\r\n\r\n* move on with proof obligations\r\n\r\n* verify packSCMP; reinstate TODO()s for doing the proof step by step\r\n\r\n* backup\r\n\r\n* backup\r\n\r\n* fix parse and type errors\r\n\r\n* fix packscmp\r\n\r\n* backup\r\n\r\n* backup\r\n\r\n* kill branches for now\r\n\r\n* backup\r\n\r\n* backup\r\n\r\n* remove files pushed by mistake\r\n\r\n* del file\r\n\r\n* fix verification error\r\n\r\n* change comment format\r\n\r\n* backup\r\n\r\n* reset changes to scion_spec.gobra\r\n\r\n* continue making progress\r\n\r\n* backup\r\n\r\n* simplify spec\r\n\r\n* backup\r\n\r\n* non-termination again\r\n\r\n* backup\r\n\r\n* packSCMP Continued (#373)\r\n\r\n* fix missing precondition for packSCMP\r\n\r\n* progress scmp\r\n\r\n* further progress\r\n\r\n* further scmp fixes\r\n\r\n* fix syntax error and strengthen spec of erros.Is function\r\n\r\n* fix verification error\r\n\r\n* fix verification errors in process()\r\n\r\n* drop last scmp assumption\r\n\r\n* fix verification errors in process()\r\n\r\n* add missing postconditions to resolveInbound\r\n\r\n* fix p.d permissions\r\n\r\n* remove wrong precondition from validateEgressUp()\r\n\r\n* clean up\r\n\r\n* feedback\r\n\r\n* Update router/dataplane.go\r\n\r\n---------\r\n\r\nCo-authored-by: João Pereira <joaopereira.19@gmail.com>\r\n\r\n* Move ownership of underlying slice of `SerializableBuffer` to outside of `Mem()` (#374)\r\n\r\n* fix missing precondition for packSCMP\r\n\r\n* progress scmp\r\n\r\n* further progress\r\n\r\n* further scmp fixes\r\n\r\n* fix syntax error and strengthen spec of erros.Is function\r\n\r\n* fix verification error\r\n\r\n* fix verification errors in process()\r\n\r\n* drop last scmp assumption\r\n\r\n* fix verification errors in process()\r\n\r\n* add missing postconditions to resolveInbound\r\n\r\n* fix p.d permissions\r\n\r\n* save\r\n\r\n* remove wrong precondition from validateEgressUp()\r\n\r\n* clean up\r\n\r\n* feedback\r\n\r\n* change dependencies to new buffer approach\r\n\r\n* remove buffWithFullPerm flag from scionPacketProcessor\r\n\r\n* fix verification errors\r\n\r\n* fix permission mistake\r\n\r\n* Apply suggestions from code review\r\n\r\nCo-authored-by: João Pereira <joaopereira.19@gmail.com>\r\n\r\n* pass underlying buffer slice to prepareSCMP\r\n\r\n* remove deep ownership of buffer slice in message\r\n\r\n* fix verification error in run\r\n\r\n* fix injectivity issue in run() and verification error in newPacketProcessor\r\n\r\n* different trigger\r\n\r\n* proves injectivity for message buffer directly without sets\r\n\r\n* test: remove unnecessary invariants in run()\r\n\r\n* improvements to injectivity lemma for messages\r\n\r\n* introduce new lemma PermsImplyIneq()\r\n\r\n* fixed missing preconditions\r\n\r\n* minor fixes and feedback\r\n\r\n* fix verification error\r\n\r\n* fmt\r\n\r\n---------\r\n\r\nCo-authored-by: João Pereira <joaopereira.19@gmail.com>\r\n\r\n---------\r\n\r\nCo-authored-by: Markus Limbeck <92801626+mlimbeck@users.noreply.github.com>","shortMessageHtmlLink":"Verify <code>packSCMP</code> (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2102277298\" data-permission-text=\"Title is private\" data-url=\"https://github.com/viperproject/VerifiedSCION/issues/243\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/viperproject/VerifiedSCION/pull/243/hovercard\" href=\"https://github.com/viperproject/VerifiedSCION/pull/243\">#243</a>)"}},{"before":"5187f87686bcf6c9926ce7cbebdba47303a9dc77","after":null,"ref":"refs/heads/markus-packscmp-new-inv","pushedAt":"2024-08-29T12:01:03.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"jcp19","name":"João Pereira","path":"/jcp19","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6281876?s=80&v=4"}},{"before":"320a1fbab0f888f4a609e18bc1152480e3c136d3","after":"ed7b61d255ef7149fa4700ad28def9b778aa0987","ref":"refs/heads/joao-uncomment-packSCMP","pushedAt":"2024-08-29T12:01:01.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"jcp19","name":"João Pereira","path":"/jcp19","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6281876?s=80&v=4"},"commit":{"message":"Move ownership of underlying slice of `SerializableBuffer` to outside of `Mem()` (#374)\n\n* fix missing precondition for packSCMP\r\n\r\n* progress scmp\r\n\r\n* further progress\r\n\r\n* further scmp fixes\r\n\r\n* fix syntax error and strengthen spec of erros.Is function\r\n\r\n* fix verification error\r\n\r\n* fix verification errors in process()\r\n\r\n* drop last scmp assumption\r\n\r\n* fix verification errors in process()\r\n\r\n* add missing postconditions to resolveInbound\r\n\r\n* fix p.d permissions\r\n\r\n* save\r\n\r\n* remove wrong precondition from validateEgressUp()\r\n\r\n* clean up\r\n\r\n* feedback\r\n\r\n* change dependencies to new buffer approach\r\n\r\n* remove buffWithFullPerm flag from scionPacketProcessor\r\n\r\n* fix verification errors\r\n\r\n* fix permission mistake\r\n\r\n* Apply suggestions from code review\r\n\r\nCo-authored-by: João Pereira <joaopereira.19@gmail.com>\r\n\r\n* pass underlying buffer slice to prepareSCMP\r\n\r\n* remove deep ownership of buffer slice in message\r\n\r\n* fix verification error in run\r\n\r\n* fix injectivity issue in run() and verification error in newPacketProcessor\r\n\r\n* different trigger\r\n\r\n* proves injectivity for message buffer directly without sets\r\n\r\n* test: remove unnecessary invariants in run()\r\n\r\n* improvements to injectivity lemma for messages\r\n\r\n* introduce new lemma PermsImplyIneq()\r\n\r\n* fixed missing preconditions\r\n\r\n* minor fixes and feedback\r\n\r\n* fix verification error\r\n\r\n* fmt\r\n\r\n---------\r\n\r\nCo-authored-by: João Pereira <joaopereira.19@gmail.com>","shortMessageHtmlLink":"Move ownership of underlying slice of <code>SerializableBuffer</code> to outside…"}},{"before":"fa8c6b1dd8f49b9d3509bb5b1cafaaa27824a72a","after":"5187f87686bcf6c9926ce7cbebdba47303a9dc77","ref":"refs/heads/markus-packscmp-new-inv","pushedAt":"2024-08-29T10:13:17.000Z","pushType":"push","commitsCount":4,"pusher":{"login":"jcp19","name":"João Pereira","path":"/jcp19","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6281876?s=80&v=4"},"commit":{"message":"Merge branch 'joao-uncomment-packSCMP' into markus-packscmp-new-inv","shortMessageHtmlLink":"Merge branch 'joao-uncomment-packSCMP' into markus-packscmp-new-inv"}},{"before":"d5df19d2a6ca51041d644c7e8761a52b7b3ee24a","after":"fa8c6b1dd8f49b9d3509bb5b1cafaaa27824a72a","ref":"refs/heads/markus-packscmp-new-inv","pushedAt":"2024-08-29T09:45:50.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mlimbeck","name":"Markus Limbeck","path":"/mlimbeck","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/92801626?s=80&v=4"},"commit":{"message":"fmt","shortMessageHtmlLink":"fmt"}},{"before":"ed2cdcf276510510d5f13f1328c316fbabee9424","after":"d5df19d2a6ca51041d644c7e8761a52b7b3ee24a","ref":"refs/heads/markus-packscmp-new-inv","pushedAt":"2024-08-29T08:47:59.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mlimbeck","name":"Markus Limbeck","path":"/mlimbeck","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/92801626?s=80&v=4"},"commit":{"message":"fix verification error","shortMessageHtmlLink":"fix verification error"}},{"before":"267c125746417443bee5bba5495ebe6ad69fa8f0","after":"ed2cdcf276510510d5f13f1328c316fbabee9424","ref":"refs/heads/markus-packscmp-new-inv","pushedAt":"2024-08-29T06:59:39.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mlimbeck","name":"Markus Limbeck","path":"/mlimbeck","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/92801626?s=80&v=4"},"commit":{"message":"minor fixes and feedback","shortMessageHtmlLink":"minor fixes and feedback"}},{"before":"d4da9cc987ada6fbee9fbcbbdd109ab47f860898","after":"320a1fbab0f888f4a609e18bc1152480e3c136d3","ref":"refs/heads/joao-uncomment-packSCMP","pushedAt":"2024-08-28T20:28:12.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"jcp19","name":"João Pereira","path":"/jcp19","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6281876?s=80&v=4"},"commit":{"message":"Merge branch 'master' into joao-uncomment-packSCMP","shortMessageHtmlLink":"Merge branch 'master' into joao-uncomment-packSCMP"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0xOVQwODoxMjowMi4wMDAwMDBazwAAAAS6kpIr","startCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0xOVQwODoxMjowMi4wMDAwMDBazwAAAAS6kpIr","endCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOC0yOFQyMDoyODoxMi4wMDAwMDBazwAAAASm7Ni7"}},"title":"Activity · viperproject/VerifiedSCION"}