-
Notifications
You must be signed in to change notification settings - Fork 123
/
Copy pathReference.lhs
1798 lines (1631 loc) · 64.9 KB
/
Reference.lhs
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
> -- |
> -- Module : Cryptol.Eval.Reference
> -- Description : The reference implementation of the Cryptol evaluation semantics.
> -- Copyright : (c) 2013-2020 Galois, Inc.
> -- License : BSD3
> -- Maintainer : [email protected]
> -- Stability : provisional
> -- Portability : portable
>
> {-# LANGUAGE BlockArguments #-}
> {-# LANGUAGE PatternGuards #-}
> {-# LANGUAGE LambdaCase #-}
>
> module Cryptol.Eval.Reference
> ( Value(..)
> , E(..)
> , evaluate
> , evalExpr
> , evalDeclGroup
> , ppValue
> , ppEValue
> ) where
>
> import Data.Bits
> import Data.Ratio((%))
> import Data.List
> (genericIndex, genericLength, genericReplicate, genericTake, sortBy)
> import Data.Ord (comparing)
> import Data.Map (Map)
> import qualified Data.Map as Map
> import qualified Data.Text as T (pack)
> import LibBF (BigFloat)
> import qualified LibBF as FP
> import qualified GHC.Num.Compat as Integer
>
> import Cryptol.ModuleSystem.Name (asPrim)
> import Cryptol.TypeCheck.Solver.InfNat (Nat'(..), nAdd, nMin, nMul)
> import Cryptol.TypeCheck.AST
> import Cryptol.Backend.FloatHelpers (BF(..))
> import qualified Cryptol.Backend.FloatHelpers as FP
> import Cryptol.Backend.Monad (EvalError(..))
> import Cryptol.Eval.Type
> (TValue(..), isTBit, evalValType, evalNumType, TypeEnv, bindTypeVar)
> import Cryptol.Eval.Concrete (mkBv, ppBV, lg2)
> import Cryptol.Utils.Ident (Ident,PrimIdent, prelPrim, floatPrim)
> import Cryptol.Utils.Panic (panic)
> import Cryptol.Utils.PP
> import Cryptol.Utils.RecordMap
>
> import qualified Cryptol.ModuleSystem as M
> import qualified Cryptol.ModuleSystem.Env as M (loadedModules,loadedNewtypes)
Overview
========
This file describes the semantics of the explicitly-typed Cryptol
language (i.e., terms after type checking). Issues related to type
inference, type functions, and type constraints are beyond the scope
of this document.
Cryptol Types
-------------
Cryptol types come in two kinds: numeric types (kind `#`) and value
types (kind `*`). While value types are inhabited by well-typed
Cryptol expressions, numeric types are only used as parameters to
other types; they have no inhabitants. In this implementation we
represent numeric types as values of the Haskell type `Nat'` of
natural numbers with infinity; value types are represented as values
of type `TValue`.
The value types of Cryptol, along with their Haskell representations,
are as follows:
| Cryptol type | Description | `TValue` representation |
|:------------------|:------------------|:----------------------------|
| `Bit` | booleans | `TVBit` |
| `Integer` | integers | `TVInteger` |
| `Z n` | integers modulo n | `TVIntMod n` |
| `Rational` | rationals | `TVRational` |
| `Float e p` | floating point | `TVFloat` |
| `Array` | arrays | `TVArray` |
| `[n]a` | finite lists | `TVSeq n a` |
| `[inf]a` | infinite lists | `TVStream a` |
| `(a, b, c)` | tuples | `TVTuple [a,b,c]` |
| `{x:a, y:b, z:c}` | records | `TVRec [(x,a),(y,b),(z,c)]` |
| `a -> b` | functions | `TVFun a b` |
We model each (closed) Cryptol value type `t` as a complete partial order (cpo)
*M*(`t`). The values of *M*(`t`) represent the _values_ present in the
type `t`; we distinguish these from the _computations_ at type `t`.
Operationally, the difference is that computations may raise errors or cause
nontermination when evaluated; however, values are already evaluated, and will
not cause errors or nontermination. Denotationally, we represent this
difference via a monad (in the style of Moggi) called *E*. As an
operation on CPOs, *E* adds a new bottom element representing
nontermination, and a collection of erroneous values representing
various runtime error conditions.
To each Cryptol expression `e : t` we assign a meaning
*M*(`e`) in *E*(*M*(`t`)); in particular, recursive Cryptol programs of
type `t` are modeled as least fixed points in *E*(*M*(`t`)). In other words,
this is a domain-theoretic denotational semantics. Note, we do not requre
CPOs defined via *M*(`t`) to have bottom elements, which is why we must take
fixpoints in *E*. We cannot directly represent values without bottom in Haskell,
so instead we are careful in this document only to write clearly-terminating
functions, unless they represent computations under *E*.
*M*(`Bit`) is a discrete cpo with values for `True`, `False`, which
we simply represent in Haskell as `Bool`.
Similarly, *M*(`Integer`) is a discrete cpo with values for integers,
which we model as Haskell's `Integer`. Likewise with the other
base types.
The value cpos for lists, tuples, and records are cartesian products
of _computations_. For example *M*(`(a,b)`) = *E*(*M*(`a`)) × *E*(*M*(`b`)).
The cpo ordering is pointwise. The trivial types `[0]t`,
`()` and `{}` denote single-element cpos. *M*(`a -> b`) is the
continuous function space *E*(*M*(`a`)) $\to$ *E*(*M*(`b`)).
Type schemas of the form `{a1 ... an} (p1 ... pk) => t` classify
polymorphic values in Cryptol. These are represented with the Haskell
type `Schema`. The meaning of a schema is cpo whose elements are
functions: For each valid instantiation `t1 ... tn` of the type
parameters `a1 ... an` that satisfies the constraints `p1 ... pk`, the
function returns a value in *E*(*M*(`t[t1/a1 ... tn/an]`)).
Computation Monad
------------------
This monad represents either an evaluated thing of type `a`
or an evaluation error. In the reference interpreter, only
things under this monad should potentially result in errors
or fail to terminate.
> -- | Computation monad for the reference evaluator.
> data E a = Value !a | Err EvalError
>
> instance Functor E where
> fmap f (Value x) = Value (f x)
> fmap _ (Err e) = Err e
> instance Applicative E where
> pure x = Value x
> Err e <*> _ = Err e
> Value _ <*> Err e = Err e
> Value f <*> Value x = Value (f x)
> instance Monad E where
> m >>= f =
> case m of
> Value x -> f x
> Err r -> Err r
>
> eitherToE :: Either EvalError a -> E a
> eitherToE (Left e) = Err e
> eitherToE (Right x) = pure x
Values
------
The Haskell code in this module defines the semantics of typed Cryptol
terms by providing an evaluator to an appropriate `Value` type.
> -- | Value type for the reference evaluator.
> data Value
> = VBit !Bool -- ^ @ Bit @ booleans
> | VInteger !Integer -- ^ @ Integer @ or @Z n@ integers
> | VRational !Rational -- ^ @ Rational @ rationals
> | VFloat !BF -- ^ Floating point numbers
> | VList Nat' [E Value] -- ^ @ [n]a @ finite or infinite lists
> | VTuple [E Value] -- ^ @ ( .. ) @ tuples
> | VRecord [(Ident, E Value)] -- ^ @ { .. } @ records
> | VFun (E Value -> E Value) -- ^ functions
> | VPoly (TValue -> E Value) -- ^ polymorphic values (kind *)
> | VNumPoly (Nat' -> E Value) -- ^ polymorphic values (kind #)
Operations on Values
--------------------
> -- | Destructor for @VBit@.
> fromVBit :: Value -> Bool
> fromVBit (VBit b) = b
> fromVBit _ = evalPanic "fromVBit" ["Expected a bit"]
>
> -- | Destructor for @VInteger@.
> fromVInteger :: Value -> Integer
> fromVInteger (VInteger i) = i
> fromVInteger _ = evalPanic "fromVInteger" ["Expected an integer"]
>
> -- | Destructor for @VRational@.
> fromVRational :: Value -> Rational
> fromVRational (VRational i) = i
> fromVRational _ = evalPanic "fromVRational" ["Expected a rational"]
>
> fromVFloat :: Value -> BigFloat
> fromVFloat = bfValue . fromVFloat'
>
> fromVFloat' :: Value -> BF
> fromVFloat' v =
> case v of
> VFloat f -> f
> _ -> evalPanic "fromVFloat" [ "Expected a floating point value." ]
>
> -- | Destructor for @VList@.
> fromVList :: Value -> [E Value]
> fromVList (VList _ vs) = vs
> fromVList _ = evalPanic "fromVList" ["Expected a list"]
>
> -- | Destructor for @VTuple@.
> fromVTuple :: Value -> [E Value]
> fromVTuple (VTuple vs) = vs
> fromVTuple _ = evalPanic "fromVTuple" ["Expected a tuple"]
>
> -- | Destructor for @VRecord@.
> fromVRecord :: Value -> [(Ident, E Value)]
> fromVRecord (VRecord fs) = fs
> fromVRecord _ = evalPanic "fromVRecord" ["Expected a record"]
>
> -- | Destructor for @VFun@.
> fromVFun :: Value -> (E Value -> E Value)
> fromVFun (VFun f) = f
> fromVFun _ = evalPanic "fromVFun" ["Expected a function"]
>
> -- | Look up a field in a record.
> lookupRecord :: Ident -> Value -> E Value
> lookupRecord f v =
> case lookup f (fromVRecord v) of
> Just val -> val
> Nothing -> evalPanic "lookupRecord" ["Malformed record"]
>
> -- | Polymorphic function values that expect a finite numeric type.
> vFinPoly :: (Integer -> E Value) -> Value
> vFinPoly f = VNumPoly g
> where
> g (Nat n) = f n
> g Inf = evalPanic "vFinPoly" ["Expected finite numeric type"]
Environments
------------
An evaluation environment keeps track of the values of term variables
and type variables that are in scope at any point.
> data Env = Env
> { envVars :: !(Map Name (E Value))
> , envTypes :: !TypeEnv
> }
>
> instance Semigroup Env where
> l <> r = Env
> { envVars = envVars l <> envVars r
> , envTypes = envTypes l <> envTypes r
> }
>
> instance Monoid Env where
> mempty = Env
> { envVars = mempty
> , envTypes = mempty
> }
> mappend l r = l <> r
>
> -- | Bind a variable in the evaluation environment.
> bindVar :: (Name, E Value) -> Env -> Env
> bindVar (n, val) env = env { envVars = Map.insert n val (envVars env) }
>
> -- | Bind a type variable of kind # or *.
> bindType :: TVar -> Either Nat' TValue -> Env -> Env
> bindType p ty env = env { envTypes = bindTypeVar p ty (envTypes env) }
Evaluation
==========
The meaning *M*(`expr`) of a Cryptol expression `expr` is defined by
recursion over its structure. For an expression that contains free
variables, the meaning also depends on the environment `env`, which
assigns values to those variables.
> evalExpr :: Env -- ^ Evaluation environment
> -> Expr -- ^ Expression to evaluate
> -> E Value
> evalExpr env expr =
> case expr of
>
> ELocated _ e -> evalExpr env e
>
> EList es _ty ->
> pure $ VList (Nat (genericLength es)) [ evalExpr env e | e <- es ]
>
> ETuple es ->
> pure $ VTuple [ evalExpr env e | e <- es ]
>
> ERec fields ->
> pure $ VRecord [ (f, evalExpr env e) | (f, e) <- canonicalFields fields ]
>
> ESel e sel ->
> evalSel sel =<< evalExpr env e
>
> ESet ty e sel v ->
> evalSet (evalValType (envTypes env) ty)
> (evalExpr env e) sel (evalExpr env v)
>
> EIf c t f ->
> condValue (fromVBit <$> evalExpr env c) (evalExpr env t) (evalExpr env f)
>
> EComp _n _ty e branches -> evalComp env e branches
>
> EVar n ->
> case Map.lookup n (envVars env) of
> Just val -> val
> Nothing ->
> evalPanic "evalExpr" ["var `" ++ show (pp n) ++ "` is not defined" ]
>
> ETAbs tv b ->
> case tpKind tv of
> KType -> pure $ VPoly $ \ty ->
> evalExpr (bindType (tpVar tv) (Right ty) env) b
> KNum -> pure $ VNumPoly $ \n ->
> evalExpr (bindType (tpVar tv) (Left n) env) b
> k -> evalPanic "evalExpr" ["Invalid kind on type abstraction", show k]
>
> ETApp e ty ->
> evalExpr env e >>= \case
> VPoly f -> f $! (evalValType (envTypes env) ty)
> VNumPoly f -> f $! (evalNumType (envTypes env) ty)
> _ -> evalPanic "evalExpr" ["Expected a polymorphic value"]
>
> EApp e1 e2 -> appFun (evalExpr env e1) (evalExpr env e2)
> EAbs n _ty b -> pure $ VFun (\v -> evalExpr (bindVar (n, v) env) b)
> EProofAbs _ e -> evalExpr env e
> EProofApp e -> evalExpr env e
> EWhere e dgs -> evalExpr (foldl evalDeclGroup env dgs) e
> appFun :: E Value -> E Value -> E Value
> appFun f v = f >>= \f' -> fromVFun f' v
Selectors
---------
Apply the the given selector form to the given value.
Note that record selectors work uniformly on both record
types and on newtypes.
> evalSel :: Selector -> Value -> E Value
> evalSel sel val =
> case sel of
> TupleSel n _ -> tupleSel n val
> RecordSel n _ -> recordSel n val
> ListSel n _ -> listSel n val
> where
> tupleSel n v =
> case v of
> VTuple vs -> vs !! n
> _ -> evalPanic "evalSel"
> ["Unexpected value in tuple selection."]
> recordSel n v =
> case v of
> VRecord _ -> lookupRecord n v
> _ -> evalPanic "evalSel"
> ["Unexpected value in record selection."]
> listSel n v =
> case v of
> VList _ vs -> vs !! n
> _ -> evalPanic "evalSel"
> ["Unexpected value in list selection."]
Update the given value using the given selector and new value.
Note that record selectors work uniformly on both record
types and on newtypes.
> evalSet :: TValue -> E Value -> Selector -> E Value -> E Value
> evalSet tyv val sel fval =
> case (tyv, sel) of
> (TVTuple ts, TupleSel n _) -> updTupleAt ts n
> (TVRec fs, RecordSel n _) -> updRecAt fs n
> (TVNewtype _ _ fs, RecordSel n _) -> updRecAt fs n
> (TVSeq len _, ListSel n _) -> updSeqAt len n
> (_, _) -> evalPanic "evalSet" ["type/selector mismatch", show tyv, show sel]
> where
> updTupleAt ts n =
> pure $ VTuple
> [ if i == n then fval else
> do vs <- fromVTuple <$> val
> genericIndex vs i
> | (i,_t) <- zip [0 ..] ts
> ]
>
> updRecAt fs n =
> pure $ VRecord
> [ (f, if f == n then fval else lookupRecord f =<< val)
> | (f, _t) <- canonicalFields fs
> ]
>
> updSeqAt len n =
> pure $ generateV (Nat len) $ \i ->
> if i == toInteger n then fval else
> do vs <- fromVList <$> val
> indexFront (Nat len) vs i
Conditionals
------------
Conditionals are explicitly lazy: Run-time errors in an untaken branch
are ignored.
> condValue :: E Bool -> E Value -> E Value -> E Value
> condValue c l r = c >>= \b -> if b then l else r
List Comprehensions
-------------------
Cryptol list comprehensions consist of one or more parallel branches;
each branch has one or more matches that bind values to variables.
The result of evaluating a match in an initial environment is a list
of extended environments. Each new environment binds the same single
variable to a different element of the match's list.
> evalMatch :: Env -> Match -> [Env]
> evalMatch env m =
> case m of
> Let d -> [ bindVar (evalDecl env d) env ]
> From nm len _ty expr -> [ bindVar (nm, get i) env | i <- idxs ]
> where
> get i =
> do v <- evalExpr env expr
> genericIndex (fromVList v) i
>
> idxs :: [Integer]
> idxs =
> case evalNumType (envTypes env) len of
> Inf -> [0 ..]
> Nat n -> [0 .. n-1]
> lenMatch :: Env -> Match -> Nat'
> lenMatch env m =
> case m of
> Let _ -> Nat 1
> From _ len _ _ -> evalNumType (envTypes env) len
The result of of evaluating a branch in an initial environment is a
list of extended environments, each of which extends the initial
environment with the same set of new variables. The length of the list
is equal to the product of the lengths of the lists in the matches.
> evalBranch :: Env -> [Match] -> [Env]
> evalBranch env [] = [env]
> evalBranch env (match : matches) =
> [ env'' | env' <- evalMatch env match
> , env'' <- evalBranch env' matches ]
> lenBranch :: Env -> [Match] -> Nat'
> lenBranch _env [] = Nat 1
> lenBranch env (match : matches) =
> nMul (lenMatch env match) (lenBranch env matches)
The head expression of the comprehension can refer to any variable
bound in any of the parallel branches. So to evaluate the
comprehension, we zip and merge together the lists of extended
environments from each branch. The head expression is then evaluated
separately in each merged environment. The length of the resulting
list is equal to the minimum length over all parallel branches.
> evalComp :: Env -- ^ Starting evaluation environment
> -> Expr -- ^ Head expression of the comprehension
> -> [[Match]] -- ^ List of parallel comprehension branches
> -> E Value
> evalComp env expr branches =
> pure $ VList len [ evalExpr e expr | e <- envs ]
> where
> -- Generate a new environment for each iteration of each
> -- parallel branch.
> benvs :: [[Env]]
> benvs = map (evalBranch env) branches
>
> -- Zip together the lists of environments from each branch,
> -- producing a list of merged environments. Longer branches get
> -- truncated to the length of the shortest branch.
> envs :: [Env]
> envs = foldr1 (zipWith mappend) benvs
>
> len :: Nat'
> len = foldr1 nMin (map (lenBranch env) branches)
Declarations
------------
Function `evalDeclGroup` extends the given evaluation environment with
the result of evaluating the given declaration group. In the case of a
recursive declaration group, we tie the recursive knot by evaluating
each declaration in the extended environment `env'` that includes all
the new bindings.
> evalDeclGroup :: Env -> DeclGroup -> Env
> evalDeclGroup env dg = do
> case dg of
> NonRecursive d ->
> bindVar (evalDecl env d) env
> Recursive ds ->
> let env' = foldr bindVar env bindings
> bindings = map (evalDecl env') ds
> in env'
>
> evalDecl :: Env -> Decl -> (Name, E Value)
> evalDecl env d =
> case dDefinition d of
> DPrim -> (dName d, pure (evalPrim (dName d)))
> DExpr e -> (dName d, evalExpr env e)
>
Newtypes
--------
At runtime, newtypes values are represented in exactly
the same way as records. The constructor function for
newtypes is thus basically just an identity function
that consumes and ignores its type arguments.
> evalNewtypeDecl :: Env -> Newtype -> Env
> evalNewtypeDecl env nt = bindVar (ntName nt, pure val) env
> where
> val = foldr tabs con (ntParams nt)
> con = VFun (\x -> x)
> tabs tp body =
> case tpKind tp of
> KType -> VPoly (\_ -> pure body)
> KNum -> VNumPoly (\_ -> pure body)
> k -> evalPanic "evalNewtypeDecl" ["illegal newtype parameter kind", show k]
Primitives
==========
To evaluate a primitive, we look up its implementation by name in a table.
> evalPrim :: Name -> Value
> evalPrim n
> | Just i <- asPrim n, Just v <- Map.lookup i primTable = v
> | otherwise = evalPanic "evalPrim" ["Unimplemented primitive", show (pp n)]
Cryptol primitives fall into several groups, mostly delineated
by corresponding type classes:
* Literals: `True`, `False`, `number`, `ratio`
* Zero: zero
* Logic: `&&`, `||`, `^`, `complement`
* Ring: `+`, `-`, `*`, `negate`, `fromInteger`
* Integral: `/`, `%`, `^^`, `toInteger`
* Bitvector: `/$` `%$`, `lg2`, `<=$`
* Comparison: `<`, `>`, `<=`, `>=`, `==`, `!=`
* Sequences: `#`, `join`, `split`, `take`, `drop`, `reverse`, `transpose`
* Shifting: `<<`, `>>`, `<<<`, `>>>`
* Indexing: `@`, `@@`, `!`, `!!`, `update`, `updateEnd`
* Enumerations: `fromTo`, `fromThenTo`, `fromToLessThan`, `fromToBy`,
`fromToByLessThan`, `fromToDownBy`, `fromToDownByGreaterThan`,
`infFrom`, `infFromThen`
* Polynomials: `pmult`, `pdiv`, `pmod`
* Miscellaneous: `error`, `random`, `trace`
> primTable :: Map PrimIdent Value
> primTable = Map.unions
> [ cryptolPrimTable
> , floatPrimTable
> ]
> infixr 0 ~>
> (~>) :: String -> a -> (String,a)
> nm ~> v = (nm,v)
> cryptolPrimTable :: Map PrimIdent Value
> cryptolPrimTable = Map.fromList $ map (\(n, v) -> (prelPrim (T.pack n), v))
>
> -- Literals
> [ "True" ~> VBit True
> , "False" ~> VBit False
> , "number" ~> vFinPoly $ \val -> pure $
> VPoly $ \a ->
> literal val a
> , "fraction" ~> vFinPoly \top -> pure $
> vFinPoly \bot -> pure $
> vFinPoly \rnd -> pure $
> VPoly \a -> fraction top bot rnd a
> -- Zero
> , "zero" ~> VPoly (pure . zero)
>
> -- Logic (bitwise)
> , "&&" ~> binary (logicBinary (&&))
> , "||" ~> binary (logicBinary (||))
> , "^" ~> binary (logicBinary (/=))
> , "complement" ~> unary (logicUnary not)
>
> -- Ring
> , "+" ~> binary (ringBinary
> (\x y -> pure (x + y))
> (\x y -> pure (x + y))
> (fpBin FP.bfAdd fpImplicitRound)
> )
> , "-" ~> binary (ringBinary
> (\x y -> pure (x - y))
> (\x y -> pure (x - y))
> (fpBin FP.bfSub fpImplicitRound)
> )
> , "*" ~> binary ringMul
> , "negate" ~> unary (ringUnary (\x -> pure (- x))
> (\x -> pure (- x))
> (\_ _ x -> pure (FP.bfNeg x)))
> , "fromInteger"~> VPoly $ \a -> pure $
> VFun $ \x ->
> ringNullary (fromVInteger <$> x)
> (fromInteger . fromVInteger <$> x)
> (\e p -> fpFromInteger e p . fromVInteger <$> x)
> a
>
> -- Integral
> , "toInteger" ~> VPoly $ \a -> pure $
> VFun $ \x ->
> VInteger <$> cryToInteger a x
> , "/" ~> binary (integralBinary divWrap)
> , "%" ~> binary (integralBinary modWrap)
> , "^^" ~> VPoly $ \aty -> pure $
> VPoly $ \ety -> pure $
> VFun $ \a -> pure $
> VFun $ \e ->
> ringExp aty a =<< cryToInteger ety e
>
> -- Field
> , "/." ~> binary (fieldBinary ratDiv zDiv
> (fpBin FP.bfDiv fpImplicitRound)
> )
>
> , "recip" ~> unary (fieldUnary ratRecip zRecip fpRecip)
>
> -- Round
> , "floor" ~> unary (roundUnary floor
> (eitherToE . FP.floatToInteger "floor" FP.ToNegInf))
>
> , "ceiling" ~> unary (roundUnary ceiling
> (eitherToE . FP.floatToInteger "ceiling" FP.ToPosInf))
>
> , "trunc" ~> unary (roundUnary truncate
> (eitherToE . FP.floatToInteger "trunc" FP.ToZero))
>
> , "roundAway" ~> unary (roundUnary roundAwayRat
> (eitherToE . FP.floatToInteger "roundAway" FP.Away))
>
> , "roundToEven"~> unary (roundUnary round
> (eitherToE . FP.floatToInteger "roundToEven" FP.NearEven))
>
>
> -- Comparison
> , "<" ~> binary (cmpOrder (\o -> o == LT))
> , ">" ~> binary (cmpOrder (\o -> o == GT))
> , "<=" ~> binary (cmpOrder (\o -> o /= GT))
> , ">=" ~> binary (cmpOrder (\o -> o /= LT))
> , "==" ~> binary (cmpOrder (\o -> o == EQ))
> , "!=" ~> binary (cmpOrder (\o -> o /= EQ))
> , "<$" ~> binary signedLessThan
>
> -- Bitvector
> , "/$" ~> vFinPoly $ \n -> pure $
> VFun $ \l -> pure $
> VFun $ \r ->
> vWord n <$> appOp2 divWrap
> (fromSignedVWord =<< l)
> (fromSignedVWord =<< r)
> , "%$" ~> vFinPoly $ \n -> pure $
> VFun $ \l -> pure $
> VFun $ \r ->
> vWord n <$> appOp2 modWrap
> (fromSignedVWord =<< l)
> (fromSignedVWord =<< r)
> , ">>$" ~> signedShiftRV
> , "lg2" ~> vFinPoly $ \n -> pure $
> VFun $ \v ->
> vWord n <$> appOp1 lg2Wrap (fromVWord =<< v)
> -- Rational
> , "ratio" ~> VFun $ \l -> pure $
> VFun $ \r ->
> VRational <$> appOp2 ratioOp
> (fromVInteger <$> l)
> (fromVInteger <$> r)
>
> -- Z n
> , "fromZ" ~> vFinPoly $ \n -> pure $
> VFun $ \x ->
> VInteger . flip mod n . fromVInteger <$> x
>
> -- Sequences
> , "#" ~> vFinPoly $ \front -> pure $
> VNumPoly $ \back -> pure $
> VPoly $ \_elty -> pure $
> VFun $ \l -> pure $
> VFun $ \r ->
> pure $ generateV (nAdd (Nat front) back) $ \i ->
> if i < front then
> do l' <- fromVList <$> l
> indexFront (Nat front) l' i
> else
> do r' <- fromVList <$> r
> indexFront back r' (i - front)
>
> , "join" ~> VNumPoly $ \parts -> pure $
> vFinPoly $ \each -> pure $
> VPoly $ \_a -> pure $
> VFun $ \v ->
> pure $ generateV (nMul parts (Nat each)) $ \i ->
> do let (q,r) = divMod i each
> xss <- fromVList <$> v
> xs <- fromVList <$> indexFront parts xss q
> indexFront (Nat each) xs r
>
> , "split" ~> VNumPoly $ \parts -> pure $
> vFinPoly $ \each -> pure $
> VPoly $ \_a -> pure $
> VFun $ \val ->
> pure $ generateV parts $ \i ->
> pure $ generateV (Nat each) $ \j ->
> do vs <- fromVList <$> val
> indexFront (nMul parts (Nat each)) vs (i * each + j)
>
> , "take" ~> VNumPoly $ \front -> pure $
> VNumPoly $ \back -> pure $
> VPoly $ \_a -> pure $
> VFun $ \v ->
> pure $ generateV front $ \i ->
> do vs <- fromVList <$> v
> indexFront (nAdd front back) vs i
>
> , "drop" ~> vFinPoly $ \front -> pure $
> VNumPoly $ \back -> pure $
> VPoly $ \_a -> pure $
> VFun $ \v ->
> pure $ generateV back $ \i ->
> do vs <- fromVList <$> v
> indexFront (nAdd (Nat front) back) vs (front+i)
>
> , "reverse" ~> vFinPoly $ \n -> pure $
> VPoly $ \_a -> pure $
> VFun $ \v ->
> pure $ generateV (Nat n) $ \i ->
> do vs <- fromVList <$> v
> indexBack (Nat n) vs i
>
> , "transpose" ~> VNumPoly $ \rows -> pure $
> VNumPoly $ \cols -> pure $
> VPoly $ \_a -> pure $
> VFun $ \val ->
> pure $ generateV cols $ \c ->
> pure $ generateV rows $ \r ->
> do xss <- fromVList <$> val
> xs <- fromVList <$> indexFront rows xss r
> indexFront cols xs c
>
> -- Shifting:
> , "<<" ~> shiftV shiftLV
> , ">>" ~> shiftV shiftRV
> , "<<<" ~> rotateV rotateLV
> , ">>>" ~> rotateV rotateRV
>
> -- Indexing:
> , "@" ~> indexPrimOne indexFront
> , "!" ~> indexPrimOne indexBack
> , "update" ~> updatePrim updateFront
> , "updateEnd" ~> updatePrim updateBack
>
> -- Enumerations
> , "fromTo" ~> vFinPoly $ \first -> pure $
> vFinPoly $ \lst -> pure $
> VPoly $ \ty -> pure $
> let f i = literal i ty in
> VList (Nat (1 + lst - first)) (map f [first .. lst])
>
> , "fromToLessThan" ~>
> vFinPoly $ \first -> pure $
> VNumPoly $ \bound -> pure $
> VPoly $ \ty -> pure $
> let f i = literal i ty in
> case bound of
> Inf -> VList Inf (map f [first ..])
> Nat bound' ->
> let len = bound' - first in
> VList (Nat len) (map f (genericTake len [first ..]))
>
> , "fromToBy" ~> vFinPoly $ \first -> pure $
> vFinPoly $ \lst -> pure $
> vFinPoly $ \stride -> pure $
> VPoly $ \ty -> pure $
> let f i = literal i ty in
> let vs = [ f (first + i*stride) | i <- [0..] ] in
> let len = 1 + ((lst-first) `div` stride) in
> VList (Nat len) (genericTake len vs)
>
> , "fromToByLessThan" ~>
> vFinPoly $ \first -> pure $
> VNumPoly $ \bound -> pure $
> vFinPoly $ \stride -> pure $
> VPoly $ \ty -> pure $
> let f i = literal i ty in
> let vs = [ f (first + i*stride) | i <- [0..] ] in
> case bound of
> Inf -> VList Inf vs
> Nat bound' ->
> let len = (bound'-first+stride-1) `div` stride in
> VList (Nat len) (genericTake len vs)
>
> , "fromToDownBy" ~>
> vFinPoly $ \first -> pure $
> vFinPoly $ \lst -> pure $
> vFinPoly $ \stride -> pure $
> VPoly $ \ty -> pure $
> let f i = literal i ty in
> let vs = [ f (first - i*stride) | i <- [0..] ] in
> let len = 1 + ((first-lst) `div` stride) in
> VList (Nat len) (genericTake len vs)
>
> , "fromToDownByGreaterThan" ~>
> vFinPoly $ \first -> pure $
> vFinPoly $ \lst -> pure $
> vFinPoly $ \stride -> pure $
> VPoly $ \ty -> pure $
> let f i = literal i ty in
> let vs = [ f (first - i*stride) | i <- [0..] ] in
> let len = (first-lst+stride-1) `div` stride in
> VList (Nat len) (genericTake len vs)
>
> , "fromThenTo" ~> vFinPoly $ \first -> pure $
> vFinPoly $ \next -> pure $
> vFinPoly $ \_lst -> pure $
> VPoly $ \ty -> pure $
> vFinPoly $ \len -> pure $
> let f i = literal i ty in
> VList (Nat len)
> (map f (genericTake len [first, next ..]))
>
> , "infFrom" ~> VPoly $ \ty -> pure $
> VFun $ \first ->
> do x <- cryToInteger ty first
> let f i = literal (x + i) ty
> pure $ VList Inf (map f [0 ..])
>
> , "infFromThen"~> VPoly $ \ty -> pure $
> VFun $ \first -> pure $
> VFun $ \next ->
> do x <- cryToInteger ty first
> y <- cryToInteger ty next
> let diff = y - x
> f i = literal (x + diff * i) ty
> pure $ VList Inf (map f [0 ..])
>
> -- Miscellaneous:
> , "parmap" ~> VPoly $ \_a -> pure $
> VPoly $ \_b -> pure $
> VNumPoly $ \n -> pure $
> VFun $ \f -> pure $
> VFun $ \xs ->
> do f' <- fromVFun <$> f
> xs' <- fromVList <$> xs
> -- Note: the reference implementation simply
> -- executes parmap sequentially
> pure $ VList n (map f' xs')
>
> , "error" ~> VPoly $ \_a -> pure $
> VNumPoly $ \_ -> pure $
> VFun $ \s ->
> do msg <- evalString s
> cryError (UserError msg)
>
> , "random" ~> VPoly $ \_a -> pure $
> VFun $ \_seed -> cryError (UserError "random: unimplemented")
>
> , "trace" ~> VNumPoly $ \_n -> pure $
> VPoly $ \_a -> pure $
> VPoly $ \_b -> pure $
> VFun $ \s -> pure $
> VFun $ \x -> pure $
> VFun $ \y ->
> do _ <- evalString s -- evaluate and ignore s
> _ <- x -- evaluate and ignore x
> y
> ]
>
>
> evalString :: E Value -> E String
> evalString v =
> do cs <- fromVList <$> v
> ws <- mapM (fromVWord =<<) cs
> pure (map (toEnum . fromInteger) ws)
>
> unary :: (TValue -> E Value -> E Value) -> Value
> unary f = VPoly $ \ty -> pure $
> VFun $ \x -> f ty x
>
> binary :: (TValue -> E Value -> E Value -> E Value) -> Value
> binary f = VPoly $ \ty -> pure $
> VFun $ \x -> pure $
> VFun $ \y -> f ty x y
>
> appOp1 :: (a -> E b) -> E a -> E b
> appOp1 f x =
> do x' <- x
> f x'
>
> appOp2 :: (a -> b -> E c) -> E a -> E b -> E c
> appOp2 f x y =
> do x' <- x
> y' <- y
> f x' y'
Word operations
---------------
Many Cryptol primitives take numeric arguments in the form of
bitvectors. For such operations, any output bit that depends on the
numeric value is strict in *all* bits of the numeric argument. This is
implemented in function `fromVWord`, which converts a value from a
big-endian binary format to an integer. The result is an evaluation
error if any of the input bits contain an evaluation error.
> fromVWord :: Value -> E Integer
> fromVWord v = bitsToInteger <$> traverse (fmap fromVBit) (fromVList v)
>
> -- | Convert a list of booleans in big-endian format to an integer.
> bitsToInteger :: [Bool] -> Integer
> bitsToInteger bs = foldl f 0 bs
> where f x b = if b then 2 * x + 1 else 2 * x
> fromSignedVWord :: Value -> E Integer
> fromSignedVWord v = signedBitsToInteger <$> traverse (fmap fromVBit) (fromVList v)
>
> -- | Convert a list of booleans in signed big-endian format to an integer.
> signedBitsToInteger :: [Bool] -> Integer
> signedBitsToInteger [] =
> evalPanic "signedBitsToInteger" ["Bitvector has zero length"]
> signedBitsToInteger (b0 : bs) = foldl f (if b0 then -1 else 0) bs
> where f x b = if b then 2 * x + 1 else 2 * x
Function `vWord` converts an integer back to the big-endian bitvector
representation.
> vWord :: Integer -> Integer -> Value
> vWord w e
> | w > toInteger (maxBound :: Int) =
> evalPanic "vWord" ["Word length too large", show w]
> | otherwise =
> VList (Nat w) [ mkBit i | i <- [w-1, w-2 .. 0 ] ]
> where
> mkBit i = pure (VBit (testBit e (fromInteger i)))
Errors
------
> cryError :: EvalError -> E a
> cryError e = Err e
Zero
----
The `Zero` class has a single method `zero` which computes
a zero value for all the built-in types for Cryptol.
For bits, bitvectors and the base numeric types, this
returns the obvious 0 representation. For sequences, records,
and tuples, the zero method operates pointwise the underlying types.
For functions, `zero` returns the constant function that returns
`zero` in the codomain.
> zero :: TValue -> Value
> zero TVBit = VBit False
> zero TVInteger = VInteger 0
> zero TVIntMod{} = VInteger 0
> zero TVRational = VRational 0
> zero (TVFloat e p) = VFloat (fpToBF e p FP.bfPosZero)
> zero TVArray{} = evalPanic "zero" ["Array type not in `Zero`"]
> zero (TVSeq n ety) = VList (Nat n) (genericReplicate n (pure (zero ety)))
> zero (TVStream ety) = VList Inf (repeat (pure (zero ety)))
> zero (TVTuple tys) = VTuple (map (pure . zero) tys)
> zero (TVRec fields) = VRecord [ (f, pure (zero fty))
> | (f, fty) <- canonicalFields fields ]
> zero (TVFun _ bty) = VFun (\_ -> pure (zero bty))
> zero (TVAbstract{}) = evalPanic "zero" ["Abstract type not in `Zero`"]
> zero (TVNewtype{}) = evalPanic "zero" ["Newtype not in `Zero`"]
Literals