-
Notifications
You must be signed in to change notification settings - Fork 63
/
Cryptol.hs
1862 lines (1658 loc) · 81.6 KB
/
Cryptol.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE DoAndIfThenElse #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE BangPatterns #-}
{- |
Module : Verifier.SAW.Cryptol
Copyright : Galois, Inc. 2012-2015
License : BSD3
Maintainer : huffman@galois.com
Stability : experimental
Portability : non-portable (language extensions)
-}
module Verifier.SAW.Cryptol where
import Control.Monad (foldM, join, unless)
import Control.Exception (catch, SomeException)
import Data.Bifunctor (first)
import qualified Data.Foldable as Fold
import Data.List
import Data.List.NonEmpty (NonEmpty(..))
import Data.Maybe (fromMaybe)
import qualified Data.IntTrie as IntTrie
import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Text (Text)
import qualified Data.Text as Text
import qualified Data.Vector as Vector
import Prelude ()
import Prelude.Compat
import Text.URI
import qualified Cryptol.Eval.Type as TV
import qualified Cryptol.Backend.Monad as V
import qualified Cryptol.Backend.SeqMap as V
import qualified Cryptol.Backend.WordValue as V
import qualified Cryptol.Eval.Value as V
import qualified Cryptol.Eval.Concrete as V
import Cryptol.Eval.Type (evalValType)
import qualified Cryptol.TypeCheck.AST as C
import qualified Cryptol.TypeCheck.Subst as C (Subst, apSubst, listSubst, singleTParamSubst)
import qualified Cryptol.ModuleSystem.Name as C
(asPrim, asParamName, nameUnique, nameIdent, nameInfo, NameInfo(..))
import qualified Cryptol.Utils.Ident as C
( Ident, PrimIdent(..), mkIdent
, prelPrim, floatPrim, arrayPrim, suiteBPrim, primeECPrim
, ModName, modNameToText, identText, interactiveName
, ModPath(..), modPathSplit
)
import qualified Cryptol.Utils.RecordMap as C
import Cryptol.TypeCheck.Type as C (Newtype(..))
import Cryptol.TypeCheck.TypeOf (fastTypeOf, fastSchemaOf)
import Cryptol.Utils.PP (pretty)
import Verifier.SAW.Cryptol.Panic
import Verifier.SAW.FiniteValue (FirstOrderType(..), FirstOrderValue(..))
import qualified Verifier.SAW.Simulator.Concrete as SC
import qualified Verifier.SAW.Simulator.Value as SC
import Verifier.SAW.Prim (BitVector(..))
import Verifier.SAW.SharedTerm
import Verifier.SAW.Simulator.MonadLazy (force)
import Verifier.SAW.TypedAST (mkSort, FieldName, LocalName)
import GHC.Stack
--------------------------------------------------------------------------------
-- Type Environments
-- | SharedTerms are paired with a deferred shift amount for loose variables
data Env = Env
{ envT :: Map Int (Term, Int) -- ^ Type variables are referenced by unique id
, envE :: Map C.Name (Term, Int) -- ^ Term variables are referenced by name
, envP :: Map C.Prop (Term, [FieldName], Int)
-- ^ Bound propositions are referenced implicitly by their types
-- The actual class dictionary we need is obtained by applying the
-- given field selectors (in reverse order!) to the term.
, envC :: Map C.Name C.Schema -- ^ Cryptol type environment
, envS :: [Term] -- ^ SAW-Core bound variable environment (for type checking)
, envRefPrims :: Map C.PrimIdent C.Expr
, envPrims :: Map C.PrimIdent Term -- ^ Translations for other primitives
, envPrimTypes :: Map C.PrimIdent Term -- ^ Translations for primitive types
}
emptyEnv :: Env
emptyEnv =
Env Map.empty Map.empty Map.empty Map.empty [] Map.empty Map.empty Map.empty
liftTerm :: (Term, Int) -> (Term, Int)
liftTerm (t, j) = (t, j + 1)
liftProp :: (Term, [FieldName], Int) -> (Term, [FieldName], Int)
liftProp (t, fns, j) = (t, fns, j + 1)
-- | Increment dangling bound variables of all types in environment.
liftEnv :: Env -> Env
liftEnv env =
Env { envT = fmap liftTerm (envT env)
, envE = fmap liftTerm (envE env)
, envP = fmap liftProp (envP env)
, envC = envC env
, envS = envS env
, envRefPrims = envRefPrims env
, envPrims = envPrims env
, envPrimTypes = envPrimTypes env
}
bindTParam :: SharedContext -> C.TParam -> Env -> IO Env
bindTParam sc tp env = do
let env' = liftEnv env
v <- scLocalVar sc 0
k <- importKind sc (C.tpKind tp)
return $ env' { envT = Map.insert (C.tpUnique tp) (v, 0) (envT env')
, envS = k : envS env }
bindName :: SharedContext -> C.Name -> C.Schema -> Env -> IO Env
bindName sc name schema env = do
let env' = liftEnv env
v <- scLocalVar sc 0
t <- importSchema sc env schema
return $ env' { envE = Map.insert name (v, 0) (envE env')
, envC = Map.insert name schema (envC env')
, envS = t : envS env' }
bindProp :: SharedContext -> C.Prop -> Env -> IO Env
bindProp sc prop env = do
let env' = liftEnv env
v <- scLocalVar sc 0
k <- scSort sc (mkSort 0)
return $ env' { envP = insertSupers prop [] v (envP env')
, envS = k : envS env'
}
-- | When we insert a nonerasable prop into the environment, make
-- sure to also insert all its superclasses. We arrange it so
-- that every class dictionary contains the implementation of its
-- superclass dictionaries, which can be extracted via field projections.
insertSupers ::
C.Prop ->
[FieldName] {- Field names to project the associated class (in reverse order) -} ->
Term ->
Map C.Prop (Term, [FieldName], Int) ->
Map C.Prop (Term, [FieldName], Int)
insertSupers prop fs v m
-- If the prop is already in the map, stop
| Just _ <- Map.lookup prop m = m
-- Insert the prop and check if it has any superclasses that also need to be added
| otherwise = Map.insert (normalizeProp prop) (v, fs, 0) $ go prop
where
super p f t = insertSupers (C.TCon (C.PC p) [t]) (f:fs) v
go (C.TCon (C.PC p) [t]) =
case p of
C.PRing -> super C.PZero "ringZero" t m
C.PLogic -> super C.PZero "logicZero" t m
C.PField -> super C.PRing "fieldRing" t m
C.PIntegral -> super C.PRing "integralRing" t m
C.PRound -> super C.PField "roundField" t . super C.PCmp "roundCmp" t $ m
C.PCmp -> super C.PEq "cmpEq" t m
C.PSignedCmp -> super C.PEq "signedCmpEq" t m
_ -> m
go _ = m
-- | We normalize the first argument of 'Literal' class constraints
-- arbitrarily to 'inf', so that we can ignore that parameter when
-- matching dictionaries.
normalizeProp :: C.Prop -> C.Prop
normalizeProp prop
| Just (_, a) <- C.pIsLiteral prop = C.pLiteral C.tInf a
| Just (_, a) <- C.pIsLiteralLessThan prop = C.pLiteralLessThan C.tInf a
| otherwise = prop
--------------------------------------------------------------------------------
importKind :: SharedContext -> C.Kind -> IO Term
importKind sc kind =
case kind of
C.KType -> scISort sc (mkSort 0)
C.KNum -> scDataTypeApp sc "Cryptol.Num" []
C.KProp -> scSort sc (mkSort 0)
(C.:->) k1 k2 -> join $ scFun sc <$> importKind sc k1 <*> importKind sc k2
importTFun :: SharedContext -> C.TFun -> IO Term
importTFun sc tf =
case tf of
C.TCWidth -> scGlobalDef sc "Cryptol.tcWidth"
C.TCAdd -> scGlobalDef sc "Cryptol.tcAdd"
C.TCSub -> scGlobalDef sc "Cryptol.tcSub"
C.TCMul -> scGlobalDef sc "Cryptol.tcMul"
C.TCDiv -> scGlobalDef sc "Cryptol.tcDiv"
C.TCMod -> scGlobalDef sc "Cryptol.tcMod"
C.TCExp -> scGlobalDef sc "Cryptol.tcExp"
C.TCMin -> scGlobalDef sc "Cryptol.tcMin"
C.TCMax -> scGlobalDef sc "Cryptol.tcMax"
C.TCCeilDiv -> scGlobalDef sc "Cryptol.tcCeilDiv"
C.TCCeilMod -> scGlobalDef sc "Cryptol.tcCeilMod"
C.TCLenFromThenTo -> scGlobalDef sc "Cryptol.tcLenFromThenTo"
-- | Precondition: @not ('isErasedProp' pc)@.
importPC :: SharedContext -> C.PC -> IO Term
importPC sc pc =
case pc of
C.PEqual -> panic "importPC PEqual" []
C.PNeq -> panic "importPC PNeq" []
C.PGeq -> panic "importPC PGeq" []
C.PFin -> panic "importPC PFin" []
C.PHas _ -> panic "importPC PHas" []
C.PPrime -> panic "importPC PPrime" []
C.PZero -> scGlobalDef sc "Cryptol.PZero"
C.PLogic -> scGlobalDef sc "Cryptol.PLogic"
C.PRing -> scGlobalDef sc "Cryptol.PRing"
C.PIntegral -> scGlobalDef sc "Cryptol.PIntegral"
C.PField -> scGlobalDef sc "Cryptol.PField"
C.PRound -> scGlobalDef sc "Cryptol.PRound"
C.PEq -> scGlobalDef sc "Cryptol.PEq"
C.PCmp -> scGlobalDef sc "Cryptol.PCmp"
C.PSignedCmp -> scGlobalDef sc "Cryptol.PSignedCmp"
C.PLiteral -> scGlobalDef sc "Cryptol.PLiteral"
C.PLiteralLessThan -> scGlobalDef sc "Cryptol.PLiteralLessThan"
C.PAnd -> panic "importPC PAnd" []
C.PTrue -> panic "importPC PTrue" []
C.PFLiteral -> panic "importPC PFLiteral" []
C.PValidFloat -> panic "importPC PValidFloat" []
-- | Translate size types to SAW values of type Num, value types to SAW types of sort 0.
importType :: SharedContext -> Env -> C.Type -> IO Term
importType sc env ty =
case ty of
C.TVar tvar ->
case tvar of
C.TVFree{} {- Int Kind (Set TVar) Doc -} -> unimplemented "TVFree"
C.TVBound v -> case Map.lookup (C.tpUnique v) (envT env) of
Just (t, j) -> incVars sc 0 j t
Nothing -> panic "importType TVBound" []
C.TUser _ _ t -> go t
C.TRec fm ->
importType sc env (C.tTuple (map snd (C.canonicalFields fm)))
C.TNewtype nt ts ->
do let s = C.listSubst (zip (map C.TVBound (C.ntParams nt)) ts)
let t = plainSubst s (C.TRec (C.ntFields nt))
go t
C.TCon tcon tyargs ->
case tcon of
C.TC tc ->
case tc of
C.TCNum n -> scCtorApp sc "Cryptol.TCNum" =<< sequence [scNat sc (fromInteger n)]
C.TCInf -> scCtorApp sc "Cryptol.TCInf" []
C.TCBit -> scBoolType sc
C.TCInteger -> scIntegerType sc
C.TCIntMod -> scGlobalApply sc "Cryptol.IntModNum" =<< traverse go tyargs
C.TCFloat -> scGlobalApply sc "Cryptol.TCFloat" =<< traverse go tyargs
C.TCArray -> do a <- go (tyargs !! 0)
b <- go (tyargs !! 1)
scArrayType sc a b
C.TCRational -> scGlobalApply sc "Cryptol.Rational" []
C.TCSeq -> scGlobalApply sc "Cryptol.seq" =<< traverse go tyargs
C.TCFun -> do a <- go (tyargs !! 0)
b <- go (tyargs !! 1)
scFun sc a b
C.TCTuple _n -> scTupleType sc =<< traverse go tyargs
C.TCAbstract (C.UserTC n _)
| Just prim <- C.asPrim n
, Just t <- Map.lookup prim (envPrimTypes env) ->
scApplyAllBeta sc t =<< traverse go tyargs
| True -> panic ("importType: unknown primitive type: " ++ show n) []
C.PC pc ->
case pc of
C.PLiteral -> -- we omit first argument to class Literal
do a <- go (tyargs !! 1)
scGlobalApply sc "Cryptol.PLiteral" [a]
C.PLiteralLessThan -> -- we omit first argument to class LiteralLessThan
do a <- go (tyargs !! 1)
scGlobalApply sc "Cryptol.PLiteralLessThan" [a]
_ ->
do pc' <- importPC sc pc
tyargs' <- traverse go tyargs
scApplyAll sc pc' tyargs'
C.TF tf ->
do tf' <- importTFun sc tf
tyargs' <- traverse go tyargs
scApplyAll sc tf' tyargs'
C.TError _k ->
panic "importType TError" []
where
go = importType sc env
isErasedProp :: C.Prop -> Bool
isErasedProp prop =
case prop of
C.TCon (C.PC C.PZero ) _ -> False
C.TCon (C.PC C.PLogic ) _ -> False
C.TCon (C.PC C.PRing ) _ -> False
C.TCon (C.PC C.PIntegral ) _ -> False
C.TCon (C.PC C.PField ) _ -> False
C.TCon (C.PC C.PRound ) _ -> False
C.TCon (C.PC C.PEq ) _ -> False
C.TCon (C.PC C.PCmp ) _ -> False
C.TCon (C.PC C.PSignedCmp ) _ -> False
C.TCon (C.PC C.PLiteral ) _ -> False
C.TCon (C.PC C.PLiteralLessThan) _ -> False
_ -> True
importPropsType :: SharedContext -> Env -> [C.Prop] -> C.Type -> IO Term
importPropsType sc env [] ty = importType sc env ty
importPropsType sc env (prop : props) ty
| isErasedProp prop = importPropsType sc env props ty
| otherwise =
do p <- importType sc env prop
t <- importPropsType sc env props ty
scFun sc p t
nameToLocalName :: C.Name -> LocalName
nameToLocalName = C.identText . C.nameIdent
nameToFieldName :: C.Name -> FieldName
nameToFieldName = C.identText . C.nameIdent
tparamToLocalName :: C.TParam -> LocalName
tparamToLocalName tp = maybe (Text.pack ("u" ++ show (C.tpUnique tp))) nameToLocalName (C.tpName tp)
importPolyType :: SharedContext -> Env -> [C.TParam] -> [C.Prop] -> C.Type -> IO Term
importPolyType sc env [] props ty = importPropsType sc env props ty
importPolyType sc env (tp : tps) props ty =
do k <- importKind sc (C.tpKind tp)
env' <- bindTParam sc tp env
t <- importPolyType sc env' tps props ty
scPi sc (tparamToLocalName tp) k t
importSchema :: SharedContext -> Env -> C.Schema -> IO Term
importSchema sc env (C.Forall tparams props ty) = importPolyType sc env tparams props ty
proveProp :: HasCallStack => SharedContext -> Env -> C.Prop -> IO Term
proveProp sc env prop =
case Map.lookup (normalizeProp prop) (envP env) of
-- Class dictionary was provided as an argument
Just (prf, fs, j) ->
do -- shift deBruijn indicies by j
v <- incVars sc 0 j prf
-- apply field projections as necessary to compute superclasses
-- NB: reverse the order of the fields
foldM (scRecordSelect sc) v (reverse fs)
-- Class dictionary not provided, compute it from the structure of types
Nothing ->
case prop of
-- instance Zero Bit
(C.pIsZero -> Just (C.tIsBit -> True))
-> do scGlobalApply sc "Cryptol.PZeroBit" []
-- instance Zero Integer
(C.pIsZero -> Just (C.tIsInteger -> True))
-> do scGlobalApply sc "Cryptol.PZeroInteger" []
-- instance Zero (Z n)
(C.pIsZero -> Just (C.tIsIntMod -> Just n))
-> do n' <- importType sc env n
scGlobalApply sc "Cryptol.PZeroIntModNum" [n']
-- instance Zero Rational
(C.pIsZero -> Just (C.tIsRational -> True))
-> do scGlobalApply sc "Cryptol.PZeroRational" []
-- instance Zero [n]
(C.pIsZero -> Just (C.tIsSeq -> Just (n, C.tIsBit -> True)))
-> do n' <- importType sc env n
scGlobalApply sc "Cryptol.PZeroSeqBool" [n']
-- instance ValidFloat e p => Zero (Float e p)
(C.pIsZero -> Just (C.tIsFloat -> Just (e, p)))
-> do e' <- importType sc env e
p' <- importType sc env p
scGlobalApply sc "Cryptol.PZeroFloat" [e', p']
-- instance (Zero a) => Zero [n]a
(C.pIsZero -> Just (C.tIsSeq -> Just (n, a)))
-> do n' <- importType sc env n
a' <- importType sc env a
pa <- proveProp sc env (C.pZero a)
scGlobalApply sc "Cryptol.PZeroSeq" [n', a', pa]
-- instance (Zero b) => Zero (a -> b)
(C.pIsZero -> Just (C.tIsFun -> Just (a, b)))
-> do a' <- importType sc env a
b' <- importType sc env b
pb <- proveProp sc env (C.pZero b)
scGlobalApply sc "Cryptol.PZeroFun" [a', b', pb]
-- instance (Zero a, Zero b, ...) => Zero (a, b, ...)
(C.pIsZero -> Just (C.tIsTuple -> Just ts))
-> do ps <- traverse (proveProp sc env . C.pZero) ts
scTuple sc ps
-- instance (Zero a, Zero b, ...) => Zero { x : a, y : b, ... }
(C.pIsZero -> Just (C.tIsRec -> Just fm))
-> do proveProp sc env (C.pZero (C.tTuple (map snd (C.canonicalFields fm))))
-- instance Logic Bit
(C.pIsLogic -> Just (C.tIsBit -> True))
-> do scGlobalApply sc "Cryptol.PLogicBit" []
-- instance Logic [n]
(C.pIsLogic -> Just (C.tIsSeq -> Just (n, C.tIsBit -> True)))
-> do n' <- importType sc env n
scGlobalApply sc "Cryptol.PLogicSeqBool" [n']
-- instance (Logic a) => Logic [n]a
(C.pIsLogic -> Just (C.tIsSeq -> Just (n, a)))
-> do n' <- importType sc env n
a' <- importType sc env a
pa <- proveProp sc env (C.pLogic a)
scGlobalApply sc "Cryptol.PLogicSeq" [n', a', pa]
-- instance (Logic b) => Logic (a -> b)
(C.pIsLogic -> Just (C.tIsFun -> Just (a, b)))
-> do a' <- importType sc env a
b' <- importType sc env b
pb <- proveProp sc env (C.pLogic b)
scGlobalApply sc "Cryptol.PLogicFun" [a', b', pb]
-- instance Logic ()
(C.pIsLogic -> Just (C.tIsTuple -> Just []))
-> do scGlobalApply sc "Cryptol.PLogicUnit" []
-- instance (Logic a, Logic b) => Logic (a, b)
(C.pIsLogic -> Just (C.tIsTuple -> Just [t]))
-> do proveProp sc env (C.pLogic t)
(C.pIsLogic -> Just (C.tIsTuple -> Just (t : ts)))
-> do a <- importType sc env t
b <- importType sc env (C.tTuple ts)
pa <- proveProp sc env (C.pLogic t)
pb <- proveProp sc env (C.pLogic (C.tTuple ts))
scGlobalApply sc "Cryptol.PLogicPair" [a, b, pa, pb]
-- instance (Logic a, Logic b, ...) => instance Logic { x : a, y : b, ... }
(C.pIsLogic -> Just (C.tIsRec -> Just fm))
-> do proveProp sc env (C.pLogic (C.tTuple (map snd (C.canonicalFields fm))))
-- instance Ring Integer
(C.pIsRing -> Just (C.tIsInteger -> True))
-> do scGlobalApply sc "Cryptol.PRingInteger" []
-- instance Ring (Z n)
(C.pIsRing -> Just (C.tIsIntMod -> Just n))
-> do n' <- importType sc env n
scGlobalApply sc "Cryptol.PRingIntModNum" [n']
-- instance Ring Rational
(C.pIsRing -> Just (C.tIsRational -> True))
-> do scGlobalApply sc "Cryptol.PRingRational" []
-- instance (fin n) => Ring [n]
(C.pIsRing -> Just (C.tIsSeq -> Just (n, C.tIsBit -> True)))
-> do n' <- importType sc env n
scGlobalApply sc "Cryptol.PRingSeqBool" [n']
-- instance ValidFloat e p => Ring (Float e p)
(C.pIsRing -> Just (C.tIsFloat -> Just (e, p)))
-> do e' <- importType sc env e
p' <- importType sc env p
scGlobalApply sc "Cryptol.PRingFloat" [e', p']
-- instance (Ring a) => Ring [n]a
(C.pIsRing -> Just (C.tIsSeq -> Just (n, a)))
-> do n' <- importType sc env n
a' <- importType sc env a
pa <- proveProp sc env (C.pRing a)
scGlobalApply sc "Cryptol.PRingSeq" [n', a', pa]
-- instance (Ring b) => Ring (a -> b)
(C.pIsRing -> Just (C.tIsFun -> Just (a, b)))
-> do a' <- importType sc env a
b' <- importType sc env b
pb <- proveProp sc env (C.pRing b)
scGlobalApply sc "Cryptol.PRingFun" [a', b', pb]
-- instance Ring ()
(C.pIsRing -> Just (C.tIsTuple -> Just []))
-> do scGlobalApply sc "Cryptol.PRingUnit" []
-- instance (Ring a, Ring b) => Ring (a, b)
(C.pIsRing -> Just (C.tIsTuple -> Just [t]))
-> do proveProp sc env (C.pRing t)
(C.pIsRing -> Just (C.tIsTuple -> Just (t : ts)))
-> do a <- importType sc env t
b <- importType sc env (C.tTuple ts)
pa <- proveProp sc env (C.pRing t)
pb <- proveProp sc env (C.pRing (C.tTuple ts))
scGlobalApply sc "Cryptol.PRingPair" [a, b, pa, pb]
-- instance (Ring a, Ring b, ...) => instance Ring { x : a, y : b, ... }
(C.pIsRing -> Just (C.tIsRec -> Just fm))
-> do proveProp sc env (C.pRing (C.tTuple (map snd (C.canonicalFields fm))))
-- instance Integral Integer
(C.pIsIntegral -> Just (C.tIsInteger -> True))
-> do scGlobalApply sc "Cryptol.PIntegralInteger" []
-- instance Integral [n]
(C.pIsIntegral -> Just (C.tIsSeq -> (Just (n, C.tIsBit -> True))))
-> do n' <- importType sc env n
scGlobalApply sc "Cryptol.PIntegralSeqBool" [n']
-- instance Field Rational
(C.pIsField -> Just (C.tIsRational -> True))
-> do scGlobalApply sc "Cryptol.PFieldRational" []
-- instance (prime p) => Field (Z p)
(C.pIsField -> Just (C.tIsIntMod -> Just n))
-> do n' <- importType sc env n
scGlobalApply sc "Cryptol.PFieldIntModNum" [n']
-- instance (ValidFloat e p) => Field (Float e p)
(C.pIsField -> Just (C.tIsFloat -> Just (e, p)))
-> do e' <- importType sc env e
p' <- importType sc env p
scGlobalApply sc "Cryptol.PFieldFloat" [e', p']
-- instance Round Rational
(C.pIsRound -> Just (C.tIsRational -> True))
-> do scGlobalApply sc "Cryptol.PRoundRational" []
-- instance (ValidFloat e p) => Round (Float e p)
(C.pIsRound -> Just (C.tIsFloat -> Just (e, p)))
-> do e' <- importType sc env e
p' <- importType sc env p
scGlobalApply sc "Cryptol.PRoundFloat" [e', p']
-- instance Eq Bit
(C.pIsEq -> Just (C.tIsBit -> True))
-> do scGlobalApply sc "Cryptol.PEqBit" []
-- instance Eq Integer
(C.pIsEq -> Just (C.tIsInteger -> True))
-> do scGlobalApply sc "Cryptol.PEqInteger" []
-- instance Eq (Z n)
(C.pIsEq -> Just (C.tIsIntMod -> Just n))
-> do n' <- importType sc env n
scGlobalApply sc "Cryptol.PEqIntModNum" [n']
-- instance Eq Rational
(C.pIsEq -> Just (C.tIsRational -> True))
-> do scGlobalApply sc "Cryptol.PEqRational" []
-- instance Eq (Float e p)
(C.pIsEq -> Just (C.tIsFloat -> Just (e, p)))
-> do e' <- importType sc env e
p' <- importType sc env p
scGlobalApply sc "Cryptol.PEqFloat" [e', p']
-- instance (fin n) => Eq [n]
(C.pIsEq -> Just (C.tIsSeq -> Just (n, C.tIsBit -> True)))
-> do n' <- importType sc env n
scGlobalApply sc "Cryptol.PEqSeqBool" [n']
-- instance (fin n, Eq a) => Eq [n]a
(C.pIsEq -> Just (C.tIsSeq -> Just (n, a)))
-> do n' <- importType sc env n
a' <- importType sc env a
pa <- proveProp sc env (C.pEq a)
scGlobalApply sc "Cryptol.PEqSeq" [n', a', pa]
-- instance Eq ()
(C.pIsEq -> Just (C.tIsTuple -> Just []))
-> do scGlobalApply sc "Cryptol.PEqUnit" []
-- instance (Eq a, Eq b) => Eq (a, b)
(C.pIsEq -> Just (C.tIsTuple -> Just [t]))
-> do proveProp sc env (C.pEq t)
(C.pIsEq -> Just (C.tIsTuple -> Just (t : ts)))
-> do a <- importType sc env t
b <- importType sc env (C.tTuple ts)
pa <- proveProp sc env (C.pEq t)
pb <- proveProp sc env (C.pEq (C.tTuple ts))
scGlobalApply sc "Cryptol.PEqPair" [a, b, pa, pb]
-- instance (Eq a, Eq b, ...) => instance Eq { x : a, y : b, ... }
(C.pIsEq -> Just (C.tIsRec -> Just fm))
-> do proveProp sc env (C.pEq (C.tTuple (map snd (C.canonicalFields fm))))
-- instance Cmp Bit
(C.pIsCmp -> Just (C.tIsBit -> True))
-> do scGlobalApply sc "Cryptol.PCmpBit" []
-- instance Cmp Integer
(C.pIsCmp -> Just (C.tIsInteger -> True))
-> do scGlobalApply sc "Cryptol.PCmpInteger" []
-- instance Cmp Rational
(C.pIsCmp -> Just (C.tIsRational -> True))
-> do scGlobalApply sc "Cryptol.PCmpRational" []
-- instance Cmp (Float e p)
(C.pIsCmp -> Just (C.tIsFloat -> Just (e, p)))
-> do e' <- importType sc env e
p' <- importType sc env p
scGlobalApply sc "Cryptol.PCmpFloat" [e', p']
-- instance (fin n) => Cmp [n]
(C.pIsCmp -> Just (C.tIsSeq -> Just (n, C.tIsBit -> True)))
-> do n' <- importType sc env n
scGlobalApply sc "Cryptol.PCmpSeqBool" [n']
-- instance (fin n, Cmp a) => Cmp [n]a
(C.pIsCmp -> Just (C.tIsSeq -> Just (n, a)))
-> do n' <- importType sc env n
a' <- importType sc env a
pa <- proveProp sc env (C.pCmp a)
scGlobalApply sc "Cryptol.PCmpSeq" [n', a', pa]
-- instance Cmp ()
(C.pIsCmp -> Just (C.tIsTuple -> Just []))
-> do scGlobalApply sc "Cryptol.PCmpUnit" []
-- instance (Cmp a, Cmp b) => Cmp (a, b)
(C.pIsCmp -> Just (C.tIsTuple -> Just [t]))
-> do proveProp sc env (C.pCmp t)
(C.pIsCmp -> Just (C.tIsTuple -> Just (t : ts)))
-> do a <- importType sc env t
b <- importType sc env (C.tTuple ts)
pa <- proveProp sc env (C.pCmp t)
pb <- proveProp sc env (C.pCmp (C.tTuple ts))
scGlobalApply sc "Cryptol.PCmpPair" [a, b, pa, pb]
-- instance (Cmp a, Cmp b, ...) => instance Cmp { x : a, y : b, ... }
(C.pIsCmp -> Just (C.tIsRec -> Just fm))
-> do proveProp sc env (C.pCmp (C.tTuple (map snd (C.canonicalFields fm))))
-- instance (fin n) => SignedCmp [n]
(C.pIsSignedCmp -> Just (C.tIsSeq -> Just (n, C.tIsBit -> True)))
-> do n' <- importType sc env n
scGlobalApply sc "Cryptol.PSignedCmpSeqBool" [n']
-- instance (fin n, SignedCmp a) => SignedCmp [n]a
(C.pIsSignedCmp -> Just (C.tIsSeq -> Just (n, a)))
-> do n' <- importType sc env n
a' <- importType sc env a
pa <- proveProp sc env (C.pSignedCmp a)
scGlobalApply sc "Cryptol.PSignedCmpSeq" [n', a', pa]
-- instance SignedCmp ()
(C.pIsSignedCmp -> Just (C.tIsTuple -> Just []))
-> do scGlobalApply sc "Cryptol.PSignedCmpUnit" []
-- instance (SignedCmp a, SignedCmp b) => SignedCmp (a, b)
(C.pIsSignedCmp -> Just (C.tIsTuple -> Just [t]))
-> do proveProp sc env (C.pSignedCmp t)
(C.pIsSignedCmp -> Just (C.tIsTuple -> Just (t : ts)))
-> do a <- importType sc env t
b <- importType sc env (C.tTuple ts)
pa <- proveProp sc env (C.pSignedCmp t)
pb <- proveProp sc env (C.pSignedCmp (C.tTuple ts))
scGlobalApply sc "Cryptol.PSignedCmpPair" [a, b, pa, pb]
-- instance (SignedCmp a, SignedCmp b, ...) => instance SignedCmp { x : a, y : b, ... }
(C.pIsSignedCmp -> Just (C.tIsRec -> Just fm))
-> do proveProp sc env (C.pSignedCmp (C.tTuple (map snd (C.canonicalFields fm))))
-- instance Literal val Bit
(C.pIsLiteral -> Just (_, C.tIsBit -> True))
-> do scGlobalApply sc "Cryptol.PLiteralBit" []
-- instance Literal val Integer
(C.pIsLiteral -> Just (_, C.tIsInteger -> True))
-> do scGlobalApply sc "Cryptol.PLiteralInteger" []
-- instance Literal val (Z n)
(C.pIsLiteral -> Just (_, C.tIsIntMod -> Just n))
-> do n' <- importType sc env n
scGlobalApply sc "Cryptol.PLiteralIntModNum" [n']
-- instance Literal val Rational
(C.pIsLiteral -> Just (_, C.tIsRational -> True))
-> do scGlobalApply sc "Cryptol.PLiteralRational" []
-- instance (fin n, n >= width val) => Literal val [n]
(C.pIsLiteral -> Just (_, C.tIsSeq -> Just (n, C.tIsBit -> True)))
-> do n' <- importType sc env n
scGlobalApply sc "Cryptol.PLiteralSeqBool" [n']
-- instance ValidFloat e p => Literal val (Float e p) (with extra constraints)
(C.pIsLiteral -> Just (_, C.tIsFloat -> Just (e, p)))
-> do e' <- importType sc env e
p' <- importType sc env p
scGlobalApply sc "Cryptol.PLiteralFloat" [e', p']
-- instance (2 >= val) => LiteralLessThan val Bit
(C.pIsLiteralLessThan -> Just (_, C.tIsBit -> True))
-> do scGlobalApply sc "Cryptol.PLiteralBit" []
-- instance LiteralLessThan val Integer
(C.pIsLiteralLessThan -> Just (_, C.tIsInteger -> True))
-> do scGlobalApply sc "Cryptol.PLiteralInteger" []
-- instance (fin n, n >= 1, n >= val) LiteralLessThan val (Z n)
(C.pIsLiteralLessThan -> Just (_, C.tIsIntMod -> Just n))
-> do n' <- importType sc env n
scGlobalApply sc "Cryptol.PLiteralIntModNum" [n']
-- instance Literal val Rational
(C.pIsLiteralLessThan -> Just (_, C.tIsRational -> True))
-> do scGlobalApply sc "Cryptol.PLiteralRational" []
-- instance (fin n, n >= lg2 val) => Literal val [n]
(C.pIsLiteralLessThan -> Just (_, C.tIsSeq -> Just (n, C.tIsBit -> True)))
-> do n' <- importType sc env n
scGlobalApply sc "Cryptol.PLiteralSeqBool" [n']
-- instance ValidFloat e p => Literal val (Float e p) (with extra constraints)
(C.pIsLiteralLessThan -> Just (_, C.tIsFloat -> Just (e, p)))
-> do e' <- importType sc env e
p' <- importType sc env p
scGlobalApply sc "Cryptol.PLiteralFloat" [e', p']
_ -> do panic "proveProp" [pretty prop]
importPrimitive :: SharedContext -> ImportPrimitiveOptions -> Env -> C.Name -> C.Schema -> IO Term
importPrimitive sc primOpts env n sch
-- lookup primitive in the main primitive lookup table
| Just nm <- C.asPrim n, Just term <- Map.lookup nm allPrims = term sc
-- lookup primitive in the main reference implementation lookup table
| Just nm <- C.asPrim n, Just expr <- Map.lookup nm (envRefPrims env) =
do t <- importSchema sc env sch
e <- importExpr sc env expr
nmi <- importName n
scConstant' sc nmi e t
-- lookup primitive in the extra primitive lookup table
| Just nm <- C.asPrim n, Just t <- Map.lookup nm (envPrims env) = return t
-- Optionally, create an opaque constant representing the primitive
-- if it doesn't match one of the ones we know about.
| Just _ <- C.asPrim n, allowUnknownPrimitives primOpts =
do t <- importSchema sc env sch
nmi <- importName n
scOpaqueConstant sc nmi t
-- Panic if we don't know the given primitive (TODO? probably shouldn't be a panic)
| Just nm <- C.asPrim n = panic "Unknown Cryptol primitive name" [show nm]
| otherwise = panic "Improper Cryptol primitive name" [show n]
allPrims :: Map C.PrimIdent (SharedContext -> IO Term)
allPrims = prelPrims <> arrayPrims <> floatPrims <> suiteBPrims <> primeECPrims
prelPrims :: Map C.PrimIdent (SharedContext -> IO Term)
prelPrims =
Map.fromList $
first C.prelPrim <$>
[ ("True", flip scBool True)
, ("False", flip scBool False)
, ("number", flip scGlobalDef "Cryptol.ecNumber") -- Converts a numeric type into its corresponding value.
-- -- {val, a} (Literal val a) => a
, ("fromZ", flip scGlobalDef "Cryptol.ecFromZ") -- {n} (fin n, n >= 1) => Z n -> Integer
-- -- Zero
, ("zero", flip scGlobalDef "Cryptol.ecZero") -- {a} (Zero a) => a
-- -- Logic
, ("&&", flip scGlobalDef "Cryptol.ecAnd") -- {a} (Logic a) => a -> a -> a
, ("||", flip scGlobalDef "Cryptol.ecOr") -- {a} (Logic a) => a -> a -> a
, ("^", flip scGlobalDef "Cryptol.ecXor") -- {a} (Logic a) => a -> a -> a
, ("complement", flip scGlobalDef "Cryptol.ecCompl") -- {a} (Logic a) => a -> a
-- -- Ring
, ("fromInteger", flip scGlobalDef "Cryptol.ecFromInteger") -- {a} (Ring a) => Integer -> a
, ("+", flip scGlobalDef "Cryptol.ecPlus") -- {a} (Ring a) => a -> a -> a
, ("-", flip scGlobalDef "Cryptol.ecMinus") -- {a} (Ring a) => a -> a -> a
, ("*", flip scGlobalDef "Cryptol.ecMul") -- {a} (Ring a) => a -> a -> a
, ("negate", flip scGlobalDef "Cryptol.ecNeg") -- {a} (Ring a) => a -> a
-- -- Integral
, ("toInteger", flip scGlobalDef "Cryptol.ecToInteger") -- {a} (Integral a) => a -> Integer
, ("/", flip scGlobalDef "Cryptol.ecDiv") -- {a} (Integral a) => a -> a -> a
, ("%", flip scGlobalDef "Cryptol.ecMod") -- {a} (Integral a) => a -> a -> a
, ("^^", flip scGlobalDef "Cryptol.ecExp") -- {a} (Ring a, Integral b) => a -> b -> a
, ("infFrom", flip scGlobalDef "Cryptol.ecInfFrom") -- {a} (Integral a) => a -> [inf]a
, ("infFromThen", flip scGlobalDef "Cryptol.ecInfFromThen") -- {a} (Integral a) => a -> a -> [inf]a
-- -- Field
, ("recip", flip scGlobalDef "Cryptol.ecRecip") -- {a} (Field a) => a -> a
, ("/.", flip scGlobalDef "Cryptol.ecFieldDiv") -- {a} (Field a) => a -> a -> a
-- -- Round
, ("ceiling", flip scGlobalDef "Cryptol.ecCeiling") -- {a} (Round a) => a -> Integer
, ("floor", flip scGlobalDef "Cryptol.ecFloor") -- {a} (Round a) => a -> Integer
, ("trunc", flip scGlobalDef "Cryptol.ecTruncate") -- {a} (Round a) => a -> Integer
, ("roundAway", flip scGlobalDef "Cryptol.ecRoundAway") -- {a} (Round a) => a -> Integer
, ("roundToEven", flip scGlobalDef "Cryptol.ecRoundToEven") -- {a} (Round a) => a -> Integer
-- -- Eq
, ("==", flip scGlobalDef "Cryptol.ecEq") -- {a} (Eq a) => a -> a -> Bit
, ("!=", flip scGlobalDef "Cryptol.ecNotEq") -- {a} (Eq a) => a -> a -> Bit
-- -- Cmp
, ("<", flip scGlobalDef "Cryptol.ecLt") -- {a} (Cmp a) => a -> a -> Bit
, (">", flip scGlobalDef "Cryptol.ecGt") -- {a} (Cmp a) => a -> a -> Bit
, ("<=", flip scGlobalDef "Cryptol.ecLtEq") -- {a} (Cmp a) => a -> a -> Bit
, (">=", flip scGlobalDef "Cryptol.ecGtEq") -- {a} (Cmp a) => a -> a -> Bit
-- -- SignedCmp
, ("<$", flip scGlobalDef "Cryptol.ecSLt") -- {a} (SignedCmp a) => a -> a -> Bit
-- -- Bitvector primitives
, ("/$", flip scGlobalDef "Cryptol.ecSDiv") -- {n} (fin n, n>=1) => [n] -> [n] -> [n]
, ("%$", flip scGlobalDef "Cryptol.ecSMod") -- {n} (fin n, n>=1) => [n] -> [n] -> [n]
, ("lg2", flip scGlobalDef "Cryptol.ecLg2") -- {n} (fin n) => [n] -> [n]
, (">>$", flip scGlobalDef "Cryptol.ecSShiftR") -- {n, ix} (fin n, n >= 1, Integral ix) => [n] -> ix -> [n]
, ("toSignedInteger",
flip scGlobalDef "Cryptol.toSignedInteger") -- {n} (fin n, n >= 1) => [n] -> Integer
-- -- Rational primitives
, ("ratio", flip scGlobalDef "Cryptol.ecRatio") -- Integer -> Integer -> Rational
-- -- FLiteral
, ("fraction", flip scGlobalDef "Cryptol.ecFraction") -- {m, n, r, a} FLiteral m n r a => a
-- -- Shifts/rotates
, ("<<", flip scGlobalDef "Cryptol.ecShiftL") -- {n, ix, a} (Integral ix, Zero a) => [n]a -> ix -> [n]a
, (">>", flip scGlobalDef "Cryptol.ecShiftR") -- {n, ix, a} (Integral ix, Zero a) => [n]a -> ix -> [n]a
, ("<<<", flip scGlobalDef "Cryptol.ecRotL") -- {n, ix, a} (fin n, Integral ix) => [n]a -> ix -> [n]a
, (">>>", flip scGlobalDef "Cryptol.ecRotR") -- {n, ix, a} (fin n, Integral ix) => [n]a -> ix -> [n]a
-- -- Sequences primitives
, ("#", flip scGlobalDef "Cryptol.ecCat") -- {a,b,d} (fin a) => [a] d -> [b] d -> [a + b] d
, ("take", flip scGlobalDef "Cryptol.ecTake") -- {front, back, a} [front + back]a -> [front]a
, ("drop", flip scGlobalDef "Cryptol.ecDrop") -- {front, back, a} (fin front) => [front + back]a -> [back]a
, ("join", flip scGlobalDef "Cryptol.ecJoin") -- {a,b,c} (fin b) => [a][b]c -> [a * b]c
, ("split", flip scGlobalDef "Cryptol.ecSplit") -- {a,b,c} (fin b) => [a * b] c -> [a][b] c
, ("reverse", flip scGlobalDef "Cryptol.ecReverse") -- {a,b} (fin a) => [a] b -> [a] b
, ("transpose", flip scGlobalDef "Cryptol.ecTranspose") -- {a,b,c} [a][b]c -> [b][a]c
, ("@", flip scGlobalDef "Cryptol.ecAt") -- {n, a, ix} (Integral ix) => [n]a -> ix -> a
, ("!", flip scGlobalDef "Cryptol.ecAtBack") -- {n, a, ix} (fin n, Integral ix) => [n]a -> ix -> a
, ("update", flip scGlobalDef "Cryptol.ecUpdate") -- {n, a, ix} (Integral ix) => [n]a -> ix -> a -> [n]a
, ("updateEnd", flip scGlobalDef "Cryptol.ecUpdateEnd") -- {n, a, ix} (fin n, Integral ix) => [n]a -> ix -> a -> [n]a
-- -- Enumerations
, ("fromTo", flip scGlobalDef "Cryptol.ecFromTo")
-- fromTo : {first, last, bits, a}
-- ( fin last, fin bits, last >== first,
-- Literal first a, Literal last a)
-- => [1 + (last - first)]a
, ("fromToLessThan", flip scGlobalDef "Cryptol.ecFromToLessThan")
-- fromToLessThan : {first, bound, a}
-- ( fin first, bound >= first,
-- LiteralLessThan bound a)
-- => [bound - first]a
, ("fromThenTo", flip scGlobalDef "Cryptol.ecFromThenTo")
-- fromThenTo : {first, next, last, a, len}
-- ( fin first, fin next, fin last
-- , Literal first a, Literal next a, Literal last a
-- , first != next
-- , lengthFromThenTo first next last == len) => [len]a
, ("fromToBy", flip scGlobalDef "Cryptol.ecFromToBy")
-- fromToBy : {first, last, stride, a}
-- (fin last, fin stride, stride >= 1, last >= first, Literal last a) =>
-- [1 + (last - first)/stride]a
, ("fromToByLessThan", flip scGlobalDef "Cryptol.ecFromToByLessThan")
-- fromToByLessThan : {first, bound, stride, a}
-- (fin first, fin stride, stride >= 1, bound >= first, LiteralLessThan bound a) =>
-- [(bound - first)/^stride]a
, ("fromToDownBy", flip scGlobalDef "Cryptol.ecFromToDownBy")
-- fromToDownBy : {first, last, stride, a}
-- (fin first, fin stride, stride >= 1, first >= last, Literal first a) =>
-- [1 + (first - last)/stride]a
, ("fromToDownByGreaterThan", flip scGlobalDef "Cryptol.ecFromToDownByGreaterThan")
-- fromToDownByGreaterThan : {first, bound, stride, a}
-- (fin first, fin stride, stride >= 1, first >= bound, Literal first a) =>
-- [(first - bound)/^stride]a
-- Evaluation primitives: deepseq, parmap
, ("deepseq", flip scGlobalDef "Cryptol.ecDeepseq") -- {a, b} (Eq b) => a -> b -> b
, ("parmap", flip scGlobalDef "Cryptol.ecParmap") -- {a, b, n} (Eq b, fin n) => (a -> b) -> [n]a -> [n]b
, ("foldl", flip scGlobalDef "Cryptol.ecFoldl") -- {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a
, ("foldl'", flip scGlobalDef "Cryptol.ecFoldlPrime") -- {n, a, b} (fin n, Eq a) => (a -> b -> a) -> a -> [n]b -> a
, ("scanl", flip scGlobalDef "Cryptol.ecScanl") -- {n, a, b} (a -> b -> a) -> a -> [n]b -> [1+n]a
, ("error", flip scGlobalDef "Cryptol.ecError") -- {at,len} (fin len) => [len][8] -> at -- Run-time error
, ("random", flip scGlobalDef "Cryptol.ecRandom") -- {a} => [32] -> a -- Random values
, ("trace", flip scGlobalDef "Cryptol.ecTrace") -- {n,a,b} [n][8] -> a -> b -> b
]
arrayPrims :: Map C.PrimIdent (SharedContext -> IO Term)
arrayPrims =
Map.fromList $
first C.arrayPrim <$>
[ ("arrayConstant", flip scGlobalDef "Cryptol.ecArrayConstant") -- {a,b} b -> Array a b
, ("arrayLookup", flip scGlobalDef "Cryptol.ecArrayLookup") -- {a,b} Array a b -> a -> b
, ("arrayUpdate", flip scGlobalDef "Cryptol.ecArrayUpdate") -- {a,b} Array a b -> a -> b -> Array a b
, ("arrayCopy", flip scGlobalDef "Cryptol.ecArrayCopy") -- {n,a} Array [n] a -> [n] -> Array [n] a -> [n] -> [n] -> Array [n] a
, ("arrayEq", flip scGlobalDef "Cryptol.ecArrayEq") -- {a, b} (Array a b) -> (Array a b) -> Bool
, ("arraySet", flip scGlobalDef "Cryptol.ecArraySet") -- {n,a} Array [n] a -> [n] -> a -> [n] -> Array [n] a
, ("arrayRangeEqual", flip scGlobalDef "Cryptol.ecArrayRangeEq") -- {n,a} Array [n] a -> [n] -> Array [n] a -> [n] -> [n] -> Bit
]
floatPrims :: Map C.PrimIdent (SharedContext -> IO Term)
floatPrims =
Map.fromList $
first C.floatPrim <$>
[ ("fpNaN", flip scGlobalDef "Cryptol.ecFpNaN")
, ("fpPosInf", flip scGlobalDef "Cryptol.ecFpPosInf")
, ("fpFromBits", flip scGlobalDef "Cryptol.ecFpFromBits")
, ("fpToBits", flip scGlobalDef "Cryptol.ecFpToBits")
, ("=.=", flip scGlobalDef "Cryptol.ecFpEq")
, ("fpAdd", flip scGlobalDef "Cryptol.ecFpAdd")
, ("fpSub", flip scGlobalDef "Cryptol.ecFpSub")
, ("fpMul", flip scGlobalDef "Cryptol.ecFpMul")
, ("fpDiv", flip scGlobalDef "Cryptol.ecFpDiv")
, ("fpToRational", flip scGlobalDef "Cryptol.ecFpToRational")
, ("fpFromRational", flip scGlobalDef "Cryptol.ecFpFromRational")
, ("fpIsNaN", flip scGlobalDef "Cryptol.fpIsNaN")
, ("fpIsInf", flip scGlobalDef "Cryptol.fpIsInf")
, ("fpIsZero", flip scGlobalDef "Cryptol.fpIsZero")
, ("fpIsNeg", flip scGlobalDef "Cryptol.fpIsNeg")
, ("fpIsNormal", flip scGlobalDef "Cryptol.fpIsNormal")
, ("fpIsSubnormal", flip scGlobalDef "Cryptol.fpIsSubnormal")
, ("fpFMA", flip scGlobalDef "Cryptol.fpFMA")
, ("fpAbs", flip scGlobalDef "Cryptol.fpAbs")
, ("fpSqrt", flip scGlobalDef "Cryptol.fpSqrt")
]
suiteBPrims :: Map C.PrimIdent (SharedContext -> IO Term)
suiteBPrims =
Map.fromList $
first C.suiteBPrim <$>
[ ("AESEncRound", flip scGlobalDef "Cryptol.AESEncRound")
, ("AESEncFinalRound", flip scGlobalDef "Cryptol.AESEncFinalRound")
, ("AESDecRound", flip scGlobalDef "Cryptol.AESDecRound")
, ("AESDecFinalRound", flip scGlobalDef "Cryptol.AESDecFinalRound")
, ("AESInvMixColumns", flip scGlobalDef "Cryptol.AESInvMixColumns")
, ("AESKeyExpand", flip scGlobalDef "Cryptol.AESKeyExpand")
, ("processSHA2_224", flip scGlobalDef "Cryptol.processSHA2_224")
, ("processSHA2_256", flip scGlobalDef "Cryptol.processSHA2_256")
, ("processSHA2_384", flip scGlobalDef "Cryptol.processSHA2_384")
, ("processSHA2_512", flip scGlobalDef "Cryptol.processSHA2_512")
]
primeECPrims :: Map C.PrimIdent (SharedContext -> IO Term)
primeECPrims =
Map.fromList $
first C.primeECPrim <$>
[ ("ec_double", flip scGlobalDef "Cryptol.ec_double")
, ("ec_add_nonzero", flip scGlobalDef "Cryptol.ec_add_nonzero")
, ("ec_mult", flip scGlobalDef "Cryptol.ec_mult")
, ("ec_twin_mult", flip scGlobalDef "Cryptol.ec_twin_mult")
]
-- | Convert a Cryptol expression to a SAW-Core term. Calling
-- 'scTypeOf' on the result of @'importExpr' sc env expr@ must yield a
-- type that is equivalent (i.e. convertible) with the one returned by
-- @'importSchema' sc env ('fastTypeOf' ('envC' env) expr)@.
importExpr :: SharedContext -> Env -> C.Expr -> IO Term
importExpr sc env expr =
case expr of
C.EList es t ->
do t' <- importType sc env t
es' <- traverse (importExpr' sc env (C.tMono t)) es
scVector sc t' es'
C.ETuple es ->
do es' <- traverse (importExpr sc env) es
scTuple sc es'
C.ERec fm ->
do es' <- traverse (importExpr sc env . snd) (C.canonicalFields fm)
scTuple sc es'
C.ESel e sel ->
-- Elimination for tuple/record/list
case sel of
C.TupleSel i _maybeLen ->
do e' <- importExpr sc env e
let t = fastTypeOf (envC env) e
case C.tIsTuple t of
Just ts -> scTupleSelector sc e' (i+1) (length ts)
Nothing -> panic "importExpr" ["invalid tuple selector", show i, pretty t]
C.RecordSel x _ ->
do e' <- importExpr sc env e
let t = fastTypeOf (envC env) e
case C.tNoUser t of
C.TRec fm ->
do i <- the (elemIndex x (map fst (C.canonicalFields fm)))
scTupleSelector sc e' (i+1) (length (C.canonicalFields fm))
C.TNewtype nt _args ->
do let fs = C.ntFields nt
i <- the (elemIndex x (map fst (C.canonicalFields fs)))
scTupleSelector sc e' (i+1) (length (C.canonicalFields fs))
_ -> panic "importExpr" ["invalid record selector", pretty x, pretty t]
C.ListSel i _maybeLen ->
do let t = fastTypeOf (envC env) e
(n, a) <-
case C.tIsSeq t of
Just (n, a) -> return (n, a)
Nothing -> panic "importExpr" ["ListSel: not a list type"]
a' <- importType sc env a
n' <- importType sc env n
e' <- importExpr sc env e
i' <- scNat sc (fromIntegral i)
scGlobalApply sc "Cryptol.eListSel" [a', n', e', i']
C.ESet _ e1 sel e2 ->
case sel of
C.TupleSel i _maybeLen ->
do e1' <- importExpr sc env e1
e2' <- importExpr sc env e2
let t1 = fastTypeOf (envC env) e1
case C.tIsTuple t1 of
Nothing -> panic "importExpr" ["ESet/TupleSel: not a tuple type"]
Just ts ->
do ts' <- traverse (importType sc env) ts
let t2' = ts' !! i
f <- scGlobalApply sc "Cryptol.const" [t2', t2', e2']
g <- tupleUpdate sc f i ts'
scApply sc g e1'
C.RecordSel x _ ->
do e1' <- importExpr sc env e1
e2' <- importExpr sc env e2
let t1 = fastTypeOf (envC env) e1
case C.tIsRec t1 of
Nothing -> panic "importExpr" ["ESet/RecordSel: not a record type"]
Just tm ->
do i <- the (elemIndex x (map fst (C.canonicalFields tm)))
ts' <- traverse (importType sc env . snd) (C.canonicalFields tm)
let t2' = ts' !! i
f <- scGlobalApply sc "Cryptol.const" [t2', t2', e2']
g <- tupleUpdate sc f i ts'
scApply sc g e1'
C.ListSel _i _maybeLen ->
panic "importExpr" ["ESet/ListSel: unsupported"]
C.EIf e1 e2 e3 ->
do let ty = fastTypeOf (envC env) e2
ty' <- importType sc env ty
e1' <- importExpr sc env e1
e2' <- importExpr sc env e2
e3' <- importExpr' sc env (C.tMono ty) e3
scGlobalApply sc "Prelude.ite" [ty', e1', e2', e3']
C.EComp len eltty e mss ->
importComp sc env len eltty e mss
C.EVar qname ->
case Map.lookup qname (envE env) of
Just (e', j) -> incVars sc 0 j e'
Nothing -> panic "importExpr" ["unknown variable: " ++ show qname]