search

input-output-hk / marlowe

Prototype implementation of domain-specific language for the design of smart-contracts over cryptocurrencies
Apache License 2.0
172 stars 43 forks source link

SCP-4869 - Add lemma and test around rounding to zero #164

Closed hrajchert closed 1 year ago

hrajchert commented 1 year ago

This PR adds a lemma that proves that if the numerator is lower than the denominator (in absolute), then DivValue rounds to 0.