Error of comparing sha256 hash value

[doslahtm]

Bug Report

When micse try to verify sha256 hash, Not Implemented Error is triggered

Scenario and Screenshot

• Target source code (Michelson code)

{ parameter
    (or (pair %commit (mutez %reward) (bytes %salted_hash))
        (pair %reveal
           (pair (address %chall_owner) (bytes %hashable))
           (lambda %message unit (list operation)))) ;
  storage
    (pair (big_map %commits address (pair (mutez %reward) (bytes %salted_hash)))
          (mutez %total_reward)) ;
  code { UNPAIR ;
         IF_LEFT
           { DUP 2 ;
             CAR ;
             SWAP ;
             SOME ;
             SENDER ;
             PAIR 3 ;
             SWAP ;
             CDR ;
             SWAP ;
             UNPAIR 3 ;
             UPDATE ;
             PAIR ;
             NIL operation ;
             PAIR }
           { DUP 2 ;
             CAR ;
             DUP 2 ;
             CAR ;
             CAR ;
             GET ;
             IF_NONE
               { PUSH string "You have not made a commitment to hash against yet." ;
                 FAILWITH }
               {} ;
             DUP 2 ;
             CAR ;
             CAR ;
             PACK ;
             DUP 3 ;
             CAR ;
             CDR ;
             CONCAT ;
             SHA256 ;
             DUP 2 ;
             CDR ;
             SWAP ;
             COMPARE ;
             NEQ ;
             IF { DROP 3 ;
                  PUSH string "This reveal does not match your commitment." ;
                  FAILWITH }
                { CAR ;
                  DUP 3 ;
                  CDR ;
                  ADD ;
                  DIG 2 ;
                  CAR ;
                  PAIR ;
                  UNIT ;
                  DIG 2 ;
                  CDR ;
                  SWAP ;
                  EXEC ;
                  PAIR } } } }

If MicSE try to analyze above code, then output is showed as below

[ERROR] [000023ms] Lib__Vc.VcError("Not Implemented : (MV_compare(MV_sha256(MV_concat_bbb(MV_cdr(MV_car(MV_unlift_right(MV_car(MV_symbol((MT_pair(MT_or(MT_pair MT_mutez MT_bytes)(MT_pair(MT_pair MT_address MT_bytes)(MT_lambda MT_unit(MT_list MT_operation))))(MT_pair(MT_big_map MT_address(MT_pair MT_mutez MT_bytes))MT_mutez))(MSC_mich_stack 0)))))))(MV_pack(MV_car(MV_car(MV_unlift_right(MV_car(MV_symbol((MT_pair(MT_or(MT_pair MT_mutez MT_bytes)(MT_pair(MT_pair MT_address MT_bytes)(MT_lambda MT_unit(MT_list MT_operation))))(MT_pair(MT_big_map MT_address(MT_pair MT_mutez MT_bytes))MT_mutez))(MSC_mich_stack 0))))))))))(MV_cdr(MV_unlift_option(MV_get_xbmo(MV_car(MV_car(MV_unlift_right(MV_car(MV_symbol((MT_pair(MT_or(MT_pair MT_mutez MT_bytes)(MT_pair(MT_pair MT_address MT_bytes)(MT_lambda MT_unit(MT_list MT_operation))))(MT_pair(MT_big_map MT_address(MT_pair MT_mutez MT_bytes))MT_mutez))(MSC_mich_stack 0)))))))(MV_car(MV_cdr(MV_symbol((MT_pair(MT_or(MT_pair MT_mutez MT_bytes)(MT_pair(MT_pair MT_address MT_bytes)(MT_lambda MT_unit(MT_list MT_operation))))(MT_pair(MT_big_map MT_address(MT_pair MT_mutez MT_bytes))MT_mutez))(MSC_mich_stack 0)))))))))")
Raised at file "MicSE/lib/vc.ml", line 543, characters 10-15
Called from file "MicSE/lib/vc.ml" (inlined), line 83, characters 20-42
Called from file "MicSE/lib/vc.ml", line 314, characters 54-64
Called from file "MicSE/lib/vc.ml", line 536, characters 9-37
Called from file "MicSE/lib/vc.ml" (inlined), line 726, characters 32-61
Called from file "MicSE/lib/vc.ml", line 759, characters 53-61
Called from file "MicSE/lib/vc.ml" (inlined), line 727, characters 20-34
Called from file "MicSE/lib/vc.ml", line 734, characters 45-53
Called from file "src/list.ml", line 409, characters 13-17
Called from file "src/list.ml" (inlined), line 418, characters 15-31
Called from file "MicSE/lib/vc.ml", line 735, characters 46-67
Called from file "MicSE/lib/vc.ml", line 1230, characters 28-48
Called from file "MicSE/lib/vc.ml", line 1326, characters 6-58
Called from file "src/list.ml", line 241, characters 19-22
Called from file "src/list.ml" (inlined), line 246, characters 22-39
Called from file "MicSE/lib/mState.ml", line 767, characters 45-73
Called from file "src/map.ml", line 815, characters 30-33
Called from file "src/map.ml", line 1700, characters 36-57
Called from file "MicSE/lib/mState.ml", line 767, characters 5-73
Called from file "MicSE/lib/res.ml", line 312, characters 6-128
Called from file "lib/execFlow_s.ml", line 23, characters 6-64
Called from file "cmd/main.ml", line 8, characters 22-62

Plan

• Edit lib/vc.ml

diff --git a/lib/vc.ml b/lib/vc.ml
index dbf7f1a..fda0087 100644
--- a/lib/vc.ml
+++ b/lib/vc.ml
@@ -659,7 +659,8 @@ module Encoder = struct
        Formula.if_then_else ctx
          ~if_:(Formula.create_neq ctx cmp_fst zero)
          ~then_:cmp_fst ~else_:cmp_snd
-     | (MT_bytes, MT_bytes) -> raise Not_Implemented
+     (*| (MT_bytes, MT_bytes) -> raise Not_Implemented*)
+     | (MT_bytes, MT_bytes) -> dummy
      | (MT_signature, MT_signature) ->
        Formula.if_then_else ctx
          ~if_:(Formula.create_is_signature_str expr1)

Reference

• ...