search

tchajed / coq-record-update

Library to create Coq record update functions
MIT License
42 stars 16 forks source link

It is easy to accidentally pass getters incorrectly #5

Closed joonazan closed 5 years ago

joonazan commented 5 years ago 
Definition register := RF_t -> int48.
Definition set_register (r : register) {_ : Setter r} v RF :=
  set r (constructor v) RF.

If I leave out {_ : Setter r} in the above code, it compiles but the function doesn't change the record.

This is what I did before finding this library:

Definition set_register (r : register) (v : int48) (RF : RF_t) : RF_t :=
  r _ (mkRF _
    (mkRF _ v (ra1 _ RF) (ra2 _ RF) (ra3 _ RF) (ra4 _ RF) (ra5 _ RF) (ra6 _ RF) (ra7 _ RF))
    (mkRF _ (ra0 _ RF) v (ra2 _ RF) (ra3 _ RF) (ra4 _ RF) (ra5 _ RF) (ra6 _ RF) (ra7 _ RF))
    (mkRF _ (ra0 _ RF) (ra1 _ RF) v (ra3 _ RF) (ra4 _ RF) (ra5 _ RF) (ra6 _ RF) (ra7 _ RF))
    (mkRF _ (ra0 _ RF) (ra1 _ RF) (ra2 _ RF) v (ra4 _ RF) (ra5 _ RF) (ra6 _ RF) (ra7 _ RF))
    (mkRF _ (ra0 _ RF) (ra1 _ RF) (ra2 _ RF) (ra3 _ RF) v (ra5 _ RF) (ra6 _ RF) (ra7 _ RF))
    (mkRF _ (ra0 _ RF) (ra1 _ RF) (ra2 _ RF) (ra3 _ RF) (ra4 _ RF) v (ra6 _ RF) (ra7 _ RF))
    (mkRF _ (ra0 _ RF) (ra1 _ RF) (ra2 _ RF) (ra3 _ RF) (ra4 _ RF) (ra5 _ RF) v (ra7 _ RF))
    (mkRF _ (ra0 _ RF) (ra1 _ RF) (ra2 _ RF) (ra3 _ RF) (ra4 _ RF) (ra5 _ RF) (ra6 _ RF) v)).
tchajed commented 5 years ago

Thanks for reporting!

Took me a while to think of what was going wrong - I substitute the projection for the updater in etaX but never check that the projection actually appears in etaX. If it didn't appear then you would get the behavior above where nothing happens. There's now an explicit check.

This shouldn't have happened with set_wf, which builds a correctness proof that wouldn't have succeeded, but it's still a bug.