1. 17 Sep, 2020 1 commit
  2. 15 Sep, 2020 1 commit
    • Raphaël Cauderlier's avatar
      Simplification of the formula produced by eval_precond · 5796046f
      Raphaël Cauderlier authored
      The following simplifications are applied:
      - eval_seq_precond immediately returns `False` on instruction sequences
      ending with a `FAILWITH` (it does so by looking at the tail-fail flag)
      - `match x with C1 y => phi y | C2 y => False` becomes
        `exists y, x = C1 y /\ phi y`
      - the code produced for `IF_ f` depends on the if-family `f` to avoid the previous double pattern matching: for example for options it produces `match o with | Some x -> ... | None -> ... end` instead of `match (match o with Some x -> inl x | None -> inr tt end) with inl x -> ... | inr y -> ... end`.
      
      Thanks to these simplifications, the proofs in the contract_coq
      directory are simpler.
      5796046f
  3. 29 Aug, 2020 1 commit
  4. 24 Aug, 2020 9 commits
  5. 17 Jul, 2020 1 commit
  6. 16 Jul, 2020 1 commit
  7. 07 Jul, 2020 4 commits
  8. 06 Jul, 2020 1 commit
  9. 22 Jun, 2020 2 commits
  10. 19 Jun, 2020 2 commits
  11. 19 May, 2020 2 commits
    • Raphaël Cauderlier's avatar
      [optimizer] Define and certify a Michelson optimizer · 2e8d5a3f
      Raphaël Cauderlier authored
      The optimizer was initially designed for the backend of the Albert
      compiler, it has been slightly generalized and certified. The main
      theorem is the last one in file typed_optimizer.v:
      
      If the untyped instruction sequence i can be typechecked from
      stack type A to stack type B and then run successfully on stack
      sA, then (optimizer.optimize i) can also be typechecked from
      stack type A to stack type B and run successfully on stack sA
      yielding the same result.
      2e8d5a3f
    • Raphaël Cauderlier's avatar
      Untyped macros in `instruction` · 11de7d7d
      Raphaël Cauderlier authored
      11de7d7d
  12. 14 May, 2020 7 commits
  13. 07 May, 2020 4 commits
  14. 18 Apr, 2020 4 commits