Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Verify the IO behavior (a.k.a., basis PR) #248

Merged
merged 111 commits into from
Apr 12, 2024
Merged

Verify the IO behavior (a.k.a., basis PR) #248

merged 111 commits into from
Apr 12, 2024

Commits on Jun 20, 2023

  1. manually trigger workflow

    @mlimbeck
    mlimbeck committed Jun 20, 2023
    Configuration menu
    Copy the full SHA
    0aa5841 View commit details
    Browse the repository at this point in the history

  2. manually trigger workflow

    @mlimbeck
    mlimbeck committed Jun 20, 2023
    Configuration menu
    Copy the full SHA
    8525b7c View commit details
    Browse the repository at this point in the history

Commits on Jul 4, 2023

  1. raw byte to spec for segments and hopfields

    @mlimbeck
    mlimbeck committed Jul 4, 2023
    Configuration menu
    Copy the full SHA
    2eaf7a4 View commit details
    Browse the repository at this point in the history

  2. bugfix

    @mlimbeck
    mlimbeck committed Jul 4, 2023
    Configuration menu
    Copy the full SHA
    e9d31ae View commit details
    Browse the repository at this point in the history

  3. import fix

    @mlimbeck
    mlimbeck committed Jul 4, 2023
    Configuration menu
    Copy the full SHA
    6b77cb6 View commit details
    Browse the repository at this point in the history

Commits on Jul 10, 2023

  1. bugfix after gobra update

    @mlimbeck
    mlimbeck committed Jul 10, 2023
    Configuration menu
    Copy the full SHA
    e9631e0 View commit details
    Browse the repository at this point in the history

  2. spec to pkt (currSeg)

    @mlimbeck
    mlimbeck committed Jul 10, 2023
    Configuration menu
    Copy the full SHA
    bd062dc View commit details
    Browse the repository at this point in the history

Commits on Jul 11, 2023

  1. spec to pkt (left, mid, right)

    @mlimbeck
    mlimbeck committed Jul 11, 2023
    Configuration menu
    Copy the full SHA
    3246a2b View commit details
    Browse the repository at this point in the history

  2. spec to pkt (termination)

    @mlimbeck
    mlimbeck committed Jul 11, 2023
    Configuration menu
    Copy the full SHA
    35ff392 View commit details
    Browse the repository at this point in the history

Commits on Jul 17, 2023

  1. code clean up

    @mlimbeck
    mlimbeck committed Jul 17, 2023
    Configuration menu
    Copy the full SHA
    f925f10 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'viperproject:master' into master

    @mlimbeck
    mlimbeck authored Jul 17, 2023
    Configuration menu
    Copy the full SHA
    6a19edf View commit details
    Browse the repository at this point in the history

  3. clean up

    @mlimbeck
    mlimbeck committed Jul 17, 2023
    Configuration menu
    Copy the full SHA
    3d90011 View commit details
    Browse the repository at this point in the history

Commits on Jul 18, 2023

  1. improvements

    @mlimbeck
    mlimbeck committed Jul 18, 2023
    Configuration menu
    Copy the full SHA
    6e8f884 View commit details
    Browse the repository at this point in the history

Commits on Jul 19, 2023

  1. instantiate abstract functions with bodies

    @mlimbeck
    mlimbeck committed Jul 19, 2023
    Configuration menu
    Copy the full SHA
    afe9e52 View commit details
    Browse the repository at this point in the history

  2. progress io spec

    @mlimbeck
    mlimbeck committed Jul 19, 2023
    Configuration menu
    Copy the full SHA
    de241b5 View commit details
    Browse the repository at this point in the history

Commits on Jul 24, 2023

  1. formatting

    @mlimbeck
    mlimbeck committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    8a0452e View commit details
    Browse the repository at this point in the history

  2. specification fixes

    @mlimbeck
    mlimbeck committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    4540095 View commit details
    Browse the repository at this point in the history

  3. improve IO-spec

    @mlimbeck
    mlimbeck committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    bf2c331 View commit details
    Browse the repository at this point in the history

  4. IO-spec to pkt rewritten

    @mlimbeck
    mlimbeck committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    53cadc9 View commit details
    Browse the repository at this point in the history

  5. clean up

    @mlimbeck
    mlimbeck committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    790e842 View commit details
    Browse the repository at this point in the history

