Changelog

2025-05-23

Other

• udpate the system model for QUIC -> minor update in network model -> still need to fix quic model and attack model

2025-05-19

Other

• finxing bug nealry ok to apt

2025-03-03

Other

• starting adding apt module -> still need to refactor old model

2025-02-19

Other

• fixing field dataclass param + init HTTP pljugin

2024-12-15

Other

• fixing package bugs

2024-12-12

Other

• add some dc string

2024-12-11

Other

• add packaged version -> still need to do test + udpate some path
• update for gperf

2024-12-10

Other

• update with docker base image for services + execution env ok -> now need to implement MiniP
• refactor of the configuration part nearly finished -> ok for docker compose IUT + tester ivy -> still need to test other netenv -> then integrate execution env -> then improving docker build -> finisiliazing observers

2024-12-09

Other

• continuing big config refactor
• update for new conf part

2024-12-08

Other

• update for new service arch

2024-12-06

Other

• Shadow nearly good -> still some hardcoded value to change for tester -> will be fixed with config update

2024-11-29

Other

• ivy tester ok on docker compose

2024-11-28

Other

• udpate for new panther -> still need to update some stuffs

2024-11-25

Other

• Still improve integration of Tester -> nearly ok still need to move ivy file, update path -> Still need to generalise for multiple env

2024-11-23

Other

• starting tester plugin

2024-09-16

Other

• add AI generated function spec + init jinja refactoring
• add AI generated function spec + init jinja refactoring

2024-09-03

Other

• update to python3.10 seems ok but strange stuff in ivTo_cpp.py
• merge from mcmillan -> still need to test

2024-08-25

Other

• adding nordsec result

2024-08-18

Other

• update system + minip test

2024-08-15

Other

• fix old/new introduce bugs
• intermediary push

2024-08-12

Other

• quic & minip attacker and mitm seem ok +- -> still bugs with mitn for quic

2024-08-08

Other

• attacker +- ok -> implementing cve + starting system model

2024-08-06

Other

• starting attacker model

2024-08-05

Other

• pushing advancment for tls connection spoofing but still not working, focusing on simple attacker model now

2024-08-03

Other

• encrypted version fast enough

2024-08-02

Other

• Problem with encryption -> need to change packet format

2024-07-31

Other

• fixed some bugs -> seems to have a problem in picoquic that send small initial packet -> TODO: do attacker api, merge attacker + mitm ? + do unified model for all protocols
• add basic mim method randomized + todo: merge attacker and mim endpoints + enable attacker to directly contact the victim + merge all protocol in one model

2024-07-30

Other

• generation seems ok -> remind: no random generation from function poping element from array !

2024-07-29

Other

• update before big update

2024-07-26

Other

• forwarding short header +- ok
• short header and padding +- supported now for apt
• short header and padding +- supported now for apt
• quic apt +- ok -> still need to implement coalesed packet everywhere with arra of packet

2024-07-24

Other

• minip + stream data ok -> quic nearly ok -> still need to merge everything

2024-07-23

Other

• update endpoint
• update endpoint -> remove client_ep/server_ep etc to encaspulate in mim_agent -> next removing/merging attacker/mim ? + add sub object to do attacker for each protocol

2024-07-22

Other

• using packet oject -> still need to fix a little bit stream_data_array + starting unifying model among different protocols

2024-07-17

Other

• mim +- ok, now good ip

2024-06-06

Other

• initiating minip attack template
• fix some bugs
• correct path
• update

2024-06-05

Other

• fix apt refactor + remove old quic model

2024-06-03

Other

• fix bugs on atp

2024-06-02

Other

• fix path
• fix path

2024-05-29

Other

• update path for new pfv arch
• starting adding http3

2024-05-28

Other

• update packet & frame super object

2024-05-27

Other

• starting unifying frame/packet
• add apt model -> still need to unify common interface

2024-05-21

Other

• small udpate attacker
• small udpate

2024-04-29

Other

• Update coap_endpoint.ivy file

Co-authored-by: AnonymousSEMA anonymous.sema.git@gmail.com - Add new Ivy files for BGP/CoAP protocol testing

Co-authored-by: AnonymousSEMA <anonymous.sema.git@gmail.com >

2024-04-25

Other

• update spec

2024-04-23

Other

• update coap

2024-04-15

Other

• update coap model

2024-04-12

Other

• update coap bases

2024-03-22

Other

• Update README.md

2024-03-18

Other

• Update README.md
• Update README.md

2023-12-19

Other

• base for coap
• remove bgp
• update bgp model

2023-11-24

Other

• push avancement on bgp, still prop to implem + deser/ser mostly finish

2023-11-03

Other

• add new protocol model

2023-10-23

Other

• update fix

2023-10-18

Other

• update for paper
• update for paper

2023-10-03

Other

• update rfc9001 model + signal heuristic + ping pong example

2023-09-02

Other

• fix some bugs - refactor extension + add props

2023-08-29

Other

• big push for time compoenent + timeout test

2023-08-13

Other

• quic_congestion and quic_rtt compile and seem working but need further integration and validation
• update base creating concept graph + quic_rtt + quic_congestion - error with quic_packet array and while loop -> now trying another approach to be more fast and do not modify ivy

2023-07-03

Other

• update repo to work with newer ivy version for QUIC -> check ivy_to_cpp

2023-06-27

Other

• update

2023-06-26

Other

• push quic

2023-01-30

Other

• remove debugging print
• fixing boolean quantifiers

2022-10-13

Other

• changing pointer to web site in README.md
• adding macos workflow

2022-10-12

Other

• fixed erase_unrefed bug, bump version to 1.8.24

2022-02-11

Other

• fixing tcp_host and other bugs

2022-02-10

Other

• fix invar checking in init

2022-02-06

Other

• workflow messing
• workflow messing
• workflow messing

2022-02-05

Other

• workflow messing
• workflow messing
• adding workflow

2021-12-10

Other

• bumped version to 1.8.22
• z3_thunk seems to be working, maybe
• still working

2021-12-09

Other

• z3_thunk works for no captured functions
• fixed destructor bug
• fixing z3_thunk

2021-12-08

Other

• bump version to 1.8.21
• fix bug in unique ids of properties

2021-12-07

Other

• bump version to 1.1.20
• fix import strip bug
• bump version to 1.1.19
• adding to keyval API

2021-12-03

Other

• ordered_set fixes

2021-12-01

Other

• adding lexord
• bump version to 1.1.18
• fixing ordered_set

2021-11-29

Other

• bump version to 1.1.17
• fixes for 2D processes

2021-11-24

Other

• bump version to 1.1.16
• fix to instantiate, add debug to trace"

2021-11-19

Other

• testing invariant check fix

2021-11-18

Other

• bump version to 1.8.15
• ops for bit vectors

2021-11-17

Other

• bump to version 1.8.14
• fixed cast of int types top bv

2021-11-13

Other

• bump to version 1.8.13
• fixes including process bug

2021-11-11

Other

• version bump to 1.8.12
• many features

2021-10-25

Other

• bumping version
• adding instance trace-back in error messages
• bump version
• bump version
• fix mod in numbers and order, issue #35
• fixing template isolate, adding counts to ivy_launch

2021-10-19

Other

• version 1.8.8
• bug fixes and template isolate

2021-10-17

Other

• bigger xterm fonts, remove impl from tcp_test

2021-10-13

Other

• changes

2021-10-07

Other

• added nat.mod, fixed cast
• adding cast operator to ivy_to_cpp

2021-10-06

Other

• adding packaging commands
• bumping version
• empty init fix and adding runs to ivy_launch

2021-10-03

Other

• improving reader randomization in test

2021-09-28

Other

