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

Connection Handshake (ICS3) L2 TLA+ spec #58

Merged
merged 44 commits into from
May 21, 2020
Merged

Connection Handshake (ICS3) L2 TLA+ spec #58

merged 44 commits into from
May 21, 2020

Commits on Apr 17, 2020

  1. Getting the ball rolling w/ CH TLA+ (L3 spec)

    @adizere
    adizere committed Apr 17, 2020
    Configuration menu
    Copy the full SHA
    11131dd View commit details
    Browse the repository at this point in the history

Commits on Apr 20, 2020

  1. Added invariant spec & fixed partyState bugs

    @adizere
    adizere committed Apr 20, 2020
    Configuration menu
    Copy the full SHA
    51ae5c0 View commit details
    Browse the repository at this point in the history

Commits on Apr 21, 2020

  1. After discussions w/ A & Z

    @adizere
    adizere committed Apr 21, 2020
    Configuration menu
    Copy the full SHA
    c2a8cee View commit details
    Browse the repository at this point in the history

Commits on Apr 22, 2020

  1. major refactoring ht/ Anca and comments from Zarko

    @adizere
    adizere committed Apr 22, 2020
    6 Configuration menu
    Copy the full SHA
    bb4808f View commit details
    Browse the repository at this point in the history

  2. Added abstractions.

    @adizere
    adizere committed Apr 22, 2020
    Configuration menu
    Copy the full SHA
    e848a84 View commit details
    Browse the repository at this point in the history

Commits on Apr 23, 2020

  1. Renamed the main file to reflect the CH 'module' within.

    @adizere
    adizere committed Apr 23, 2020
    Configuration menu
    Copy the full SHA
    bec60a5 View commit details
    Browse the repository at this point in the history

  2. quick fix for the inMsg deadlock

    @adizere
    adizere committed Apr 23, 2020
    Configuration menu
    Copy the full SHA
    a0d7728 View commit details
    Browse the repository at this point in the history

  3. fixed second deadlock with inMsg

    @adizere
    adizere committed Apr 23, 2020
    Configuration menu
    Copy the full SHA
    f590116 View commit details
    Browse the repository at this point in the history

Commits on Apr 28, 2020

  1. Significant progress on modularizing CH TLA spec.

    @adizere
    adizere committed Apr 28, 2020
    Configuration menu
    Copy the full SHA
    ad267d4 View commit details
    Browse the repository at this point in the history

  2. Fixed bug; still have the bug.

    @adizere
    adizere committed Apr 28, 2020
    Configuration menu
    Copy the full SHA
    7fd34a1 View commit details
    Browse the repository at this point in the history

Commits on Apr 29, 2020

  1. After reviewing with Anca & Zarko.

    @adizere
    adizere committed Apr 29, 2020
    Configuration menu
    Copy the full SHA
    f610468 View commit details
    Browse the repository at this point in the history

Commits on May 1, 2020

  1. Initial versions of liveness & safety properties; not much progress o… 

    …n WF
    @adizere
    adizere committed May 1, 2020
    Configuration menu
    Copy the full SHA
    c8fff52 View commit details
    Browse the repository at this point in the history

Commits on May 4, 2020

  1. Simplifications based on suggestion from Igor&Anca.

    @adizere
    adizere committed May 4, 2020
    Configuration menu
    Copy the full SHA
    d598cc4 View commit details
    Browse the repository at this point in the history

  2. Spec model check OK. WIP: liveness & safety

    @adizere
    adizere committed May 4, 2020
    Configuration menu
    Copy the full SHA
    6f1f82d View commit details
    Browse the repository at this point in the history

Commits on May 5, 2020

  1. Constant params in CHM; checking consistency

    @adizere
    adizere committed May 5, 2020
    Configuration menu
    Copy the full SHA
    e6cb34c View commit details
    Browse the repository at this point in the history

  2. ConsistencyInv holds. Better code structure

    @adizere
    adizere committed May 5, 2020
    Configuration menu
    Copy the full SHA
    f8a9653 View commit details
    Browse the repository at this point in the history

  3. Switching to sequences for buffers (instead of a single location).

    @adizere
    adizere committed May 5, 2020
    Configuration menu
    Copy the full SHA
    685a839 View commit details
    Browse the repository at this point in the history

Commits on May 6, 2020

  1. Better sequence-based buffers

    @adizere
    adizere committed May 6, 2020
    Configuration menu
    Copy the full SHA
    7393038 View commit details
    Browse the repository at this point in the history

  2. Fixed CHOOSE todos; more idiomatic handlers

    @adizere
    adizere committed May 6, 2020
    Configuration menu
    Copy the full SHA
    295c0fa View commit details
    Browse the repository at this point in the history

Commits on May 7, 2020

  1. Found generic solution for invoking msg. handlers

    @adizere
    adizere committed May 7, 2020
    Configuration menu
    Copy the full SHA
    c89803b View commit details
    Browse the repository at this point in the history

Commits on May 12, 2020

  1. Snapshot of current state; still have bug 'In evaluation, the identif… 

    …ier bufChainA is either undefined or not an operator.'
    @adizere
    adizere committed May 12, 2020
    Configuration menu
    Copy the full SHA
    42a70e4 View commit details
    Browse the repository at this point in the history

  2. Possible solution found by removing the WF and adding explicit precon… 

    …ditions instead
    @adizere
    adizere committed May 12, 2020
    Configuration menu
    Copy the full SHA
    6fdf351 View commit details
    Browse the repository at this point in the history

  3. HandleConfirmMsg, proofs mock, and ModifyStore general action. Model … 

    …checking OK
    @adizere
    adizere committed May 12, 2020
    Configuration menu
    Copy the full SHA
    41b0b49 View commit details
    Browse the repository at this point in the history