Commits on Jul 28, 2023

  1. improve readability

    @mlimbeck
    mlimbeck committed Jul 28, 2023
    Configuration menu
    Copy the full SHA
    ca581db View commit details
    Browse the repository at this point in the history

Commits on Sep 28, 2023

  1. Merge branch 'master' into master

    @jcp19
    jcp19 authored Sep 28, 2023
    Configuration menu
    Copy the full SHA
    0d3cc57 View commit details
    Browse the repository at this point in the history

Commits on Oct 17, 2023

  1. Merge branch 'master' into master

    @jcp19
    jcp19 authored Oct 17, 2023
    Configuration menu
    Copy the full SHA
    01eade7 View commit details
    Browse the repository at this point in the history

Commits on Nov 1, 2023

  1. rename of function lengthOfCurrSeg

    @mlimbeck
    mlimbeck committed Nov 1, 2023
    Configuration menu
    Copy the full SHA
    bfd6c2f View commit details
    Browse the repository at this point in the history

Commits on Nov 14, 2023

  1. Merge remote-tracking branch 'remotescion/master'

    @mlimbeck
    mlimbeck committed Nov 14, 2023
    Configuration menu
    Copy the full SHA
    8c7b6c1 View commit details
    Browse the repository at this point in the history

Commits on Nov 15, 2023

  1. Merge remote-tracking branch 'remotescion/master'

    @mlimbeck
    mlimbeck committed Nov 15, 2023
    Configuration menu
    Copy the full SHA
    89997c6 View commit details
    Browse the repository at this point in the history

Commits on Nov 16, 2023

  1. extract asid-seqence from raw pkt

    @mlimbeck
    mlimbeck committed Nov 16, 2023
    Configuration menu
    Copy the full SHA
    f1cf0b1 View commit details
    Browse the repository at this point in the history

  2. missing trigger

    @mlimbeck
    mlimbeck committed Nov 16, 2023
    Configuration menu
    Copy the full SHA
    4343478 View commit details
    Browse the repository at this point in the history

  3. quick fix

    @mlimbeck
    mlimbeck committed Nov 16, 2023
    Configuration menu
    Copy the full SHA
    715fa51 View commit details
    Browse the repository at this point in the history

Commits on Nov 17, 2023

  1. Update router/dataplane_spec.gobra 

    Co-authored-by: Dionysios Spiliopoulos <[email protected]>
    @mlimbeck @Dspil
    mlimbeck and Dspil authored Nov 17, 2023
    Configuration menu
    Copy the full SHA
    b051f09 View commit details
    Browse the repository at this point in the history

Commits on Nov 22, 2023

  1. Apply suggestions from code review 

    Co-authored-by: João Pereira <[email protected]>
    @mlimbeck @jcp19
    mlimbeck and jcp19 authored Nov 22, 2023
    Configuration menu
    Copy the full SHA
    7cbe9d6 View commit details
    Browse the repository at this point in the history

  2. readability improvements

    @mlimbeck
    mlimbeck committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    689e9da View commit details
    Browse the repository at this point in the history

  3. further improvements

    @mlimbeck
    mlimbeck committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    24d19e1 View commit details
    Browse the repository at this point in the history

  4. replace 4 by its constant InfoLen

    @mlimbeck
    mlimbeck committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    e923c40 View commit details
    Browse the repository at this point in the history

  5. readability improvement

    @mlimbeck
    mlimbeck committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    45b432e View commit details
    Browse the repository at this point in the history

  6. constant for metaLen in package path

    @mlimbeck
    mlimbeck committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    8f15113 View commit details
    Browse the repository at this point in the history

  7. Update router/io-spec.gobra 

    Co-authored-by: João Pereira <[email protected]>
    @mlimbeck @jcp19
    mlimbeck and jcp19 authored Nov 22, 2023
    Configuration menu
    Copy the full SHA
    503b0e0 View commit details
    Browse the repository at this point in the history

  8. minor improvements

    @mlimbeck
    mlimbeck committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    c292a84 View commit details
    Browse the repository at this point in the history

  9. move validMetaLenInPath() to test file

    @mlimbeck
    mlimbeck committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    a68a3e7 View commit details
    Browse the repository at this point in the history