• some udp changes and fix broken unbounded_queue

2021-09-25

Other

• fix tcp return address problem

2021-09-24

Other

• version bump
• fixing randomization, bmc, nat, queue

2021-09-18

Other

• about to try to fix randomization of range types

2021-09-09

Other

• various bug fixes for class

2021-09-04

Other

• version number

2021-09-02

Other

• version number
• hack to prevent core dump at end of test on linux

2021-09-01

Other

• fixes for Linux
• fixed saturation arithmetic bug

2021-08-22

Other

• fix g++ vectot compat

2021-08-17

Other

• moved up to version 1.8

2021-08-14

Other

• homeworks up to 4 working

2021-08-12

Other

• implemented class and for
• can bmc append example

2021-08-05

Other

• bmc of append example is working

2021-08-02

Other

• strange quantifier compilation bug

2021-07-27

Other

• various fixes
• fixes to extract_aws

2021-07-10

Other

• lamport_mutex test, proof and bmc are working

2021-07-09

Other

• fix compiler bug
• fix to lamport_mutex
• various fixes

2021-07-07

Other

• fix for named property bug

2021-07-03

Other

• many testing fixes

2021-07-01

Other

• fixed bug in handling of "this"

2021-06-27

Other

• linmapdel is working

2021-06-21

Other

• various language fixes

2021-06-17

Other

• fix for string parameters
• added some comments

2021-06-10

Other

• put/get consistency is working

2021-06-06

Other

• handling error responses

2021-06-05

Other

• working on concurrent transactions

2021-06-03

Other

• cleaning up dangling threads
• added threaded callbacks

2021-06-02

Other

• added txid
• first version of aws api generator
• working on parameterized networks

2021-05-29

Other

• working on network and process
• can test put/get

2021-05-28

Other

• add liveness examples from POPL'18, FMCAD'18 and FMSD'21 papers

2021-05-09

Other

• starting aws api

2021-05-05

Other

• adding ivy_launch

2021-05-02

Other

• adding parameter substitution in submodules and network library

2021-04-29

Other

• working on mc

2021-04-23

Other

• fixing performance bug caused by definitions dependent on mutable variables

2021-04-21

Other

• added explicit goal premises
• fix for relarray

2021-03-16

Other

• l2s fixes
• added aiger and abc as submodules
• fixes for compilation on mac
• mac install updates

2021-03-15

Other

• forgotten file
• working on builds on mac
• fixes to v3 compiler for mac

2021-03-14

Other

• fixed error reporting bug and added lemma to number_theory.ivy because of Z3 performance regression

2021-03-13

Other

• added aiger and abc as submodules
• small bugs

2021-03-10

Other

• liveness example with quantifier works with mc
• working on l2s and mc

2021-03-05

Other

• added mc tactic, working on l2s_full tactic

2021-02-27

Other

• fixing compositional liveness proof problems

2021-02-17

Other

• fixing skolemize tactic for temporal properties

2021-02-16

Other

• test file
• starting liveness fixes

2021-02-10

Other

• tentative l2s fix

2020-12-04

Other

• build fixes for Darwin

2020-08-26

Other

• fix regressions in arith_proofs branch
• number theory doc fixes
• number theory doc fixes
• number theory doc fixes
• forgotten file
• making doc page for number theory proofs

2020-08-22

Other

• still on gcd

2020-08-21

Other

• install doc bug

2020-08-19

Other

• got some arith lemmas
• fixing arith proofs
• adding files
• working on arithmetic proofs

2020-08-07

Other

• doc fixes
• spell check proving.ivy

2020-08-06

Other

• fixed mc regression caused by adding labeled proofs
• working on fba

2020-08-03

Other

• fixed bug in ivy_trace
• working on instantiate/witness

2020-07-31

Other

• adding skolem tactic

2020-07-30

Other

• adding labels in deduction
• added warning the associativity of if/then and implies are non-standard
• fix for bug in named proofs

2020-07-29

Other

• doc fix
• added premise lables in deduction.ivy
• added vcgen examples
• ivy_proof regression

2020-07-27

Other

• fix for issue #90
• working on proof documentation

2020-07-23

Other

• working on function tactic

2020-07-18

Other

• working on forward proof

2020-07-16

Other

• added counterexample annotations to proof goals

2020-07-15

Other

• added vcgen tactic

2020-07-14

Other

• checking in std.ivy
• removed getelem
• fix for issue #88

2020-06-30

Other

• got nbody benchmark working

2020-06-22

Other

• making a mess

2020-06-17

Other

• starting fp support

2020-06-15

Other

• fix issue #75

2020-06-08

Other

• fix for fix to issue #74
• fix for issue #74

2020-05-27

Other

• fixing issue #73
• middle of things

2020-05-25

Other

• fixes crash on match failure in ivy_proof

2020-05-20

Other

• fixed issue #71
• fixed issue #70
• fixing
• fix for issue #68

2020-05-18

Other

• fix for issue #67

2020-05-16

Other

• fix for issue #65

2020-05-05

Other

• starting isolate proofs

2020-04-19

Other

• issue #60

2020-04-18

Other

• issue63

2020-04-15

Other

• strange tls api problem

2020-04-14

Other

• fix for issue 62

2020-04-06

Other

• boolean parameter fix
• ivy_solver.py fix from networking branch
• ivy_isolate.py fix from networking branch
• ivyc fix
• adding file
• adding ip files
• added bv random

2020-04-05

Other

• chanhe test modelfil content
• change weighting of generate and receive in testing
• forgotten file
• fixi testing bug
• testing fixes
• moving hash_h to end of ivy_to_cpp.py

2020-03-22

Other

• allow module definitions in objects

2020-03-20

Other

• add broadcast shim example

2020-03-15

Other

• fixed missing parentheses in printed expressions, and printing of interpreted functions in trafes

2020-02-26

Other

• update chord2s example

2020-02-20

Other

• forgot pydot

2020-02-19

Other

• separate v2 comiler build
• fix for v2 compiler bootstrap
• fix install on mac typo
• fixing leader election test

2020-02-07

Other

• doc fixes
• fixed regression in diagram caused by annotations

2020-02-03

Other

• add build for v2 compiler

2020-01-28

Other

• fixed two l2s regressions
• fix invariant regression
• fixing cid overflow problem

2020-01-27

Other

• added bmc method
• testing fix

2020-01-23

Other

• fix for leader tutorial

2020-01-22

Other

• remove debugging
• changed operator syntax

2020-01-21

Other

• finite sorts
• explicit

2020-01-20

Other

• got borrow example working
• forgotten file
• forgotten file
• fixes for multi-paxos

2020-01-18

Other

• fixing mc traces
• more mc fixes

2020-01-10

Other

• adding REST files

2019-12-24

Other

• added leader liveness example

2019-12-20

Other

• l2s tactic fixes -- test_liveness2.ivy now passes

2019-12-19

Other

• new liveness example
• l2s_fixes
• l2s tactic syntax examples
• uncomment save in l2s
• working on l2s tactic

2019-12-02

Other

• Add missing pydot dependency

The ivy executable ends up importing ivy_graphviz, which requires pydot to be installed. - Fix PYTHONPATH dir in scripts/setup/z3.sh

The correct directory to add to PYTHONPATH is /python. Previously was just in z3.sh.

2019-11-27

Other

• serializer fix
• fix typos in doc/examples/networking
• leader tutorial finished

2019-11-26

Other

• changes
• continuing retire connection id implementation
• leader tutorial

2019-11-25

Other

• more mc fixes

2019-11-22

Other

• working on mc and trace fixes
• fixing mc issues

2019-11-20

Other

• removing extra commited files to avoid being overwritten by checkout

2019-11-19

Other

