We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 330c546 commit c3c25b6Copy full SHA for c3c25b6
examples/MEE-CBC/RCPA_CMA.ec
@@ -336,7 +336,7 @@ theory EtM.
336
type leaks <- leaks,
337
op leak <- leak,
338
op dC (l:leaks) <- (dC l) `*` (MUnit.dunit witness<:tag>)
339
- proof * by smt.
+ proof * by smt(dC_ll dprod_ll dunit_ll).
340
341
(** The black-box construction is as follows **)
342
module EtM(E:SKEa.Enc_Scheme, M:MACa.MAC_Scheme): Enc_Scheme = {
0 commit comments