Commits on Dec 12, 2023

  1. Merge remote-tracking branch 'remotescion/master'

    @mlimbeck
    mlimbeck committed Dec 12, 2023
    Configuration menu
    Copy the full SHA
    ff00b89 View commit details
    Browse the repository at this point in the history

  2. io-spec in Run

    @mlimbeck
    mlimbeck committed Dec 12, 2023
    Configuration menu
    Copy the full SHA
    4e85c1f View commit details
    Browse the repository at this point in the history

Commits on Dec 21, 2023

  1. Merge branch 'master' into io-spec-in-Run

    @jcp19
    jcp19 authored Dec 21, 2023
    Configuration menu
    Copy the full SHA
    cd887c9 View commit details
    Browse the repository at this point in the history

Commits on Jan 16, 2024

  1. Merge branch 'master' into io-spec-in-Run

    @jcp19
    jcp19 authored Jan 16, 2024
    Configuration menu
    Copy the full SHA
    81b951a View commit details
    Browse the repository at this point in the history

Commits on Feb 7, 2024

  1. Merge remote-tracking branch 'remotescion/master' into io-spec-in-Run

    @mlimbeck
    mlimbeck committed Feb 7, 2024
    Configuration menu
    Copy the full SHA
    8d468b8 View commit details
    Browse the repository at this point in the history

  2. add body to absIO_val

    @mlimbeck
    mlimbeck committed Feb 7, 2024
    Configuration menu
    Copy the full SHA
    b92ee32 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'io-spec-in-Run' of https://github.com/mlimbeck/Verified… 

    …SCION into io-spec-in-Run
    @mlimbeck
    mlimbeck committed Feb 7, 2024
    Configuration menu
    Copy the full SHA
    2f250fb View commit details
    Browse the repository at this point in the history

  4. fix merge mistake

    @mlimbeck
    mlimbeck committed Feb 7, 2024
    Configuration menu
    Copy the full SHA
    95af227 View commit details
    Browse the repository at this point in the history

Commits on Feb 8, 2024

  1. fix merge mistake

    @mlimbeck
    mlimbeck committed Feb 8, 2024
    Configuration menu
    Copy the full SHA
    00d92c5 View commit details
    Browse the repository at this point in the history

  2. fix typo

    @mlimbeck
    mlimbeck committed Feb 8, 2024
    Configuration menu
    Copy the full SHA
    8c57264 View commit details
    Browse the repository at this point in the history

  3. io-spec skeleton for processPkt and processSCION

    @mlimbeck
    mlimbeck committed Feb 8, 2024
    Configuration menu
    Copy the full SHA
    1c1850b View commit details
    Browse the repository at this point in the history

  4. import fix

    @mlimbeck
    mlimbeck committed Feb 8, 2024
    Configuration menu
    Copy the full SHA
    4ccdab1 View commit details
    Browse the repository at this point in the history

  5. Update router/io-spec.gobra

    @mlimbeck
    mlimbeck authored Feb 8, 2024
    Configuration menu
    Copy the full SHA
    3161a68 View commit details
    Browse the repository at this point in the history

Commits on Feb 13, 2024

  1. Merge branch 'io-spec-in-Run' into unsupported

    @Dspil
    Dspil committed Feb 13, 2024
    Configuration menu
    Copy the full SHA
    92b4a1a View commit details
    Browse the repository at this point in the history

Commits on Feb 15, 2024

  1. unit

    @Dspil
    Dspil committed Feb 15, 2024
    Configuration menu
    Copy the full SHA
    9680dd6 View commit details
    Browse the repository at this point in the history

  2. well formdness

    @Dspil
    Dspil committed Feb 15, 2024
    Configuration menu
    Copy the full SHA
    50beee9 View commit details
    Browse the repository at this point in the history

  3. relate dataplane with dataplaneSpec

    @mlimbeck
    mlimbeck committed Feb 15, 2024
    Configuration menu
    Copy the full SHA
    8300ead View commit details
    Browse the repository at this point in the history