• commiting changes after installing forked version
• fixed ack credit incrementing and decrementing condition

2019-11-18

Other

• new connection id and retire connection id frame events
• fix for g++ flag
• commiting changes to ivy_to_cpp
• added retire_connection_id frame codec
• mistake

2019-11-15

Other

• ACK Rule

2019-11-14

Other

• windows install doc

2019-11-13

Other

• fixes for windows port
• fixed regression in unrolling

2019-11-12

Other

• windows install docs
• ip_spec.ivy changes
• windows build

2019-11-08

Other

• starting windows port
• more mac fixes

2019-11-07

Other

• mac build fix
• another example
• adding ip_spec example

2019-11-04

Other

• regression test for issue #49
• issue #49

2019-10-31

Other

• fix issue #48 in docs

2019-10-29

Other

• regression from fix to issue #46
• issue #46

2019-10-28

Other

• issue #47

2019-10-25

Other

• picoquic instructions

2019-10-24

Other

• logs for picoquic issue #969
• picoquic issue #969

2019-10-23

Other

• fixes issue #43
• language doc and regressions

2019-10-22

Other

• fixes issue #44

2019-10-18

Other

• docs

2019-10-17

Other

• issue #42

2019-10-15

Other

• ui fixes
• doc fixes
• add doc images
• mac doc

2019-10-14

Other

• more docs

2019-10-10

Other

• more docs
• more docs
• more docs
• more docs

2019-10-09

Other

• docs

2019-10-08

Other

• leader election example works again

2019-10-07

Other

• handling fail

2019-10-05

Other

• many fixes

2019-09-24

Other

• fixing server testers
• fix for g++-5

2019-09-16

Other

• Improved Formatting.
• Typos on #48 & #254 & #256 & #535

2019-09-13

Other

• picoquic
• z3 submodule update
• more build details
• adding picotls as submodule

2019-09-12

Other

• improving quic event logging
• updating to z3 4.7.1
• fixing wheel build
• fiddling with z3 lib location
• setup.py
• fixing submodules
• adding setup

2019-09-11

Other

• finding submodule z3 in test
• adding submodule build
• stop trying to strip constructors
• error message error

2019-09-10

Other

• fixed initial key setup

2019-09-05

Other

• working on stripping inits
• mac install change

2019-09-03

Other

• trying to fix website https
• fixing mac install instructions
• updated mac install from source instructions

2019-08-17

Other

• in the middle of big changes

2019-08-15

Other

• factoring out protocol layers

2019-08-02

Other

• cleaning up quic18

2019-07-31

Other

• another INSTALL.md

2019-07-30

Other

• INSTALL.md fixes

2019-07-03

Other

• added native inline section

2019-06-27

Other

• working on borrowing

2019-06-21

Other

• fixing mod_roots

2019-06-20

Other

• fixed move of refernce parameters, compiles up to s6
• implementing move

2019-06-15

Other

• added some error checking to s2/s3 compilers

2019-06-12

Other

• Fixing corner cases in argument passing

2019-06-10

Other

• removed file
• sys.command
• stage 1,2,3 compilers separated

2019-06-07

Other

• bootstraps
• fixed object slicing problem, ivy_to_cpp works
• pass_typeinfer works

2019-06-06

Other

• pass_flat works
• added constructor functions and their axioms
• reader works
• working on reader
• write and file exist
• read_file

2019-06-05

Other

• getenv
• can parse and print syntax.ivy
• compiler fixes

2019-06-03

Other

• hash.ivy and some fixes for bootstrap

2019-06-01

Other

• cow pointers

2019-05-28

Other

• unown

2019-05-27

Other

• doc fix
• working
• autoinstance

2019-05-26

Other

• logvar
• fixed undefined check for dot
• file annotations
• starting on file annotations
• before fixing destructors
• working
• working on var assignments

2019-05-25

Other

• starting var assignments
• working
• fixing ifst, whilest, type contexts
• tuple assignments
• working on tuples

2019-05-24

Other

• method call by reference
• method call by reference
• working on method call by reference
• working on call by reference

2019-05-23

Other

• working on prototypes

2019-05-22

Other

• prototypes
• resize
• starting resize
• cow in v1 compiler

2019-05-21

Other

• name mangling
• fixing ite and vector
• syntax errors, ite

2019-05-20

Other

• include path and traits for native types
• forgotten file
• forgotten file
• fix ivy_to_cpp
• fix function decl

2019-05-18

Other

• collections,order
• function

2019-05-17

Other

• standard traits
• enums and structs

2019-05-16

Other

• function representation
• verison, comments, standard library

2019-05-15

Other

• fixing zero-ary actions
• still working on foreign functions

2019-05-14

Other

• working on foreign functions

2019-05-13

Other

• fixed flattening of interpret
• adding dense representation

2019-05-12

Other

• dereference arrow
• bottom-up type inference and dot
• working on type inference

2019-05-11

Other

• working on variants

2019-05-10

Other

• this
• namespaces and prototypes

2019-05-09

Other

• namespace
• install instructions fixes
• adding quic documentation
• adding quic documentation
• fixing test.py
• fixing install docs
• fixing flattening
• objects

2019-05-08

Other

• instantiate

2019-05-07

Other

• include
• interpret
• headers

2019-04-30

Other

• install instructions
• working
• install changes
• working on destructor
• working on classes
• working
• ../../doc/INSTALL.md
• working

2019-04-28

Other

• added prog
• added vardc, typedc

2019-04-27

Other

• adding error.ivy
• working on ivy_to_cpp

2019-04-26

Other

• type_elide seems to work
• op type fix
• starting on builtins
• simple type infer working

2019-04-25

Other

• added hash
• starting typeinf

2019-04-24

Other

• added app
• ivy_to_cpp
• adding cpp

2019-04-22

Other

• adding property tactic

2019-04-19

Other

• decl groups
• action parses
• starting action
• fixing skip and ite
• added skip and ite

2019-04-18

Other

• added asgn and sequence
• pretty printing
• still on pretty printing
• pretty printing

2019-04-17

Other

• improving encoder
• fixing multiple output parameters
• recursive variants and multiple returns

2019-04-15

Other

• added forgotten file

2019-04-12

Other

• more windows porting
• windows porting
• fixing quadratic construction of Ite trees

2019-04-09

Other

• fixing echo
• handle retransmission of client hello

2019-04-05

Other

• working on modular temporal proofs

2019-04-03

Other

• using temporals to prove temporals

2019-04-02

Other

• starting on temporal tactics

2019-03-30

Other

• still working on quic18 client tester

2019-03-25

Other

• starting on client tester

2019-03-22

Other

• quic18 before changing encoding of crypto streams

2019-03-19

Other

• added some docs to ivy/README.md
• adding _finalize for test
• added some docs to ivy/README.md

2019-03-18

Other

• quic8 stream frames must respect rst_stream final length
• removed application close from quic_server_test_max
• handle one-byte payload length in quic18

2019-03-13

Other

• putting app close and stop_sending back in to quic_server_test_max

2019-03-06

Other

• quic18 add SNI, fix max stream id, error message on sendto fail

2019-03-05

Other

• switched to draft-18

2019-03-01

Other

• fixing regressions

2019-02-20

Other

• working on fraft-17

2019-02-19

Other

• echo example

2019-02-16

Other

• quic17 somewhat working

2019-02-15

Other

• anomaly24
• fixes for bft

2019-02-13

Other

• working on quic17

2019-02-12

Other

• quic17 work

2019-02-09

Other

• moving to draft-17

2019-02-08

Other

• anomaly24

2019-01-17

Other

• not sure

2018-12-21

Other

• quic16 anomaly22

2018-12-20

Other

• fixed problem with long integers in test

