proving redundancy of "plain" writes

[opqrs]

Low priority:
Conjecture: it is possible to remove "plain" writes, keeping only promises and fulfilment.

Corollary: in "batch" mode, it is possible to enumerate fewer things.

[jeehoonkang]

If I understand correctly, we have four models:

• axiomatic: the golden standard
• global consistency: simplist model
• local consistency w/o writes: for exhaustive enumeration of possible behaviors
• local consistency: for interactive exploration of possible behaviors

[opqrs]

In fact, I'm not sure we need "plain" writes as first-class citizens: we can define them as a macro for promising and immediately fulfilling.
@cp526 ?

[jeehoonkang]

@opqrs I agree with you.

[jeehoonkang]

@gilhur and I discussed on this issue, and we also prefer to remove plain writes. I tentatively removed it in the development: 815bff0

[opqrs]

It means that we will have to allow promises in certification.
Example by Jeehoon: promising W y 1 based on the 'else' branch, and certifying using the 'then' branch:

if ...
  x = 1
  y = 1
else
  y = 1