From ee92d49837ab8d92c7dd6b3a90a2fcd81c335546 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Wed, 28 Apr 2021 15:57:24 -0700 Subject: [PATCH] cryptol-saw-core: Fix tuple encoding used by `proveEq`. Fixes #1166. --- cryptol-saw-core/src/Verifier/SAW/Cryptol.hs | 37 ++++++++++++-------- 1 file changed, 22 insertions(+), 15 deletions(-) diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs index 2e293779c3..3814999b86 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs +++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs @@ -1408,27 +1408,34 @@ proveEq sc env t1 t2 aEq <- proveEq sc env a1 a2 bEq <- proveEq sc env b1 b2 scGlobalApply sc "Cryptol.fun_cong" [a1', a2', b1', b2', aEq, bEq] - (C.tIsTuple -> Just (a1 : ts1), C.tIsTuple -> Just (a2 : ts2)) - | length ts1 == length ts2 -> - do let b1 = C.tTuple ts1 - b2 = C.tTuple ts2 - a1' <- importType sc env a1 - a2' <- importType sc env a2 - b1' <- importType sc env b1 - b2' <- importType sc env b2 - aEq <- proveEq sc env a1 a2 - bEq <- proveEq sc env b1 b2 - if b1 == b2 - then scGlobalApply sc "Cryptol.pair_cong1" [a1', a2', b1', aEq] - else if a1 == a2 - then scGlobalApply sc "Cryptol.pair_cong2" [a1', b1', b2', bEq] - else scGlobalApply sc "Cryptol.pair_cong" [a1', a2', b1', b2', aEq, bEq] + (tIsPair -> Just (a1, b1), tIsPair -> Just (a2, b2)) -> + do a1' <- importType sc env a1 + a2' <- importType sc env a2 + b1' <- importType sc env b1 + b2' <- importType sc env b2 + aEq <- proveEq sc env a1 a2 + bEq <- proveEq sc env b1 b2 + if b1 == b2 + then scGlobalApply sc "Cryptol.pair_cong1" [a1', a2', b1', aEq] + else if a1 == a2 + then scGlobalApply sc "Cryptol.pair_cong2" [a1', b1', b2', bEq] + else scGlobalApply sc "Cryptol.pair_cong" [a1', a2', b1', b2', aEq, bEq] (C.tIsRec -> Just tm1, C.tIsRec -> Just tm2) | map fst (C.canonicalFields tm1) == map fst (C.canonicalFields tm2) -> proveEq sc env (C.tTuple (map snd (C.canonicalFields tm1))) (C.tTuple (map snd (C.canonicalFields tm2))) (_, _) -> panic "proveEq" ["Internal type error:", pretty t1, pretty t2] +-- | Deconstruct a cryptol tuple type as a pair according to the +-- saw-core tuple type encoding. +tIsPair :: C.Type -> Maybe (C.Type, C.Type) +tIsPair t = + do ts <- C.tIsTuple t + case ts of + [] -> Nothing + [t1, t2] -> Just (t1, t2) + t1 : ts' -> Just (t1, C.tTuple ts') + -------------------------------------------------------------------------------- -- List comprehensions