Commits on Feb 19, 2024

  1. Merge remote-tracking branch 'remotescion/master' into io-spec-in-Run

    @mlimbeck
    mlimbeck committed Feb 19, 2024
    Configuration menu
    Copy the full SHA
    468fab7 View commit details
    Browse the repository at this point in the history

  2. various fixes

    @mlimbeck
    mlimbeck committed Feb 19, 2024
    Configuration menu
    Copy the full SHA
    cdd2ce8 View commit details
    Browse the repository at this point in the history

  3. Update verification/io/values.gobra

    @jcp19
    jcp19 authored Feb 19, 2024
    Configuration menu
    Copy the full SHA
    7eca4dc View commit details
    Browse the repository at this point in the history

  4. permission fix for dpSpecWellConfigured

    @mlimbeck
    mlimbeck committed Feb 19, 2024
    Configuration menu
    Copy the full SHA
    67a4d5d View commit details
    Browse the repository at this point in the history

  5. permission fix in rc

    @mlimbeck
    mlimbeck committed Feb 19, 2024
    Configuration menu
    Copy the full SHA
    de48fa1 View commit details
    Browse the repository at this point in the history

  6. fix verification error

    @mlimbeck
    mlimbeck committed Feb 19, 2024
    Configuration menu
    Copy the full SHA
    f892030 View commit details
    Browse the repository at this point in the history

  7. Merge branch 'master' into io-spec-in-Run

    @jcp19
    jcp19 authored Feb 19, 2024
    Configuration menu
    Copy the full SHA
    9258b54 View commit details
    Browse the repository at this point in the history

  8. dp.Valid() as opaque

    @mlimbeck
    mlimbeck committed Feb 19, 2024
    Configuration menu
    Copy the full SHA
    7df48b8 View commit details
    Browse the repository at this point in the history

Commits on Feb 20, 2024

  1. merge master

    @jcp19
    jcp19 committed Feb 20, 2024
    Configuration menu
    Copy the full SHA
    1560668 View commit details
    Browse the repository at this point in the history

  2. backup

    @jcp19
    jcp19 committed Feb 20, 2024
    Configuration menu
    Copy the full SHA
    1a9daf3 View commit details
    Browse the repository at this point in the history

  3. format spacing

    @jcp19
    jcp19 committed Feb 20, 2024
    Configuration menu
    Copy the full SHA
    0160b2c View commit details
    Browse the repository at this point in the history

  4. improve perf; drop assumption

    @jcp19
    jcp19 committed Feb 20, 2024
    Configuration menu
    Copy the full SHA
    465553b View commit details
    Browse the repository at this point in the history

  5. fix formatting

    @jcp19
    jcp19 committed Feb 20, 2024
    Configuration menu
    Copy the full SHA
    71866b2 View commit details
    Browse the repository at this point in the history

  6. Merge branch 'joao-continue-markus-pr-iospec' into io_spec_verification

    @Dspil
    Dspil committed Feb 20, 2024
    Configuration menu
    Copy the full SHA
    0a4c77d View commit details
    Browse the repository at this point in the history

Commits on Feb 23, 2024

  1. merge master

    @jcp19
    jcp19 committed Feb 23, 2024
    Configuration menu
    Copy the full SHA
    ea7c499 View commit details
    Browse the repository at this point in the history

  2. Update router/dataplane.go

    @jcp19
    jcp19 authored Feb 23, 2024
    Configuration menu
    Copy the full SHA
    f07073e View commit details
    Browse the repository at this point in the history