2018-12-19

Other

• working on max_data

2018-12-18

Other

• fixed precondition of connection_close

2018-12-17

Other

• adding flexibility to quic test script

2018-12-12

Other

• working on max data in quic

2018-12-08

Other

• quic16 added stop_sending frame

2018-12-07

Other

• adding some command line parameters to quic tester

2018-12-06

Other

• adding parameter defaults
• forgotten file

2018-12-05

Other

• changes for multiple stream in quic16

2018-11-29

Other

• quic15 anomalies 19,20

2018-11-28

Other

• quic15 anomalies 17,18
• quic15 anomaly16

2018-11-27

Other

• working on getting key establishment info from TLS
• add build directory to ivy_to_cpp
• fix to interference check

2018-11-24

Other

• quic15 anomaly15
• quant issues

2018-11-23

Other

• more forgotten files
• more forgotten files
• more forgotten files
• adding forgotten files

2018-11-22

Other

• working on quic15 and quant

2018-11-20

Other

• doc fixes
• quic15 doc fix
• quic15 anomaly11
• working on testing quant

2018-11-17

Other

• fixed action= option

2018-11-16

Other

• quic15 finishes one full test with encryption

2018-11-10

Other

• quic15 sent encrypted packet

2018-11-09

Other

• working on QUIC encryption

2018-11-08

Other

• fix bug in serdes

2018-11-07

Other

• quic15 merge passes tests
• fixed bug with old

2018-11-06

Other

• working on explicit invariants

2018-11-05

Other

• can extract keys from ptls
• working on tc1

2018-11-02

Other

• starting on proofs for conjectures

2018-11-01

Other

• working on picotls

2018-10-31

Other

• added tls_picotls
• weaken the requirement that migration is only detected on receiving a highest-numbered packet so that only 1rtt packets are considered;
• various fixes to fragment checker and interference checker

2018-10-30

Other

• fixed trace for if some

2018-10-26

Other

• working on picotls

2018-10-25

Other

• fixed missing returns in ivy_fragment

2018-10-24

Other

• some comments
• updates on quic15 anomaly10
• quic15 anomaly10

2018-10-23

Other

• fixed bug implicit universal quantifiers in fragment checker
• adding migration rules
• fixed bug in path_response in quic15
• fixed bug with return_context and boolean ops

2018-10-19

Other

• diagnosed picoquic anomaly9

• Update setup.py

• add a long description from README

• use codecs to prevent the crash during the installation on machines with non-standard locales.

2018-10-17

Other

• updating transport parameters to quic15

2018-10-16

Other

• serdes fixes for quic15
• about to switch to version 15

2018-10-15

Other

• quic15 changes
• adding ivy_libs.py

2018-10-12

Other

• picoquic anomaly9
• two client endpoints in quic15 tester
• working on migration in quic15

2018-10-11

Other

• adding new_connection_id in quic15

2018-10-09

Other

• anomaly8
• more on testing
• working on quic test framework

2018-10-08

Other

• ivy-mode.el: clean up

• use standard source layout

• add packaging directives
• use defconst/defvar for top-level variables
• add customize-group for and customize variables for user-editable variables

2018-10-04

Other

• working on stream frame testing in quic14
• testing max_stream_data in quic14

2018-10-03

Other

• quic14 connectino close seems to work
• details for quic14 anomaly7
• quic14 anomaly7
• modified quic14 spec for anomaly6
• quic14 anomaly6
• small fixes
• more graphviz problems

2018-10-02

Other

• fixed problem with bmc in cti mode and initializers
• fixes to ivy_graphviz
• Update README.md

Added installation commands for linux and windows.

2018-09-27

Other

• working on parsing partial TLS messages in quic14

2018-09-26

Other

• quic14 test rst_stream seems to work
• working on rst_stream in quic14
• quic14 packet number problem temporarily fixed

2018-09-25

Other

• in quic14 test, can send stream frames, but packet number decoding is incorrect

2018-09-24

Other

• acks seem to work in quic14 test

2018-09-22

Other

• working on acks in quic14 tester

2018-09-20

Other

• extending macro instantiation
• trying to send bytes to tls in quic14

2018-09-19

Other

• got up to tls_recv_event on quic14 test
• got one quic14 packet sent to server

2018-09-18

Other

• small fixes for quic14 tester
• working on tester for quic14

2018-09-17

Other

• can monitor picoquic.pcap

2018-09-15

Other

• working on picoquic.pcap

2018-09-13

Other

• working on quic14 deser

2018-09-12

Other

• some changes for CORE
• fix handling of cids in quic

2018-09-11

Other

• performance fixes for quic_server_test
• minquic anomaly
• fixing up dependent parameters and quic_server_test

2018-09-07

Other

• adding constructor axioms

2018-09-06

Other

• finishing window_adt

2018-09-05

Other

• creport2.ivy
• fixing mc merge
• creport example

2018-09-03

Other

• adding file

2018-08-23

Other

• working on dependend fields

2018-08-11

Other

• working on dependent input fields

2018-08-10

Other

• in the middle of adding dependent inputs in test

2018-08-09

Other

• quic_server_test can generate data packet, but very slowly

2018-08-08

Other

• more gnutls

2018-08-07

Other

• working on gnutls

2018-08-04

Other

• updating install instructions

2018-08-03

Other

• testing gnutls

2018-07-31

Other

• quic tls work

2018-07-26

Other

• working on quic_server_test, adding extensions to tls

2018-07-25

Other

• forgotten files

2018-07-04

Other

• fol command is actually fo

2018-06-29

Other

• reverse breaking change to array spec
• working on quic_server_test
• adding deserializer for quic

2018-06-27

Other

• added serializer/deserializer parameters to udp_impl
• adding udp_impl

2018-06-25

Other

• update udp_test to 1.7, remove debugging from ivy_parser

2018-06-19

Other

• can generate full tls handshake, z3 slow

2018-06-18

Other

• hooking tls up to quic

2018-06-17

Other

• moving to QUIC version 11

2018-06-16

Other

• working on quic generation

2018-06-12

Other

• adding intbv

2018-06-10

Other

• small ivy_to_cpp fix

2018-06-09

Other

• refactored quic_connection into smaller actions

2018-06-08

Other

• added override attribute
• fixing test bugs

2018-06-07

Other

• added inference of TLS events

2018-06-06

Other

• starting quic test branch

2018-06-05

Other

• adding tls

2018-05-31

Other

• adding quic traces
• more quic frames

2018-05-30

Other

• added quic max_stream_data frames
• working on quic close connection frame

2018-05-29

Other

• adding parsers for quic stream_reset and max_stream_id frames
• adding parsers for quic stream_reset and max_stream_id frames
• forgotten file

2018-05-28

Other

• updating docs
• update some examples for new array module
• fixing ivy_to_cpp problem
• some work on back pressure in quic

2018-05-26

Other

• quic spec additions
• fixing parser problem (combining term and fmla)

2018-05-25

Other

• working on transport parameters

2018-05-24

Other

• tls_deser starting to work

2018-05-23

Other

• adding fragment tests, fixing list_reverse doc

2018-05-22

Other

• checking in ivy_to_md
• fixes to fragment checker

2018-05-21

Other

• doc fixes

2018-05-18

Other

• starting decidability doc

2018-05-17

Other

• fixing some problems with ivy_to_cpp
• theorem branch passes tests
• handle weird quoting of names in recent z3
• handling finite types in new fragment checker

2018-05-16

Other

• fixing up proving doc
• fixing induction example in indexset
• ivy_prover problems

2018-05-15

Other

• sht works again

2018-05-12

Other

• sht still not working
• fixing bugs in new fragment checker

2018-05-11

Other

