runtimeverification / avm-semantics

BSD 3-Clause "New" or "Revised" License
15 stars 4 forks source link

Ensure that pushing an inner transaction won't duplicate `<txID>` #269

Closed geo2a closed 1 year ago

geo2a commented 1 year ago

When executing inner transactions, we must ensure that we don't concatenate transactions with duplicate IDs with the existing <transactions> cell, since this is unsound and will turn LHS to #Bottom. We should make the semantics get stuck instead, which this change ensures.