FV: Error reporting on db model before tx invalidated

[EnoF]

Is your enhancement request related to a problem? Please describe.

When you define a property specifying the state of a table before the transaction and the code does not satisfy this specification, the error reporting does not clarify the problem.

Describe the solution you'd like

Show the state of the asserted property before the transaction and what the assertion was inside of the report.

Additional context

(module test G
  (defcap G() true)

  (defschema foo-schema
    bar:string)

  (deftable foo:{foo-schema})

  (defun test(id:string value:string)
    @model [
      (property (= (at 'bar (read foo id 'before)) "hello"))
    ]
    ; (with-read foo id
    ;   { 'bar := bar }
    ;   (enforce (= bar "hello") "bar must be hello"))
    (update foo id 
      { 'bar : value })))

(verify 'test)

[rsoeldner]

@EnoF interesting case, I would even go further and argue that a table read with 'before should be forbidden. See the minimal example:

(module test G (defcap G() true)

  (defschema foo-schema bar:string)
  (deftable foo:{foo-schema})

  (defun test(id:string value:string)
    @model [(property (= (at 'bar (read foo id 'after)) "hello"))]
     1)
)
(verify 'test)

You have no option in talking about the initial value, except you specify an invariant but I suspect the use-cases are extremely rare.

The read using 'after on the other hand makes sense, i.e.:

(module test G (defcap G() true)

  (defschema foo-schema bar:string)
  (deftable foo:{foo-schema})

  (defun test(id:string value:string)
    @model [(property (= (at 'bar (read foo id 'after)) "hello"))]
     (update foo id
      { 'bar : "hello" }))
)

(verify 'test)

@jmcardon, @jwiegley any thoughts on this?

[EnoF]

Hey @rsoeldner I believe checking for a value before modification is not that uncommon if we consider a table to hold a state. For example a order status, where the column holds one of the following values: NEW, IN_PROGRESS, DELIVERED. FV could then enforce the state transition of NEW -> IN_PROGRESS and IN_PROGRESS -> DELIVERED.

What do you think?