• passes run_expects
• working on new fragment checker

2018-05-10

Other

• working on new fragment checker

2018-05-09

Other

• indexset works
• trying to get indexset to work again

2018-05-08

Other

• working on array reverse example

2018-05-07

Other

• adding normalize_ops

2018-05-05

Other

• working on alpha conversion bugs

2018-05-04

Other

• working on example theorems

2018-05-03

Other

• fixing proof order
• fixing ivy_to_md
• proving.ivy almost works

2018-05-02

Other

• working on proving doc

2018-05-01

Other

• fixing quic instructions
• stashing
• stashing again

2018-04-30

Other

• stashing

2018-04-28

Other

• working on proving.md

2018-04-27

Other

• working on dox

2018-04-26

Other

• fixing list_reverse.md
• fixing list_reverse.md
• fixing list_reverse.md
• adding list_reverse.md
• quic readme fix
• spelling
• adding README.md
• adding dox
• forgotten file
• working on array reversal example

2018-04-25

Other

• alpha conversion seems to be working
• working on alpha conversion

2018-04-24

Other

• working on capture
• fix for matching
• working on capture in ivy_proof

2018-04-23

Other

• fixing tactic compilation

2018-04-21

Other

• still on theorem prover

2018-04-20

Other

• working on assume tactic

2018-04-19

Other

• working on prover

2018-04-18

Other

• fixing some fragment checker bugs

2018-04-17

Other

• autoinstance and struct
• implementing autoinstance
• adding TLS records
• starting TLS interface

2018-04-16

Other

• fixed unsoundness: added detection of free variables in if conditions
• something for quic
• testing markdown syntax
• working on ivy_to_md
• quic to md
• adding ivy_to_md

2018-04-15

Other

• quic anomalies
• anomaly in minquic

2018-04-13

Other

• added "isa"
• small cleanup to quic

2018-04-11

Other

• fixed glitch in example
• fixing tcp thread leak problems

2018-04-07

Other

• removed Z3 paths from repl compile
• more on quic

2018-04-06

Other

• fixes for object continuations, C++ thunks, quic
• fixed broken packet nuymber decode in quic
• fix for ivyc
• adding ivyc command

2018-04-05

Other

• fixing large integer constants
• forgot ip.ivy
• forgot pcap.ivy
• getting quic running
• adding quic files
• middle of something

2018-04-04

Other

• fixed socket leak in tcp
• quic stream packets parse

2018-04-03

Other

• fixing some error messages in ivy_isolate
• tcp send queueing seems to be working
• messing with queueing tcp sends

2018-04-02

Other

• added "segment" module to collections
• messing with deser

2018-03-30

Other

• starting on frame parsing

2018-03-29

Other

• fix to bug in ivy_socket_deser affecting tcp

2018-03-24

Other

• moving some files

2018-03-23

Other

• small doc change
• parsing the QUIC packet headers and tracking packet number seem to work
• small changes for testing TCP

2018-03-22

Other

• relaxed interference rule for initializers
• adding hex output

2018-03-13

Other

• working on disk_token_ring

2018-03-12

Other

• still working on thunk

2018-03-10

Other

• working on thunk
• variants seem to be sort of working

2018-03-09

Other

• disk sync callbacks seem to work

2018-03-08

Other

• file works in crashpong1
• adding disk impl to crashpong1

2018-03-07

Other

• added crashpong example
• adding crash

2018-03-06

Other

• added TCP_NODELAY
• tcp support added to stdlib
• tcp seems to be working

2018-03-05

Other

• fixed unsoundness in interference check
• still working on tcp

2018-03-02

Other

• working on tcp

2018-02-27

Other

• fixed bug in get_isolate_attr
• small change to ivy_mc
• fixed error message in ivy_isolate
• finite model checking working for flash2

2018-02-24

Other

• fixing model checking cex output
• fixing mc macro bug

2018-02-23

Other

• added attributes method and separate
• added mc schemata to std include
• implemented separate option

2018-02-22

Other

• fixing up vsync_paxos

2018-02-21

Other

• fixed isolate parameter check bug
• fixed but introduced by multiple inits
• fixed with in ivy_isolate.py

2018-02-20

Other

• adding if tactic

2018-02-18

Other

• fixed strlit deser

2018-02-17

Other

• allowing multiple after and before mixins for a given action in same name space
• fixed bug that spuriously added undefined "with" arguments to hierarchy

2018-02-16

Other

• added trace option to docs
• fixed broken test
• still on trace

2018-02-14

Other

• improved error message about invariants
• compile quantifiers over iterable
• adding seed and incremental options

2018-02-13

Other

• fixed bug in VC generator that caused formulas with many quantifiers
• fixed error message on inconsistent axioms/initial conditions
• fixes bug with type object alias and with

2018-02-08

Other

• fixing proof syntax
• fix for timeout.ivy

2018-02-07

Other

• fix FAIL PASS problem
• doc fix
• added some command-line docs

2018-02-06

Other

• making assert=lineno option apply to invariants
• added option for z3 macro_finder
• turn off run-time checking of invariants
• fixed problem with asserts at same line number in different actions

2018-02-05

Other

• messing with yacc bugs

2018-01-29

Other

• removing unneeded lemmas from vsync_paxos_ms

2018-01-24

Other

• ibm-cache-N works with invariants
• starting on ibm-cache-N with invariants
• toma8.ivy works
• vsync_paxos works, needs cleanup

2018-01-23

Other

• still working on vsync_paxos
• still on vsync_paxos

2018-01-22

Other

• still working on vsync_paxos

2018-01-21

Other

• problem with quantifiers in assumptions in mc

2018-01-20

Other

• working on vsync_paxos_mc

2018-01-19

Other

• starting vsync_paxos
• flash2_mc works

2018-01-18

Other

• flash2 invariant works
• working on flash with induction

2018-01-17

Other

• flash_mc works
• working on flash_mc

2018-01-16

Other

• toma8_mc works
• working on assert in mc

2018-01-15

Other

• toma8_mc reservation ststaino properties ok
• stop logic.py from commuting disjunctions

2018-01-13

Other

• working on tomasulo

2018-01-12

Other

• fixing let tactic

2018-01-11

Other

• added let tactic, invariant proofs

2018-01-03

Other

• got rid of some extraneous stvars in mc

2018-01-02

Other

• schema instantiation works for ibm-cache-N
• schema instantiation works for client_server_mc3
• forgotten
• adding German cache model
• working on schemata in mc

2018-01-01

Other

• client_server_mc2 works

2017-12-29

Other

• forgotten
• forgotten files
• more fixes for enums in gui

2017-12-28

Other

• fix bug in ivy_graph.py
• abstract conterexample OK on client_server_mc.ivy

2017-12-27

Other

• working on model checking counterexamples

2017-12-23

Other

• starting to add annotations to transition relatiosns
• about to work on trace generation
• Typo on #29

And some minor fixes (proposal) - Typo on #01 - Update URL - Typos - useless commit

2017-12-22

Other

• getting possibly good abstract counterexample for client_server_mc.ivy

2017-12-21

Other

• nowhere
• quantifier instantation in mc partly works

2017-12-20

Other

• axiom instantiation partly works
• starting on propositional abstraction

2017-12-19

Other

• fix "if *" regression
• working on enumerated types
• fixed skolemization bug

2017-12-18

Other

• working on encoding finite sorts

2017-12-16

Other

• starting on ivy_mc

2017-12-15

Other

• workaround for Jekyll relative path bug
• jekyll test
• jekyll test
• some doc updates for 1.7
• toy_consensus now compiles and runs

2017-12-14

Other

• fixed tilelink regression
• working on parameter

2017-12-13

Other