Commits on Feb 27, 2024

  1. Merge branch 'master' into io_spec_verification

    @mlimbeck
    mlimbeck committed Feb 27, 2024
    Configuration menu
    Copy the full SHA
    d6b8d33 View commit details
    Browse the repository at this point in the history

  2. formatting postconditions of processPkt, processSCION

    @mlimbeck
    mlimbeck committed Feb 27, 2024
    Configuration menu
    Copy the full SHA
    384661e View commit details
    Browse the repository at this point in the history

  3. fix extra permission

    @Dspil
    Dspil committed Feb 27, 2024
    Configuration menu
    Copy the full SHA
    8514223 View commit details
    Browse the repository at this point in the history

  4. typo

    @Dspil
    Dspil committed Feb 27, 2024
    Configuration menu
    Copy the full SHA
    c27a66a View commit details
    Browse the repository at this point in the history

  5. processSCION had the same issue

    @Dspil
    Dspil committed Feb 27, 2024
    Configuration menu
    Copy the full SHA
    71aadfe View commit details
    Browse the repository at this point in the history

  6. ingressID is preseved intead of sInit

    @Dspil
    Dspil committed Feb 27, 2024
    Configuration menu
    Copy the full SHA
    88db3fd View commit details
    Browse the repository at this point in the history

  7. Revert "ingressID is preseved intead of sInit" 

    This reverts commit 88db3fd.
    @Dspil
    Dspil committed Feb 27, 2024
    Configuration menu
    Copy the full SHA
    8383408 View commit details
    Browse the repository at this point in the history

  8. Revert "processSCION had the same issue" 

    This reverts commit 71aadfe.
    @Dspil
    Dspil committed Feb 27, 2024
    Configuration menu
    Copy the full SHA
    ab5e91f View commit details
    Browse the repository at this point in the history

  9. Updated IO-Spec-Function to Correlate Bytes with Terms (#262) 

    * fixes in the asid extraction functions

* pre-/postconditions for process

* fix formatting

* fix same issue in processSCION

* fix var names

* precondition changes in hopfield and asidFromIfs

* prostcondition fix in process and processSCION

* update imports links

* Apply suggestions from code review

---------

Co-authored-by: Dspil <[email protected]>
Co-authored-by: João Pereira <[email protected]>
    @mlimbeck @Dspil @jcp19
    3 people authored Feb 27, 2024
    Configuration menu
    Copy the full SHA
    2c08fb3 View commit details
    Browse the repository at this point in the history

Commits on Feb 28, 2024

  1. made absIO_val opaque

    @Dspil
    Dspil committed Feb 28, 2024
    Configuration menu
    Copy the full SHA
    39330b5 View commit details
    Browse the repository at this point in the history

Commits on Mar 14, 2024

  1. Merge branch 'master' into io_spec_verification

    @jcp19
    jcp19 committed Mar 14, 2024
    Configuration menu
    Copy the full SHA
    99bd1e6 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'io_spec_verification' of github.com:viperproject/Verifi… 

    …edSCION into io_spec_verification
    @jcp19
    jcp19 committed Mar 14, 2024
    Configuration menu
    Copy the full SHA
    7d13caf View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' into io_spec_verification

    @jcp19
    jcp19 authored Mar 14, 2024
    Configuration menu
    Copy the full SHA
    e733dc8 View commit details
    Browse the repository at this point in the history

Commits on Mar 17, 2024

  1. Merge branch 'master' into io_spec_verification

    @jcp19
    jcp19 authored Mar 17, 2024
    Configuration menu
    Copy the full SHA
    005fa2a View commit details
    Browse the repository at this point in the history

Commits on Mar 18, 2024

  1. use artificial triggers for quantifiers inside IO resources (#280)

    @jcp19
    jcp19 authored Mar 18, 2024
    Configuration menu
    Copy the full SHA
    98a867b View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into io_spec_verification

    @jcp19
    jcp19 committed Mar 18, 2024
    Configuration menu
    Copy the full SHA
    ebf95fb View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' into io_spec_verification

    @jcp19
    jcp19 committed Mar 18, 2024
    Configuration menu
    Copy the full SHA
    baa1bb6 View commit details
    Browse the repository at this point in the history

  4. AbsPkt improvements (#270) 

    * absPkt opaque and other improvements

* quick fixes

* changed permission from R55 to R56

* added missing permission amount in ReadBatch

* fixed pre/postconditions of processPkt, processSCION and process

* fixed opaque format

---------

Co-authored-by: João Pereira <[email protected]>
    @mlimbeck @jcp19
    mlimbeck and jcp19 authored Mar 18, 2024
    Configuration menu
    Copy the full SHA
    72a5aec View commit details
    Browse the repository at this point in the history

  5. Merge branch 'master' into io_spec_verification

    @jcp19
    jcp19 authored Mar 18, 2024
    Configuration menu
    Copy the full SHA
    c9c16c7 View commit details
    Browse the repository at this point in the history

Commits on Mar 25, 2024

  1. Merge branch 'master' into io_spec_verification

    @jcp19
    jcp19 authored Mar 25, 2024
    Configuration menu
    Copy the full SHA
    e40741a View commit details
    Browse the repository at this point in the history

  2. Verify send guard in Run (#263) 

    * remove send operation

* lemma for smaller buffer result in same abstract pkt

* progress send guard

* progress send guard

* Fix incompleteness and continue with send guard (#273)

* backup

* backup

* backup

* backup

* backup

* drop space

* pick better triggers

* add necessary lemma and call to it; contains an assume false that needs to be dropped

* backup

* backup

* add missing loop invariant about ingressID

* backup

* backup

* fix verification error

* try out a simpler trigger

* widen lemma for absIO_val (#268)

* widen lemma for abspkt (non termianting)

* abspkt proven

* renamed io-spec-lemmas

* io val also proven

* cleanup

* merged markus' abspkt improvements

* consdir lemma

* proved

* reinstate lemma4

* fix verification error

* Simplify widen lemma from #268 (#282)

* start simplifying

* continue simplifying

* continue simplifying stuff

* continue simplifying

* continue simplifying

* simplify further

* finish for now

* Update router/io-spec.gobra

---------

Co-authored-by: João Pereira <[email protected]>

* Continue send (#283)

* widen lemma for abspkt (non termianting)

* abspkt proven

* renamed io-spec-lemmas

* io val also proven

* cleanup

* merged markus' abspkt improvements

* consdir lemma

* proved

* reinstate lemma4

* fix verification error

* Simplify widen lemma from #268 (#282)

* start simplifying

* continue simplifying

* continue simplifying stuff

* continue simplifying

* continue simplifying

* simplify further

* finish for now

* Update router/io-spec.gobra

* finish send in Run

* propagate changes to processSCION

---------

Co-authored-by: Dspil <[email protected]>

* backup

* adapt to the new syntax of backend annotations

* clean-up

* changes according to feedback

---------

Co-authored-by: João Pereira <[email protected]>
Co-authored-by: Dionysios Spiliopoulos <[email protected]>
Co-authored-by: Dspil <[email protected]>
    @mlimbeck @jcp19 @Dspil
    4 people authored Mar 25, 2024
    Configuration menu
    Copy the full SHA
    2c509cc View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' into io_spec_verification

    @jcp19
    jcp19 authored Mar 25, 2024
    Configuration menu
    Copy the full SHA
    bc7494b View commit details
    Browse the repository at this point in the history

Commits on Mar 28, 2024

  1. Merge branch 'master' into io_spec_verification

    @jcp19
    jcp19 authored Mar 28, 2024
    Configuration menu
    Copy the full SHA
    431a897 View commit details
    Browse the repository at this point in the history

Commits on Apr 2, 2024

  1. Merge branch 'master' into io_spec_verification

    @jcp19
    jcp19 authored Apr 2, 2024
    Configuration menu
    Copy the full SHA
    045d57e View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into io_spec_verification

    @jcp19
    jcp19 authored Apr 2, 2024
    Configuration menu
    Copy the full SHA
    e49b959 View commit details
    Browse the repository at this point in the history

Commits on Apr 3, 2024

  1. Merge branch 'master' into io_spec_verification

    @jcp19
    jcp19 authored Apr 3, 2024
    Configuration menu
    Copy the full SHA
    60bbbf8 View commit details
    Browse the repository at this point in the history

  2. IO specification skeleton in process (#284) 

    * absPkt opaque and other improvements

* tests for local enter guard

* new approach for absPkt

* tests with GetIngressIDNotZero()

* fix verification error

* progress io-skeleton in process

* progress Xover

* progress io-spec skeleton in process

* removed dulicate of lemma

* fix verification error

* removed old concurrency test

* refactored absPkt

* continue refactoring of absPkt

* fixed postcondition in process

* progress lemmas for io-spec

* addressed feedback

* progress in updateNonConsDirIngressSegID

* fix verification errors

* Prove IO lemmas in `path/scion` (#290)

* try to prove lemma

* backup

* fix incompletness via additional lemma

* fix verification error

* fix verification errors and clean up

* fix verification errors introduced in the latest changes to the PR

* fix consistency error

* add lemmas for updateNonConsDirIngressSegID()

* Change to EQAbsHeader (#293)

* changed EQAbsHeader

* readbility improvements

* progress in handleRouterAlerts methods

* Fix verification errors in dependencies (#291)

* backup

* backup

* backup

* simplify Decoded.Reverse

* clean-up

* add section header

* drop comment

* fix  verification errors in processEgress and DoXover
addressing feedback
clean up

---------

Co-authored-by: João Pereira <[email protected]>
    @mlimbeck @jcp19
    mlimbeck and jcp19 authored Apr 3, 2024
    Configuration menu
    Copy the full SHA
    1349d7a View commit details
    Browse the repository at this point in the history

Commits on Apr 4, 2024

  1. Add functional spec to InfoField.SerializeTo (#300) 

    * absPkt opaque and other improvements

* tests for local enter guard

* new approach for absPkt

* tests with GetIngressIDNotZero()

* fix verification error

* progress io-skeleton in process

* progress Xover

* progress io-spec skeleton in process

* removed dulicate of lemma

* fix verification error

* removed old concurrency test

* refactored absPkt

* continue refactoring of absPkt

* fixed postcondition in process

* progress lemmas for io-spec

* addressed feedback

* progress in updateNonConsDirIngressSegID

* fix verification errors

* Prove IO lemmas in `path/scion` (#290)

* try to prove lemma

* backup

* fix incompletness via additional lemma

* fix verification error

* fix verification errors and clean up

* fix verification errors introduced in the latest changes to the PR

* fix consistency error

* add lemmas for updateNonConsDirIngressSegID()

* backup

* Change to EQAbsHeader (#293)

* changed EQAbsHeader

* readbility improvements

* backup

* backup

* simplify Decoded.Reverse

* progress in handleRouterAlerts methods

* clean-up

* add section header

* drop comment

* Fix verification errors in dependencies (#291)

* backup

* backup

* backup

* simplify Decoded.Reverse

* clean-up

* add section header

* drop comment

* backup

* backup

* fix  verification errors in processEgress and DoXover
addressing feedback
clean up

* backup

* drop one assume

* readability improvements

* backup

* backup

* simplify proof

* adapt lemmas

* verify spec for SerializeTo of infofield
    @jcp19
    jcp19 authored Apr 4, 2024
    Configuration menu
    Copy the full SHA
    5ae6bfd View commit details
    Browse the repository at this point in the history

  2. Missing Postcondition in Process (#301) 

    * absPkt opaque and other improvements

* tests for local enter guard

* new approach for absPkt

* tests with GetIngressIDNotZero()

* fix verification error

* progress io-skeleton in process

* progress Xover

* progress io-spec skeleton in process

* removed dulicate of lemma

* fix verification error

* removed old concurrency test

* refactored absPkt

* continue refactoring of absPkt

* fixed postcondition in process

* progress lemmas for io-spec

* addressed feedback

* progress in updateNonConsDirIngressSegID

* fix verification errors

* Prove IO lemmas in `path/scion` (#290)

* try to prove lemma

* backup

* fix incompletness via additional lemma

* fix verification error

* fix verification errors and clean up

* fix verification errors introduced in the latest changes to the PR

* fix consistency error

* add lemmas for updateNonConsDirIngressSegID()

* Change to EQAbsHeader (#293)

* changed EQAbsHeader

* readbility improvements

* Revert "Update gobra.yml to disableNL (#289)"

This reverts commit 1e60830.

* progress in handleRouterAlerts methods

* Fix verification errors in dependencies (#291)

* backup

* backup

* backup

* simplify Decoded.Reverse

* clean-up

* add section header

* drop comment

* fix  verification errors in processEgress and DoXover
addressing feedback
clean up

* fix verification error

* changed postcondition in process

* fix verification error

* fix verification error

* Update gobra.yml

* added postcondition to packSCMP

---------

Co-authored-by: João Pereira <[email protected]>
    @mlimbeck @jcp19
    mlimbeck and jcp19 authored Apr 4, 2024
    Configuration menu
    Copy the full SHA
    7ea708c View commit details
    Browse the repository at this point in the history

Commits on Apr 5, 2024

  1. Drop unnecessary function hopFieldsNotConsDir (#303) 

    * reverse hopFieldsNotConsDir once

* remove hopfieldsNotConsDir

* hopFieldsConsDir => hopFields

---------

Co-authored-by: João Pereira <[email protected]>
    @Dspil @jcp19
    Dspil and jcp19 authored Apr 5, 2024
    Configuration menu
    Copy the full SHA
    003bb51 View commit details
    Browse the repository at this point in the history

  2. Update IO-spec to drop the xover_core event (#302) 

    * progress updating the IO-spec

* finish updating new IO-spec
    @mlimbeck
    mlimbeck authored Apr 5, 2024
    Configuration menu
    Copy the full SHA
    d512053 View commit details
    Browse the repository at this point in the history

  3. merge master

    @jcp19
    jcp19 committed Apr 5, 2024
    Configuration menu
    Copy the full SHA
    f3ff7a0 View commit details
    Browse the repository at this point in the history

Commits on Apr 6, 2024

  1. Fix precondition of processSCION (#307) 

    * start fixing pres of processSCION

* backup

* backup

* Drop unnecessary assertions

* tiny fmt
    @jcp19
    jcp19 authored Apr 6, 2024
    Configuration menu
    Copy the full SHA
    5b658be View commit details
    Browse the repository at this point in the history

Commits on Apr 9, 2024

  1. streamline msgterm assumptions (#308)

    @jcp19
    jcp19 authored Apr 9, 2024
    Configuration menu
    Copy the full SHA
    97e4ac7 View commit details
    Browse the repository at this point in the history

Commits on Apr 10, 2024

  1. merge with master

    @jcp19
    jcp19 committed Apr 10, 2024
    Configuration menu
    Copy the full SHA
    f03cb47 View commit details
    Browse the repository at this point in the history

  2. improve verification time of processPkt

    @jcp19
    jcp19 committed Apr 10, 2024
    Configuration menu
    Copy the full SHA
    24b0577 View commit details
    Browse the repository at this point in the history

Commits on Apr 11, 2024

  1. IO-spec update for link check logic (#310) 

    * io-spec update

* proof of link logic

* fix verification errors

* drop assumption in validateSrcDstIA()

* fix verification error

* Update pkg/slayers/path/scion/raw.go
    @mlimbeck
    mlimbeck authored Apr 11, 2024
    Configuration menu
    Copy the full SHA
    d8fb8f1 View commit details
    Browse the repository at this point in the history

  2. Pre/Post conditions of processPkt (#312) 

    * progress with pre and post conditions for io-spec in processPkt

* fix verification error

* changes in process

* additional temporary assumptions in process()

* cleanup

---------

Co-authored-by: João Pereira <[email protected]>
    @mlimbeck @jcp19
    mlimbeck and jcp19 authored Apr 11, 2024
    Configuration menu
    Copy the full SHA
    863bfa3 View commit details
    Browse the repository at this point in the history

Commits on Apr 12, 2024

  1. fmt

    @jcp19
    jcp19 committed Apr 12, 2024
    Configuration menu
    Copy the full SHA
    a67c139 View commit details
    Browse the repository at this point in the history