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

Add functional spec to InfoField.SerializeTo #300

Merged
merged 57 commits into from
Apr 4, 2024
Merged

Add functional spec to InfoField.SerializeTo #300

merged 57 commits into from
Apr 4, 2024

Commits on Mar 13, 2024

  1. absPkt opaque and other improvements

    @mlimbeck
    mlimbeck committed Mar 13, 2024
    Configuration menu
    Copy the full SHA
    ac2c877 View commit details
    Browse the repository at this point in the history

Commits on Mar 21, 2024

  1. tests for local enter guard

    @mlimbeck
    mlimbeck committed Mar 21, 2024
    Configuration menu
    Copy the full SHA
    ae39655 View commit details
    Browse the repository at this point in the history

  2. Merge io_spec_verification' into markus-io-spec-enter

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

Commits on Mar 24, 2024

  1. new approach for absPkt

    @mlimbeck
    mlimbeck committed Mar 24, 2024
    Configuration menu
    Copy the full SHA
    b1618cd View commit details
    Browse the repository at this point in the history

  2. tests with GetIngressIDNotZero()

    @mlimbeck
    mlimbeck committed Mar 24, 2024
    Configuration menu
    Copy the full SHA
    736ad9b View commit details
    Browse the repository at this point in the history

  3. fix verification error

    @mlimbeck
    mlimbeck committed Mar 24, 2024
    Configuration menu
    Copy the full SHA
    56f6348 View commit details
    Browse the repository at this point in the history

Commits on Mar 26, 2024

  1. progress io-skeleton in process

    @mlimbeck
    mlimbeck committed Mar 26, 2024
    Configuration menu
    Copy the full SHA
    6706d80 View commit details
    Browse the repository at this point in the history

  2. progress Xover

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

  3. merge with basis pr

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

Commits on Mar 27, 2024

  1. progress io-spec skeleton in process

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

  2. removed dulicate of lemma

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

  3. fix verification error

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

  4. removed old concurrency test

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

  5. refactored absPkt

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

  6. continue refactoring of absPkt

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

Commits on Mar 28, 2024

  1. fixed postcondition in process

    @mlimbeck
    mlimbeck committed Mar 28, 2024
    Configuration menu
    Copy the full SHA
    4b26ae0 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'io_spec_verification' into markus-io-spec-enter

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

  3. progress lemmas for io-spec

    @mlimbeck
    mlimbeck committed Mar 28, 2024
    Configuration menu
    Copy the full SHA
    bb5d531 View commit details
    Browse the repository at this point in the history

  4. addressed feedback

    @mlimbeck
    mlimbeck committed Mar 28, 2024
    Configuration menu
    Copy the full SHA
    3b634c3 View commit details
    Browse the repository at this point in the history

Commits on Mar 29, 2024

  1. progress in updateNonConsDirIngressSegID

    @mlimbeck
    mlimbeck committed Mar 29, 2024
    Configuration menu
    Copy the full SHA
    5344c79 View commit details
    Browse the repository at this point in the history

Commits on Apr 1, 2024

  1. fix verification errors

    @mlimbeck
    mlimbeck committed Apr 1, 2024
    Configuration menu
    Copy the full SHA
    6b24fca View commit details
    Browse the repository at this point in the history

  2. Prove IO lemmas in path/scion (#290) 

    * try to prove lemma

* backup

* fix incompletness via additional lemma

* fix verification error
    @jcp19
    jcp19 authored Apr 1, 2024
    Configuration menu
    Copy the full SHA
    a86a357 View commit details
    Browse the repository at this point in the history

  3. fix verification errors and clean up

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

  4. fix verification errors introduced in the latest changes to the PR

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

  5. Merge branch 'markus-io-spec-enter' of github.com:viperproject/Verifi… 

    …edSCION into markus-io-spec-enter
    @jcp19
    jcp19 committed Apr 1, 2024
    Configuration menu
    Copy the full SHA
    f784cf5 View commit details
    Browse the repository at this point in the history

  6. fix consistency error

    @mlimbeck
    mlimbeck committed Apr 1, 2024
    Configuration menu
    Copy the full SHA
    0e7c3bd View commit details
    Browse the repository at this point in the history

  7. add lemmas for updateNonConsDirIngressSegID()

    @mlimbeck
    mlimbeck committed Apr 1, 2024
    Configuration menu
    Copy the full SHA
    794c8a6 View commit details
    Browse the repository at this point in the history

Commits on Apr 2, 2024

  1. backup

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

  2. Merge branch 'markus-io-spec-enter' into joao-add-spec-decoded-reverse

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

  3. Change to EQAbsHeader (#293) 

    * changed EQAbsHeader

* readbility improvements
    @mlimbeck
    mlimbeck authored Apr 2, 2024
    Configuration menu
    Copy the full SHA
    c72d66e View commit details
    Browse the repository at this point in the history

  4. backup

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

  5. backup

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

  6. simplify Decoded.Reverse

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

  7. progress in handleRouterAlerts methods

    @mlimbeck
    mlimbeck committed Apr 2, 2024
    Configuration menu
    Copy the full SHA
    fc4311f View commit details
    Browse the repository at this point in the history

  8. Merge branch 'markus-io-spec-enter' into joao-add-spec-decoded-reverse

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

  9. fix verification errors

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

  10. clean-up

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

  11. add section header

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

  12. drop comment

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

  13. Merge branch 'io_spec_verification' into markus-io-spec-enter

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

  14. merge master

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

Commits on Apr 3, 2024

  1. Fix verification errors in dependencies (#291) 

    * backup

* backup

* backup

* simplify Decoded.Reverse

* clean-up

* add section header

* drop comment
    @jcp19
    jcp19 authored Apr 3, 2024
    Configuration menu
    Copy the full SHA
    aedb06b View commit details
    Browse the repository at this point in the history

  2. backup

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

  3. merge master

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

  4. Merge branch 'io_spec_verification' into markus-io-spec-enter

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

  5. backup

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

  6. fix verification errors in processEgress and DoXover 

    addressing feedback
clean up
    @mlimbeck
    mlimbeck committed Apr 3, 2024
    Configuration menu
    Copy the full SHA
    fd58c74 View commit details
    Browse the repository at this point in the history

  7. backup

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

  8. merge changes from skeleton PR

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

  9. drop one assume

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

  10. readability improvements

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

  11. backup

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

  12. backup

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

  13. merge with basis pr

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

  14. simplify proof

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

Commits on Apr 4, 2024

  1. adapt lemmas

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

  2. verify spec for SerializeTo of infofield

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