Commits on May 13, 2020

  1. Stable version with sets for client.consensusStates

    @adizere
    adizere committed May 13, 2020
    Configuration menu
    Copy the full SHA
    34317f3 View commit details
    Browse the repository at this point in the history

  2. Fixed client initialization & termination bug (caused by full buffers)

    @adizere
    adizere committed May 13, 2020
    Configuration menu
    Copy the full SHA
    199c31c View commit details
    Browse the repository at this point in the history

  3. 3-step proof validation. Stuttering step is problematic

    @adizere
    adizere committed May 13, 2020
    Configuration menu
    Copy the full SHA
    dd42615 View commit details
    Browse the repository at this point in the history

Commits on May 14, 2020

  1. Fixed stuttering problem w/ a fairness constraint.

    @adizere
    adizere committed May 14, 2020
    Configuration menu
    Copy the full SHA
    7313e00 View commit details
    Browse the repository at this point in the history

  2. Cleaned-up & added comments to CHM

    @adizere
    adizere committed May 14, 2020
    Configuration menu
    Copy the full SHA
    072a23f View commit details
    Browse the repository at this point in the history

  3. Handlers overhaul after input from Anca & Zarko

    @adizere
    adizere committed May 14, 2020
    Configuration menu
    Copy the full SHA
    1044fb2 View commit details
    Browse the repository at this point in the history

Commits on May 15, 2020

  1. Safety invariant breaks upon parallel Init msgs. Some refurbishing 

    If we make ConnectionParameters more general (see the union in ConnectionParameters.remoteEnd and localEnd) then
both chains could initialize and lock on different connections.
    @adizere
    adizere committed May 15, 2020
    Configuration menu
    Copy the full SHA
    5943c9f View commit details
    Browse the repository at this point in the history

  2. Env constrained on Init msgs after sync w/ Anca. Model checks.

    @adizere
    adizere committed May 15, 2020
    Configuration menu
    Copy the full SHA
    6d8b85d View commit details
    Browse the repository at this point in the history

Commits on May 18, 2020

  1. Documented the init message deadlock issue. Made the malicious env. m… 

    …ore powerful. Adjusted the properties.
    @adizere
    adizere committed May 18, 2020
    Configuration menu
    Copy the full SHA
    de326c7 View commit details
    Browse the repository at this point in the history

  2. Consistent comment notation

    @adizere
    adizere committed May 18, 2020
    Configuration menu
    Copy the full SHA
    cf70dd3 View commit details
    Browse the repository at this point in the history

Commits on May 19, 2020

  1. Fixed ACK handler bug; factored out common declarations into a separa… 

    …te module ICS3Types.tla; added type invariants.
    @adizere
    adizere committed May 19, 2020
    Configuration menu
    Copy the full SHA
    7cc2933 View commit details
    Browse the repository at this point in the history

  2. Fixed local connection end init values

    @adizere
    adizere committed May 19, 2020
    Configuration menu
    Copy the full SHA
    ca02bb7 View commit details
    Browse the repository at this point in the history

  3. Tried liveness check with buffers of lenght 1, no success

    @adizere
    adizere committed May 19, 2020
    Configuration menu
    Copy the full SHA
    043c745 View commit details
    Browse the repository at this point in the history

  4. Added a full-fledged termination property; fixed relaying bugs; still… 

    … left -- remove the turn mechanism
    @adizere
    adizere committed May 19, 2020
    Configuration menu
    Copy the full SHA
    59f8075 View commit details
    Browse the repository at this point in the history

Commits on May 20, 2020

  1. Added guards for RelayNextEnv action; termination checks for good env… 

    ….; state space explosion for malicious env.
    @adizere
    adizere committed May 20, 2020
    Configuration menu
    Copy the full SHA
    910d4c9 View commit details
    Browse the repository at this point in the history

  2. After Anca & Zarko's PR suggestions.

    @adizere
    adizere committed May 20, 2020
    Configuration menu
    Copy the full SHA
    9ccfc89 View commit details
    Browse the repository at this point in the history

  3. Cleaned-up; removed malicious env.

    @adizere
    adizere committed May 20, 2020
    Configuration menu
    Copy the full SHA
    90b1252 View commit details
    Browse the repository at this point in the history

Commits on May 21, 2020

  1. Recreating the deadlock #1

    @adizere
    adizere committed May 21, 2020
    Configuration menu
    Copy the full SHA
    d798850 View commit details
    Browse the repository at this point in the history

  2. Cleaned version, ready for #58

    @adizere
    adizere committed May 21, 2020
    Configuration menu
    Copy the full SHA
    28bc5d9 View commit details
    Browse the repository at this point in the history

  3. Updated readme.md

    @adizere
    adizere committed May 21, 2020
    Configuration menu
    Copy the full SHA
    d0a08c1 View commit details
    Browse the repository at this point in the history

  4. Updated readme.md typos

    @adizere
    adizere committed May 21, 2020
    Configuration menu
    Copy the full SHA
    b349d32 View commit details
    Browse the repository at this point in the history