• toy_consensus compiles
• toy_consensus verifies but does not compile

2017-12-12

Other

• working on method call with variables
• still working on toy_consensus

2017-12-10

Other

• working on toy_consensus

2017-12-09

Other

• working on toy_consensus

2017-12-08

Other

• invariant seems to work, updating docs
• forgotten file
• working in invariant

2017-12-07

Other

• working on invariant
• implemented require and ensure
• specifiction, implementation, private seem ok
• implememting specifiction, implementation, private

2017-12-06

Other

• fixing reporting of implementations and monitors
• updating docs for summary
• added back assert= feature
• passes tests

2017-12-05

Other

• foo

2017-12-04

Other

• adding "type this"

2017-12-01

Other

• further cleanup of sht table and docs
• cleaning up sht table
• sht table is working again
• trying to get sht to work again

2017-11-30

Other

• working on updateing docs to 1.7

2017-11-29

Other

• three soundness fixes seem to work

2017-11-28

Other

• working on unsoundness
• cone passes tests

2017-11-27

Other

• temporary
• still working on cone

2017-11-23

Other

• working on cone reduction

2017-11-21

Other

• fixed tester to unlovk object after construction
• fixed call with variable on lhs
• getting call by reference to work with method calls

2017-11-18

Other

• working on parameter aliasing

2017-11-17

Other

• fixed bug in sequence_iterator

2017-11-16

Other

• adding inplace modification

2017-11-14

Other

• fixing UDP config problems

2017-11-07

Other

• adding config to udp
• some fixes for class extraction
• cancel threads on class destructor
• added sleep to class example
• class creation might be working
• threads might be working

2017-11-03

Other

• do not havoc parameters if compiling

2017-11-02

Other

• reinstanted z3 macro_finder option

2017-10-31

Other

• fixed fragment checker bug

2017-10-16

Other

• fixed in/out parameter bug and array.set bug, removed Z3 macro_finder option which produced bad models

2017-10-04

Other

• fixed unsoundness in function definitions
• integrating liveness

2017-10-02

Other

• integrating odedp liveness branch

2017-09-27

Other

• fix

2017-08-10

Other

• fixed regressions

2017-08-05

Other

• fixes for testing vsp

2017-08-04

Other

• changed isolate semantics for properties

2017-08-03

Other

• working on extracting vsp

2017-08-02

Other

• fixing fragment checker

2017-08-01

Other

• workaround for MBQI looping in z3

2017-07-31

Other

• debugging fragment checker

2017-07-21

Other

• working on vsp

2017-07-20

Other

• fix error messages
• working on vsp

2017-07-18

Other

• adding ivy/README.md
• fixing fragment checker to allow quantifiers over finite sorts

2017-07-13

Other

• removed debug pring
• fixed module reference in ivy_show

2017-07-12

Other

• fix indexset3.ivy

2017-07-10

Other

• fixing fragment checker and prover

2017-07-09

Other

• adding comments
• working on fragment checker, indexset3.ivy

2017-07-08

Other

• working on theory fragment checker

2017-07-07

Other

• remove debugging assert
• working on fragment check

2017-07-05

Other

• fixed problem with alias in native code
• fix for hang in get_small_model when axioms are not EPR
• misc fixes
• fix for cal with method syntax

2017-07-04

Other

• fix error messages
• install doc fix
• temporary fix for parser infinite loop
• fixing indexset2.ivy

2017-07-03

Other

• working on prover

2017-07-01

Other

• working on prover

2017-06-29

Other

• add file
• fixes for matching
• working on prover documentation

2017-06-28

Other

• extending isolate
• working on named

2017-06-26

Other

• working on recursion
• fix for run_expects
• fix for z3-4.5.0

2017-06-25

Other

• working on recursion

2017-06-24

Other

• forgotten file
• working on recursive definitions

2017-06-21

Other

• toy_consensus and fixes

2017-06-12

Other

• Fixed trace=true in an action without parameters
• proof of majority property

2017-06-11

Other

• cardinality tests

2017-06-10

Other

• fix for udp and tcp
• removing tabs from MSV examples
• adding MSV examples
• small doc fix

2017-06-06

Other

• doc fixes

2017-05-22

Other

• adding file

2017-05-21

Other

• updating installation documentation
• support built-in z3

2017-05-19

Other

• added empty transition target in scenario
• fix for mixin parameter inference

2017-05-18

Other

• remove debug prints
• fixing scenario bugs
• adding scenario after transitions
• small fix

2017-05-16

Other

• clarification in installation instructions.

2017-05-15

Other

• initial implementation iof scenario

2017-05-12

Other

• fixes for windows
• clarification in installation instructions.
• fix typos.
• update README.md with installation instructions.

2017-05-11

Other

• update .vscode/settings.json with more ignore patterns.
• open text files with newline translation support (missing files from previous commit).
• open text files with newline translation support (mode rU instead of r).
• adjust z3 PYTHONPATH setting to be compatible with version of z3 used.
• separate ivy dependencies from other apt packages.
• checkout compatible z3 submodule commit.
• got ivy gui working over ssh with x11 forwarding.

2017-05-09

Other

• cross-pollinate with flutterbye vagrant/installation scripts.

2017-05-08

Other

• working on windows release
• working on windows release

2017-05-05

Other

• fix bugs in python environment setup.
• rename scripts/setup/userspace.sh to .../userland.sh.
• add python to path.

2017-05-04

Other

• tests now pass

2017-05-03

Other

• from class dry run
• updated Vagrantfile from latest in flutterbye repository.

2017-04-19

Other

• partially fixing strbv overflow problem

2017-04-15

Other

• allow native quote in after, improve loop bound detection

2017-04-11

Other

• added bit vector ops

2017-03-30

Other

• fixes for MSV

2017-03-29

Other

• adding VS solutions for MSV
• working on MSV exercises

2017-03-28

Other

• fixes for windows and udp.ivy
• working on MSV examples

2017-03-27

Other

• visual studio extension
• visual studio integration

2017-03-26

Other

• changes for vs and multiple compile

2017-03-25

Other

• working on tutorial
• fix to nested destructor assignment

2017-03-22

Other

• working on nested field references

2017-03-18

Other

• forgotten file
• forgotten file
• repstore3 is working

2017-03-17

Other

• repstore2 and repstore2bug are working
• repstore2 and repstore2bug are working
• adding sequential repstore

2017-03-16

Other

• repstore seems to be working
• still working on repstore example
• sorking on repstore example

2017-03-15

Other

• working on variants

2017-03-14

Other

• working on replicated key/value store example

2017-03-13

Other

• working on chain rep example

2017-03-12

Other

• adding options to tester
• forgotten file

2017-03-11

Other

• fixing many bugs

2017-03-07

Other

• working on variants
• fixed error in setup.py

2017-03-05

Other

• trying to make symbolic execution more efficient prompt

2017-03-03

Other

• about to try improving symbolic execution prompt

2017-03-02

Other

• update z3 submodule

2017-02-28

Other

• simplify Vagrantfile.

2017-02-23

Other

• more fixes for ivyspec

2017-02-22

Other

• update .gitattributes for shell scripts.
• some fixes for ivyspec
• exclude files in vscode workspace settings.

2017-02-20

Other

• fixes

2017-02-19

Other

• z3 now works in vagrant environment.

2017-02-17

Other

• use git root detection instead of relative paths in provisioning scripts.

2017-02-16

Other

• added vagrantfile, z3 submodule, and setup scripts.

2017-02-11

Other

• handle empty struct

2017-02-02

Other

• fix to parsing of numeric arrays in repl

2017-01-30

Other

• fixed but in integer constant thunks

2017-01-27

Other

• various fixes

2017-01-25

Other

