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.

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

Improve UX for falsified properties #132

bts opened this Issue Jun 21, 2018 · 0 comments


None yet
2 participants
Copy link

bts commented Jun 21, 2018

/cc @slpopejoy @joelburget

We're currently working towards an improved UX in the face of falsified properties. Our current model reports on master are difficult for users unfamiliar with the system to debug/understand.

  • The requisite foundational work for this has already been completed (on analyze).
  • We are "tagging" args, the result, intermediate variables/values, reads, writes, & auths in a new datatype called Model. This is complete (on analyze).
  • Make "auths" in Model smarter
    • use keyset names when possible (for global keysets)
    • use table/row key when possible (for row-level keysets)
    • use arg name when possible (for user inputs)
    • integrate metadata into Model
    • investigate potential upstream schema issue for objects (this should remove some rogue keysets from reporting)
    • disallow partial inserts/writes in analysis (depends on schema issue)
    • improve reporting around "numbered" keysets
  • We will tag edges on an execution graph, to track the evaluation flow of code for a falsified model. e.g. which way does the code go when we hit a conditional?
  • We will use this graph information to linearize an execution trace of variable bindings and effects, to report back to the user. This is necessary because our Model is "overfitted" in that it pretends that every single read, write, authorization and variable binding occurs, even for code outside the single execution path. This is too much noise for an end user, and confusing to use without being further distilled.

@bts bts self-assigned this Jun 21, 2018

@slpopejoy slpopejoy added the FV label Jul 17, 2018

@bts bts closed this Nov 1, 2018

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment