Meeting Notes

[sskeirik]

Append one comment to this issue for each meeting.

[sskeirik]

Wednesday, June 24th

Also includes notes from Wednesday, June 10th since we hadn't started this list yet.

PROGRESS

• two testing PRs landed (#46, #52)
• two documentation/cleanup PRs landed (#54, #59)

TODO

• investigate Michelson fork/formalization refx (https://gitlab.com/akawashiro/tezos/-/blob/refx/refinement-subcommand.md)
  • especially, their notation for loop invariants
• investigate Michelson formalization Mi-Cho-Coq (https://gitlab.com/nomadic-labs/mi-cho-coq)
  • especially, support for .tzt files (https://gitlab.com/nomadic-labs/mi-cho-coq/-/merge_requests/67)
• consider shared announcement of collaboration

NOTES

• considering update to format to include initial operation nonce value
• big_map diffs are always applied on contract end

[sskeirik]

Wednesday, July 8th

PROGRESS

Week 1

• refactoring mega-function #MichelineToNative (#70)
• refactoring semantics initialization (#61)
• merging of concrete and symbolic unit semantics (#71)
• documentation overhaul of README and two source files (#74, #76)

Week 2

• refactor internal StackElementList structure to use K's parameterized lists, simplify Aborted semantics (#85)
• add initial implementation of loop invariant checking (#79)

TODO

NOTES

• (a) need clarity on supporting symbolic collection type variables: preferences on syntax, desired features
• (b) should discuss loop invariant syntax
  1. need at least a way to refer to stack items and;
  2. a way to constrain stack items
  3. for some invariants, we may need syntax to refer to program inaccessible state, i.e. operation nonces, bigmap indices, etc...

External Updates:

• reference client now passes all of unit tests, but there are some caveats:
  • operation literals are now represented by reusing the operation type primitive
  • need normalization pass on the output stack to choose between the human readable and optimized notation --- currently human readable output is chosen
  • goal: all .tzt clients should pass the same tests (see https://gitlab.com/nomadic-labs/tezos/-/tree/rafoo@unit_test/tests_python/contracts/unit)
• (a) can start by supporting collection variables in a fully symbolic way and then add support for partially symbolic literals if needed
• (b) syntax seems OK for now; we can overhaul on as needed basis

[sskeirik]

Friday, July 17th

PROGRESS

Week 1

• improvements to the test result summary/test debugger (#88)
• optimized version of loop invariants + theoretical justification of correctness (#89)

Week 2

• merged in upstreamed Set union operator (#91)
• started work on symbolic data structure usage (#90)

TODO

• investigate whylson (https://gitlab.com/releaselab/fresco/whylson) and refx and compare how to use, performance, etc...
• investigate how to improve performance
• investigate how to get more information out of the backend

NOTES

• decided to tackle partially symbolic data structures at a later date, because it requires restructuring our typing semantics

[sskeirik]

Thursday, August 20th

PROGRESS

• Move token sorts to external syntax modules (#98)
• Fix unused symbol/variable warnings (#99)
• Tests for binding symbolic structures (#100)
• Makefresh fixes and test check corner cases (#101)
• Miscellaneous documentation/code cleanup (#102)

• MakeFresh Redesign (#103)

• Improve symbolic match and comparison (#106)
• Cleanup directory/module structure (#109)
• Symbolic PUSH and Maps (#111)

TODO

• fix issues with symbolic maps
• add symbolic lambda support (in progress #113)
• fix vote and multisig contracts

NOTES

• Consider tests of the form:

input { Stack_elt int $x ; Stack_elt int $y };
precondition { PUSH int $x; PUSH int $y; ASSERT_CMPEQ };
code { SWAP };
output { Stack_elt int $z; Stack_elt int $z }

[sskeirik]

Thursday, September 10th

PROGRESS

Week 1

• Enable symbolic LOOP_LEFT and add tests (#115)
• Add runtime type checking via typed stack (#117)
• Makefile: fix LLVM backend build on OSX/brew (#119)
• Reimplement GET for maps operationally (#120)
• Improve ./kmich test runner (#122)

Week 2

• Improve symbolic maps symbolic reasoning performance + other small fixes (#123)
• Add support for symbolic lambdas (#124)
• Simplify symbolic test lookup and add vote contract tests (#125)
• Documentation Update (#127)

Week 3

Code Contributions:

• Refactor Michelson syntax definition (#130)
• Michelson type checking documentation + fixes (#131)

Exploratory Research:

• Investigated Michelson key, key_hash, and address literal encoding + wrote up notes (https://github.com/runtimeverification/michelson-semantics/issues/48#issuecomment-687335269)
• Investigated Michelson parsing pipeline + wrote up notes (https://github.com/runtimeverification/michelson-semantics/blob/micheline/parser-info.md)
• Investigated approaches to writing ITER invariants needed for multisig contract (https://github.com/runtimeverification/michelson-semantics/issues/84#issuecomment-687329516)

TODO

• Add generic multisig contract (#128) --- depends on #84
• Fix bug with matcher + symbolic lambda evaluation

NOTES

• Previous protocol amendment proposal was delayed (https://forum.tezosagora.org/t/state-of-the-languages/1559/7)
• Actual protocol amendment proposal changes are here (https://blog.nomadic-labs.com/delphi-changelog.html) with the high-level announcement here (https://blog.nomadic-labs.com/delphi-official-release.html) --- these changes were motivated by problems with people being unable to write interesting contracts because the gas costs were too high
  • Gas model changes/simplifications
  • Explicit stack and recursion limits as well as limits on DIP, DIG, and DUG
• Annotation mechanism is often not used because annotations add to on-chain storage cost --- do not worry about investing too much time into this

[sskeirik]

Thursday, September 24th

PROGRESS

Week 1

• kmich: tighten argument validation/fix usage message (#135)
• blockchain-k-plugin: upstream and unify hook code, a necessary step towards Michelson integration (kframework/evm-semantics#917, runtimeverification/blockchain-k-plugin#115)

Week 2

• remove some legacy code and simplify symbolic value initialization (#138)
• enable macro evaluation for most macros (#136)
• started standalone proof of multisig contract to gain insight into needed invariant structure

TODO

• enable vote contract (pending minor tweak to backend)
• continuing work on generic multisig contract
• fix bug with matcher + symbolic lambda evaluation

NOTES

• PAIR/UNPAIR macros may be de-emphasized in a future version

[sskeirik]

Thursday, October 22nd

PROGRESS

Week 1

• write PR that enables partial vote contract to complete (#142)

Week 2

• give demo about Michelson language work
• remove some C hooks/cleanup the parser (#141)

TODO

• continuing work on generic multisig contract
• fix bug with matcher + symbolic lambda evaluation

NOTES

• try to hand-prove another simple contract listed in the slack channel (e.g. min of a list)
• try to prove contracts in the reverse order
• testing contracts:
  • using a higher-level language like LIGO which includes builtin unit test support
  • originate all of the contracts on the test network and use a block explorer
• ticket feature history:
  • https://forum.tezosagora.org/t/contract-signatures/1458
  • https://gitlab.com/metastatedev/tezos/-/merge_requests/136
  • https://gitlab.com/metastatedev/tezos/-/merge_requests/328

[sskeirik]

Thursday, November 5th

PROGRESS

Week 1

kmich: add --repl option for kprove with aliases (#143)

Week 2

• Reimplement Michelson lists using InternalList (#144)

In Progress

• Re-enable kprove tests (#146)
• Update common.md documentation (#147)
• Various updates to the unit tests (#37)

TODO

• continuing work on generic multisig contract (blocked on backend issue)
• fix bug with matcher + symbolic lambda evaluation

NOTES

[sskeirik]

Thursday, November 19th

PROGRESS

Week 1

• Re-enable kprove tests (#146)
• Update common.md documentation (#147)
• Update unit tests to be consistent with upstream (#148 subsumes #37)
• kmich: fix --version command (#150)

Week 2

N/A

In Progress

• Better normalize abstract terms for symbolic reasoning (#153)
• Update count tests and add times two test (#154)
• Add user guide (#155)

TODO

• continuing work on generic multisig contract; finally unblocked!
• fix bug with matcher + symbolic lambda evaluation

NOTES

• consider using macros which have special meaning in the backend
  • forall/exists can probably be written as a macro which types correctly using pairs/lambdas
  • list indexing can be written as a macro
• there is a new scenario testing format being developed. links here:
  • https://gitlab.com/metastatedev/tezos/-/merge_requests/320
  • https://gitlab.com/metastatedev/tezos/-/merge_requests/320/diffs#baf5ae9731b9394007fd74e845e331ddbffc1564_0_94

[sskeirik]

Thursday, December 4th

PROGRESS

Week 1

• Better normalize abstract terms for symbolic reasoning (#153)
• Update count tests and add times two test (#154)
• Add user guide (#155)

Week 2

N/A

In Progress

• Add backend infrastructure to support quantification (#156)
• Add macros representing quantification (pending PR)
• Experimentation with quantification on list min program

TODO

• continuing work on unblocked generic multisig contract!
• fix bug with matcher + symbolic lambda evaluation

NOTES