• changed assert to exit on strbv overflow

2017-01-24

Other

• fix for redirect on windows
• fixing redirect
• adding output redirect for test
• changed null_type module to use 0x7fffffff for null value

2017-01-23

Other

• fixed bug in to_solver for arrays
• generation bug

2017-01-20

Other

• serialization fixes

2017-01-17

Other

• add encoding feature

2017-01-12

Other

• fixes for var bug and method call
• event parsing fixes

2017-01-10

Other

• some fixes for repl on windows

2017-01-05

Other

• working on var
• windows porting

2017-01-03

Other

• some changes for z3.py changes

2016-12-31

Other

• working on var
• strbv type seems to work

2016-12-30

Other

• adding strbv, delegate is not working...

2016-12-26

Other

• working on gen for strings

2016-12-25

Other

• working on loop unrolling

2016-12-24

Other

• removing -lz3 from repl compile

2016-12-23

Other

• fixing field handling, extending to actions

2016-12-22

Other

• still trying to break dependency
• still trying to break dependency

2016-12-21

Other

• trying to remove dependency on pygraphviz
• added destructor references with dot notation

2016-12-20

Other

• fixing repl with trace

2016-12-19

Other

• adding isolate = this

2016-12-17

Other

• working on event viewer

2016-12-14

Other

• more repl tests

2016-12-13

Other

• more repl tests
• cleaning up
• workiong on testing repls

2016-12-08

Other

• not much
• testing tests pass

2016-12-06

Other

• adding testing regression tests

2016-12-05

Other

• unknown

2016-12-04

Other

• eliminating unused definitions in test gen
• adding before_exports

2016-12-03

Other

• arraygen.ivy
• unknown

2016-11-29

Other

• working on testing

2016-11-19

Other

• fixing up target=test

2016-11-18

Other

• working on compiling strings, enums

2016-11-17

Other

• fixing bugs
• adding string type

2016-11-15

Other

• working on event viewer
• working on event viewer

2016-11-14

Other

• adding event viewer

2016-11-12

Other

• adding event parser

2016-11-11

Other

• testing fixes

2016-11-08

Other

• fixing test bugs

2016-10-25

Other

• removed some debug prints
• fixed problems with implicit imports

2016-10-21

Other

• fixing up chord example

2016-10-20

Other

• typo

2016-10-19

Other

• fixed run_expects
• fixed bug with abstracted "after init"

2016-10-17

Other

• more changes
• change

2016-10-09

Other

