search

freespek / ssf-mc

EF project Exploring Automatic Model-Checking of the Ethereum specification
Apache License 2.0
3 stars 0 forks source link

One-to-many recursion translation rule + latexification #23

Open Kukovec opened 1 month ago

Kukovec commented 1 month ago

Adds a special translation rule, for the case where a recursive operator computes multiple values recursively (instead of a single recursive call).

closes #22

konnov commented 1 month ago

@Kukovec is it still in the draft stage?

Kukovec commented 1 month ago

Technically, the rule itself is complete, what's missing is https://github.com/freespek/ssf-mc/blob/e64112b08780409153e2644609b6123e3ac2e03a/Translation.md?plain=1#L558

Kukovec commented 2 weeks ago

Note that this makes Translation.md deprecated, do we want to just delete it as part of this pr?

konnov commented 2 weeks ago

Note that this makes Translation.md deprecated, do we want to just delete it as part of this pr?

Yes, if it's not needed anymore, let's remove it

thpani commented 2 weeks ago

Could you please change those commit messages to something meaningful?

konnov commented 1 week ago

I've read the report.tex (compiled with pdflatex). The translation makes sense to me, though I've not read the proofs carefully yet. Perhaps, @banhday could give us an opinion here?

banhday commented 1 week ago

@konnov : I will try to have a look at it by this Wednesday.

banhday commented 1 week ago

@Kukovec : I have added a few questions in the *.tex files.