search

input-output-hk / ouroboros-high-assurance

High-assurance implementation of the Ouroboros protocol family
Apache License 2.0
1 stars 1 forks source link

Make `state_machine_bisimulation` use `Let_def` more often #91

Closed jeltsch closed 1 year ago

jeltsch commented 1 year ago

Currently, the fastforce run of state_machine_bisimulation uses the default handling of let expressions, which, according to our understanding, invokes Let_def as a simplification rule only when the variable bound by let is used at most once. This makes state_machine_bisimulation too weak to handle certain programs. Concretely, we encountered this issue when resolving #81.

According to our understanding, adding Let_def as a simplification rule may cause the prover to run very long, because terms may grow drastically in size by let expansion, but it may not prevent termination of the prover. Since the terms that are bound to variables by let within programs should typically be fairly small, we consider adding Let_def as a simplification rule viable and consequently call for doing this.

jeltsch commented 1 year ago

More information concerning this issue can be found in the mailing list post at https://mailman46.in.tum.de/pipermail/isabelle-dev/2011-August/010146.html.