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

Defproperty #135

Closed
wants to merge 5 commits into
base: master
from

Conversation

Projects
None yet
3 participants
@joelburget
Copy link
Contributor

joelburget commented Jun 21, 2018

No description provided.

Generalize prenex normalization.
Previously only applicable to bool, now applicable to any ground type or
object.

@joelburget joelburget requested review from bts and slpopejoy Jun 21, 2018

@joelburget

This comment has been minimized.

Copy link
Contributor Author

joelburget commented Jun 21, 2018

fixes #123

(defproperty auth-required
(when
(not (authorized-by 'accounts-admin-keyset))
abort)))

This comment has been minimized.

@bts

bts Jun 21, 2018

Contributor

I think this should be just be:

(defproperty auth-required
  (authorized-by 'accounts-admin-keyset))

This comment has been minimized.

@joelburget

joelburget Jun 22, 2018

Author Contributor

true

@joelburget joelburget force-pushed the defproperty branch from 8f39c18 to 81cde1b Jun 22, 2018

@joelburget joelburget force-pushed the defproperty branch from 81cde1b to 59e981c Jun 22, 2018

TTable {} -> return d
TUse {} -> return d
TBless {} -> return d
TDefProperty {} -> return d

This comment has been minimized.

@slpopejoy

slpopejoy Jun 23, 2018

Contributor

So, the first thing to note here is this has moved out of meta. Why?

This comment has been minimized.

@joelburget

joelburget Jun 23, 2018

Author Contributor

Perhaps you could give an example of where / how properties would be defined.

This comment has been minimized.

@slpopejoy

slpopejoy Jun 23, 2018

Contributor

It's more that it begs the question, why are properties in meta at all.

A reason why is to indicate clearly what is code and what is model checking. Properties are tightly integrated with code, more than unit tests, but the reason for a clear distinction is to make it obvious that the properties are not loaded on the blockchain, much like doctests might be if we were to add support for them in meta.

Also, it fits our architectural model thus far: model checking doesn't bleed out of Pact/Analyze -- we could CPP out model checking entirely from blockchain builds.

I will give some thought to a design, but I first wanted to defend the whole reason why we're in meta in the first place. defproperty as a Term radically changes that, so I would argue that a change this momentous needs its own justification.

As a final note, I would still like to keep the idea of a foo.property file as a way to share property abstractions, but also to potentially move proofs out of blockchain code if desired. One thing I do think is strange is useing a module to get only its properties -- you're putting that dep now on the blockchain, which if it's just for proofs is not very valuable.

This comment has been minimized.

@slpopejoy

slpopejoy Jun 23, 2018

Contributor

A simple design is just def or defs leading off a block, similarly to properties now. For importing properties from a file you could have import, or from another module, use.

(module foo 'ks
  (meta "foo docstring"
    (use bar "optional-hashvalue")
    (import "shared/stuff.properties")
    (defs [
      (def conserves-mass
        "Ensure a BALANCE column in ACCOUNTS table is net zero"
        (= (column-delta 'accounts 'balance) 0.0))
      (def auth-required
        "Always governed by accounts-admin-keyset"
        (authorized-by 'accounts-admin-keyset))
    ])
    ...
)

I'm trying out defs + def but it could also just be (conserves-mass (= ...))

Looking at that, it seems to me some level of argument/macro specification could be cool, ie:

 (def conserves-mass (balance-col accounts-table)
        "Ensure a BALANCE-COL in ACCOUNTS-TABLE is net zero"
        (= (column-delta accounts-table balance-col) 0.0)) 

This comment has been minimized.

@bts

bts Jun 23, 2018

Contributor

Yeah Joel talks about property args here: #123 (comment)

This comment has been minimized.

@joelburget

joelburget Jun 24, 2018

Author Contributor

One thing I do think is strange is useing a module to get only its properties -- you're putting that dep now on the blockchain, which if it's just for proofs is not very valuable.

This makes sense to me. My first thought is to add syntax like use properties (rather than import to specify you're only importing properties). However, either way, you're mentioning a file which is not put on the blockchain, so it's basically creating a dead link. Can we avoid this?

I think defining properties within a meta would work. My only concerns are

  1. does it feel cumbersome to use?
  2. is it intuitive that the defined property is visible from the entire module / when the module is imported?
  3. do we have to replicate a lot of the same machinery that already exists, but for the meta level?

@joelburget joelburget closed this Aug 3, 2018

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