Skip to main content

Browse the archive

Revision 9e85ab18f02ff773df83e7bf925a8d15949e6f6b authored by Benjamin Gregoire on 06 December 2023, 17:00:18 UTC, committed by Pierre-Yves Strub on 07 December 2023, 10:21:48 UTC 
Add tactic `weakmem`
 
This tactic allows to weaken the memory of a phoare hypothesis
by adding new variables to it.

This tactic is needed in the while rule for phoare, when one
wants to apply the induction hypothesis & the memories are
not compatible. Currently, the convertibility check does not
enforce that memories are equal, but a to-come PR is going to
fix that point.
1 parent d248e73
Raw File
dune 
(dirs src theories examples scripts)

(install
  (section (site (easycrypt commands)))
  (files (scripts/testing/runtest as runtest)))

(install
  (section (bin))
  (files (scripts/testing/bin-ec-runtest as ec-runtest)))
back to top