• changed cycle counting for timeouts
• reduced timeout for test harness to 1ms
• fixed bug reported no im[plementation for imported action
• removed () from test logs
• removed ext: from test logs
• fixed import action bug in ivy_isolate.py

2016-10-04

Other

• fixed ivy_to_cpp thunk bug
• tests pass
• fixed bug in ivy_isolate.pu

2016-10-03

Other

• fixed bug in interference check

2016-10-01

Other

• working on testing tutorial

2016-09-29

Other

• works testing buggy transport layer

2016-09-28

Other

• simple example of generating structures is working
• more on generating structs
• working on token ring example

2016-09-26

Other

• working on hash thunk

2016-09-25

Other

• adding hash thunk

2016-09-21

Other

• finished leader example in testing tutorial

2016-09-20

Other

• working on testing tutorial

2016-09-19

Other

• working on testing tutorial

2016-09-17

Other

• working on target=test

2016-09-15

Other

• passes regressions
• sht tutorial completed
• sharded hash table tutorial runs
• sht tutorial example checks
• working on sht tutorial

2016-09-14

Other

• added doc page on sht trans
• reworking sht queue

2016-09-13

Other

• adding trans module to sht tutorial

2016-09-12

Other

• reworking delmap

2016-09-11

Other

• adding table doc

2016-09-10

Other

• table_test works
• adding files
• adding file
• fixing bugs for sht example

2016-09-09

Other

• adding files
• starting tutorial on sht

2016-09-08

Other

• all tests pass and tutorial examples run
• more bug fixing
• more bug fixes
• bug fixing

2016-09-07

Other

• bug fix
• cleaning up bugs

2016-09-06

Other

• working on arrayset

2016-09-05

Other

• working on bounded quantifiers, arrayest example

2016-09-03

Other

• working on arrays

2016-09-01

Other

• sht running multi-process

2016-08-31

Other

• added reply messages to sht
• really fixing sht liveness bug
• sht liveness fix
• sht compiles
• working on compiling sht

2016-08-30

Other

• putting sht together

2016-08-29

Other

• sht trans checks
• workin on sht table

2016-08-28

Other

• working on sht

2016-08-27

Other

• working on sht table proof
• working on per-assertion checking

2016-08-26

Other

• working on definition unfolding
• working on definition unfolding

2016-08-25

Other

• sht table is tested
• test_table compiles
• working on sht

2016-08-24

Other

• working on struct
• working on structs

2016-08-23

Other

• adding while

2016-08-20

Other

• working on "for some" and collections.ivy

2016-08-19

Other

• fixing target=gen problem"
• addint initializers

2016-08-18

Other

• working in parameterized init

2016-08-17

Other

• working on networking doc

2016-08-16

Other

• working on C++ callbacks

2016-08-14

Other

• working on udp

2016-08-13

Other

• working on select in runtime
• working on extract

2016-08-12

Other

• working on leader in REPL

2016-08-11

Other

• adding helloworld section
• working on native code and repl

2016-08-08

Other

• adding foreign function interface and REPL support

2016-08-06

Other

• adding leader section to doc, improving diagram

2016-08-05

Other

• still working on prettifying

2016-08-04

Other

• working on prettier formula printing

2016-08-03

Other

• lots of debugging, fixing model_to_diagram

2016-08-02

Other

• fixing issues with instance paramenters and implicit parameters to mixins

2016-08-01

Other

• fix for issue #1
• fix broken link

2016-07-30

Other

• adding doc example
• adding property

2016-07-29

Other

• adding types in objects and inequality macros

2016-07-27

Other

• improving coverage check messages
• adding implement

2016-07-26

Other

• added before and after declarations

2016-07-16

Other

• fixing completeness check

2016-07-15

Other

• adding completeness check

2016-07-14

Other

• fixing interference check
• fixing sht example, fixing boolean locals

2016-07-09

Other

• starting check_interference

2016-07-08

Other

• add "private"

2016-07-07

Other

• fixing ivy_check and some bmc problems
• fixing ivy_check

2016-07-06

Other

• modified tilelink test makefile to keep up with tilelink refactoring
• pulled out boilerplate into std
• factored out ordered_set structure

2016-07-05

Other

• sht_abs working with stripping
• working on stripping isolate parameters
• sht delegationmap impl proof works but messy

2016-07-04

Other

• working on sht delegation map

2016-07-02

Other

• working on maximizing/minimizing

2016-07-01

Other

• updated tests for new project structure
• updated tests for new project structure
• modified tilelink spec to require ordered release beats
• adding destructor and some

2016-06-29

Other

• fixing inconsistency in sht example

2016-06-25

Other

• working on destructors

2016-06-23

Other

• fixed tilelink spec handle grants without data

2016-06-14

Other

• fixing ivy_theory and working on sht refinement

2016-06-13

Other

• fixing cti regression
• workaround for Z3 EPR incompleteness
• workaround for z3.py regression in z3 4.4.2
• fixed file not found reporting
• fixing plugin loading regression
• fixing error reporting in ivy_to_cpp

2016-06-10

Other

• starting to refine network model in sht

2016-06-09

Other

• added test for ivy_to_cpp
• fixed some regressions in ivy_to_cpp

2016-06-08

Other

• added Mac installation notes

2016-06-07

Other

• adding Windows install documentation
• fixing up for python packaging

2016-06-04

Other

• fixing ivy_test
• reorg for python package

2016-06-03

Other

• fixing projections in new ui, adding test
• working on sharded hash table

2016-06-01

Other

• forgotten file
• raft log model changes

2016-05-31

Other

• adding raft_logs example

2016-05-28

Other

• adding diagram to cti

2016-05-27

Other

• fixing home page again
• fixing home page again
• fixing home page
• fixing README
• fixing up regression tests

2016-05-26

Other

• invariant example and cti issues
• working on induction example

2016-05-25

Other

• adding docs

2016-05-24

Other

• adding website deployment cruft
• trying to fix github url problem
• adding web site
• adding assertion check to cti tui and some docs

2016-05-21

Other

• working on language features

2016-05-20

Other

• adding to language doc

2016-05-19

Other

• removed some prints
• still fixing regressions in gui_refactor
• fixing regressions in gui_refactor
• fix for zero size pane in tk gui

2016-05-18

Other

• give line numbers of asserts in ivy_to_cpp, fixed serialization issue in tilelink testbench
• cleanup for tilelink unit tester

2016-05-17

Other

• cleaning up tilelink tester
• fixed some regressions on tilelink unit tester

2016-05-13

Other

• added instructions for getting uncore configs from kenmcmil fork
• removed old targets from tilelink/unit_test/Makefile
• fixed backward compat problem parsing concept spaces

2016-05-06

Other

• new gui does leader example pretty well

2016-05-05

Other

• working on leader example

2016-05-04

Other

• working on ivy_ui_cti.py
• created ivy_ui_cti.py
• still working on transition widget in new gui
• working on transition widget in new gui

2016-05-03

Other

• adding ui plugins

2016-05-02

Other

• fixing transitive relations in new gui

2016-04-29

Other

• fixing new gui problems

2016-04-28

Other

• fixed tilelink proof

2016-04-27

Other

• fixing "delegate to"
• adding mixord and "delegate to"

2016-04-26

Other

• fix to ivy_to_cpp
• working on check

2016-04-25

Other

• working on gui refactor

2016-04-22

Other

• working on check

2016-04-21

Other

• adding ivy_check

2016-04-20

Other

• working on theory checking

2016-04-19

Other

• working on toy_lock proof
• got toy_lock working over UDP

2016-04-15

Other

• working on code extraction

2016-04-14

Other

• working on emitting code for toy lock example

2016-04-13

Other

• gui refactor, working on ART

2016-04-12

Other

• refactoring gui, adding tests
• still in ui refactor

2016-04-11

Other

• still on gui refactor

2016-04-10

Other

• still on gui refactor

2016-04-09

Other

• still in ui refactor

2016-04-08

Other

• rearranging example files and adding gitignore files
• still on concept graph refactor

2016-04-07

Other

• starting concept graph refactor

2016-04-06

Other

• still refactoring ui
• refactoring GUI to use MVC pattern

2016-04-04

Other

• added emacs mode
• refactoring ui

2016-04-03

Other

• fixing some ui issues

2016-04-02

Other

• working on bit vectors

2016-04-01

Other

• refining toy lock model
• more on refinement

2016-03-30

Other

• adding after mixins
• still working on integer support

2016-03-29

Other

• adding integer support
• bigger example
• adding int support

2016-03-23

Other

• adding forgotten file

2016-03-21

Other

• fixes for l2

2016-03-20

Other

• working on tilelink progress properties

2016-03-19

Other

• working on progress properties

2016-03-17

Other

• adding workaround for uncached op problem

2016-03-16

Other

• updated README
• shows uncore issue 29
• handling derived predicates in test gen

2016-03-15

Other

• adding language doc

2016-03-12

Other

• adding testbench support for uncached tilelink clients
• Makefile
• update README

2016-03-11

Other

• update README
• shows uncore issue 23

2016-03-10

Other

• not much

2016-03-09

Other

• getting BroadcastHub to work again
• small tilelink changes

2016-03-08

Other

• making compatible with tilelink uncore unit-testing branch

2016-03-07

Other

• shows uncore issue 20
• install fixes

2016-03-06

Other

• adding ivytocpp
• adding install instructions

2016-03-03

Other

• working on L2 cache

2016-03-02

Other

• L2CACHE bug #1

2016-03-01

Other

• some tilelink spec refactoring

2016-02-29

Other

• BroadcastHub running without issues

2016-02-27

Other

• working on multi-client tilelink spec

2016-02-26

Other

• added manager txids to tilelink spec
• working on BroadcastHub, about to change txids in tilelink_concrete_spec
• working on BroadcastHub

2016-02-25

Other

• working on coherence manager tester

2016-02-24

Other

• working on test harness to tilelink coherence manager

2016-02-22

Other

• working on tilelink tester
• adding Makefile for tilelink tester
• working on tilelink tester

2016-02-20

Other

• working on c++ test generation

2016-02-19

Other

• working on c++ test generation

2016-02-15

Other

• Cleaned up examples/pldi16
• Better structure_renaming for nicer projections.
• Fixed off by 1 bug in bmc_conjecture.
• Fixed bug in ivy_bmc.py
• Added ivy_bmc.py and hide redundent graphs and buttons from IvyMain widget.
• Converted leader election to ivy1.3 + started converting database_chain_replication.

2016-02-14

Other

• Added fixing of random seeds, and fixed bug causing gray edges.
• Added missing file: widget_cy_graph_iframe.html
• Started to convert pldi16 examples to ivy1.3
• More adjustments to the new UI.
• Added .gitignore
• Updated the new UI and the CTI based interaction mode to work with function symbols.

For now, switched to numerals=False, since numerals break the assumptions of the type inference, which is used by concept.py.

2016-02-13

Other

• adding ivy_to_cpp

2016-02-12

Other

• fix learning switch example

2016-01-29

Other

• comments

2016-01-22

Other

• protocol props checked for tilelink_concrete_directory.ivy
• working on tilelink directory model
• adding tilelink directory example

2016-01-21

Other

• protocol props checked for tilelink_concrete_snoopy.ivy
• cleaning up tilelink spec
• protocol props checked for tilelink_concrete_unordered_channel.ivy
• working on tilelink invariants
• working on tilelink invariant

2016-01-20

Other

• working on tilelink invariants
• working on tilelink invariant

2016-01-19

Other

• working on tilelink invariants
• working on tilelink invariant

2016-01-18

Other

• working on tilelink invariants

2016-01-17

Other

• fixing tilelink invariant

2016-01-16

Other

• fixing tilelink invariant
• wotking on tilelink invariant

2016-01-15

Other

• working on tilelink invariants

2016-01-14

Other

• fixing tilelink spec

2016-01-13

Other

• fixing tilelink spec

2016-01-12

Other

• adding tilelink_concrete_snoopy

2016-01-11

Other

• added logic option, worked on tilelink

2016-01-09

Other

• adding forgotten file
• fixing tilelink specs

2016-01-08

Other

• fixing tilelink specs

2016-01-07

Other

• decomposing failure actions

2016-01-06

Other

• fixing bugs in decompose

2016-01-05

Other

• line number improvements

2016-01-04

Other

• line number tracking fixes
• removed a print
• improved formatting of edge labels in ART
• adding view source
• adding file name tracking
• adding action decomposition

2016-01-03

Other

• fix to tilelink concrete spec
• concept graph color fix
• working on ui

2016-01-02

Other

• working on concrete tilelink

2016-01-01

Other

• working on tilelink_concrete_spec.ivy

2015-12-28

Other

• adding examples, notebooks
• adding ivy2 sources
• adding ivy sources
• adding license.txt
• adding .gitattributes
• Initial commit