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 (Symbolic tests #46, Closes #50 : Use tezos mock client and cleanup #52)
• two documentation/cleanup PRs landed (Mass reformat of all markdown **text** #54, Reorganize documentation and simplify compat modules #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 (Extract #MichelineToNative function to MICHELSON-COMMON #70)
• refactoring semantics initialization (Simplify semantics initialization #61)
• merging of concrete and symbolic unit semantics (Merge unit test and symbolic #71)
• documentation overhaul of README and two source files (Improve documentation #74, michelson/configuration.md: Fix indentation #76)

Week 2

• refactor internal StackElementList structure to use K's parameterized lists, simplify Aborted semantics (Refactorings #85)
• add initial implementation of loop invariant checking (Invariants #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 (Improve symbolic test result printer #88)
• optimized version of loop invariants + theoretical justification of correctness (Justify/Cleanup loop invariants #89)

Week 2

• merged in upstreamed Set union operator (Update dependency: ext/k (fix |Set) #91)
• started work on symbolic data structure usage (Option and pair type matching #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 (Move token sorts to external syntax modules #98)
• Fix unused symbol/variable warnings (Fix unused symbol/variable warnings #99)
• Tests for binding symbolic structures (Tests for binding symbolic structures #100)
• Makefresh fixes and test check corner cases (Makefresh fixes and test check corner cases #101)
• Miscellaneous documentation/code cleanup (Miscellaneous documentation/code cleanup #102)
• #MakeFresh Redesign (#MakeFresh Redesign #103)
• Improve symbolic match and comparison (Improve symbolic match and comparison #106)
• Cleanup directory/module structure (Cleanup dir structure #109)
• Symbolic PUSH and Maps (Symbolic PUSH and Maps #111)

TODO

• fix issues with symbolic maps
• add symbolic lambda support (in progress Symbolic Lambdas #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 (Enable symbolic LOOP_LEFT and add tests #115)
• Add runtime type checking via typed stack (Add runtime type checking via typed stack #117)
• Makefile: fix LLVM backend build on OSX/brew (Makefile: fix LLVM backend build on OSX/brew #119)
• Reimplement GET for maps operationally (Reimplement GET for maps operationally #120)
• Improve ./kmich test runner (Improve ./kmich test runner #122)

Week 2

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

Week 3

Code Contributions:

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

Exploratory Research:

• Investigated Michelson key, key_hash, and address literal encoding + wrote up notes (Parser Cleanup Meta-Issue #48 (comment))
• 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 (Design format for ITER and MAP invariants #84 (comment))

TODO

• Add generic multisig contract (Add generic multisig contract test #128) --- depends on Design format for ITER and MAP invariants #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 (kmich: tighten argument validation/fix usage message #135)
• blockchain-k-plugin: upstream and unify hook code, a necessary step towards Michelson integration (Upstream kevm hooks v2 evm-semantics#917, Upstream KEVM hook code blockchain-k-plugin#115)

Week 2

• remove some legacy code and simplify symbolic value initialization (Simplify stack initialization/symbolic value processing #138)
• enable macro evaluation for most macros (Enable Macro Evaluation #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 (Add symbolic semantics for IF_NONE and vote tests #142)

Week 2

• give demo about Michelson language work
• remove some C hooks/cleanup the parser (Cleanup parser/remove C hooks #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 (Reimplement Michelson lists using InternalList #144)

In Progress

• Re-enable kprove tests (Re-enable kprove tests #146)
• Update common.md documentation (Update common.md documentation #147)
• Various updates to the unit tests (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 (Re-enable kprove tests #146)
• Update common.md documentation (Update common.md documentation #147)
• Update unit tests to be consistent with upstream (Update unit tests to be consistent with upstream #148 subsumes Various updates to the unit tests #37)
• kmich: fix --version command (kmich: fix --version command #150)

Week 2

N/A

In Progress

• Better normalize abstract terms for symbolic reasoning (Better normalize abstract terms for symbolic reasoning #153)
• Update count tests and add times two test (Update count tests and add times two test #154)
• Add user guide (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 (Better normalize abstract terms for symbolic reasoning #153)
• Update count tests and add times two test (Update count tests and add times two test #154)
• Add user guide (Add user guide #155)

Week 2

N/A

In Progress

• Add backend infrastructure to support quantification (Move to Meta-K based driver, fix issues with stuck configurations #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