@@ -411,17 +411,22 @@ with
411
411
show : Int256 -> String := toInt >> Show.show;
412
412
};
413
413
414
+ twosComplement (n : UInt256) : Int256 :=
415
+ let
416
+ w := UInt256.toNat n;
417
+ in if
418
+ | w < threshold := privateMk (Int.fromNat w)
419
+ | else :=
420
+ let
421
+ subs : Nat := mod w threshold + 1;
422
+ in privateMk (Int.negSuc (Nat.sub threshold subs));
423
+
414
424
instance
415
425
FromBytes-Int256 : FromBytes Int256 :=
416
426
FromBytes.mk
417
427
do {
418
- w <- UInt256.toNat <$> fromBytes;
419
- if
420
- | w < threshold := pure (privateMk (Int.fromNat w))
421
- | else :=
422
- let
423
- subs : Nat := mod w threshold + 1;
424
- in pure (privateMk (Int.negSuc (Nat.sub threshold subs)));
428
+ w <- fromBytes;
429
+ pure (twosComplement w);
425
430
};
426
431
427
432
instance
@@ -477,23 +482,13 @@ with
477
482
FromBytes-Int32 : FromBytes Int32 :=
478
483
FromBytes.mk
479
484
do {
480
- w <- UInt32.toNat <$> fromBytes;
481
- if
482
- | w < pow 2 31 := pure (privateMk (Int.fromNat w))
483
- | else :=
484
- let
485
- subs : Nat := mod w (pow 2 31) + 1;
486
- in pure (privateMk (Int.negSuc (Nat.sub (pow 2 31) subs)));
485
+ w <- fromBytes;
486
+ pure (privateMk (Int256.toInt (Int256.twosComplement w)));
487
487
};
488
488
489
489
instance
490
490
ToBytes-Int32 : ToBytes Int32 :=
491
- ToBytes.mk
492
- \{i :=
493
- case toInt i of
494
- | Int.ofNat n := toBytes {UInt32} (fromNat n)
495
- | Int.negSuc n :=
496
- toBytes {UInt32} (fromNat (sub (pow 2 32) (n + 1)))};
491
+ ToBytes.mk \{(privateMk i) := ToBytes.toBytes {Int256} (Int256.fromInt i)};
497
492
498
493
instance
499
494
HasEvmSize-Int32 : HasEvmSize Int32 := HasEvmSize.evmUInt;
@@ -627,121 +622,3 @@ tupleSplit (l : List EvmSize) : BytesConsumer (List (List Byte)) :=
627
622
};
628
623
};
629
624
in go [] l;
630
-
631
- {-- In order to define ;ToBytes; and ;FromBytes; instances for a
632
- tuple, we need to follow some mechanical steps.
633
- This module provides a concrete example. See the comments in the instances
634
- declarations below.
635
- --}
636
- module TupleUsageExample;
637
-
638
- type Example : Type :=
639
- mk@{
640
- word : UInt32;
641
- bytearray : ByteArray;
642
- int : Int256;
643
- int32 : Int32;
644
- };
645
-
646
- deriving instance
647
- Eq-Example : Eq Example;
648
-
649
- {-- To define the ;ToBytes; instance we must create an ;EvmTuple; with the fields
650
- of the record given in order. Then we use the ;ToBytes; instance of the ;EvmTuple;
651
- as shown below.
652
- Note that each of the fields must be an instance of ;ToBytes; and ;HasEvmSize;.
653
- --}
654
- instance
655
- ToBytes-Example : ToBytes Example :=
656
- ToBytes.mk@{
657
- toBytes (e : Example) : BytesBuilder Unit :=
658
- do {
659
- let
660
- tup : EvmTuple :=
661
- Example.word e
662
- ::: Example.bytearray e
663
- ::: Example.int e
664
- ::: Example.int32 e
665
- ::: EvmTuple.nil;
666
- in
667
- ToBytes.toBytes tup;
668
- };
669
- };
670
-
671
- {-- To define the ;FromBytes; instance we must follow these steps:
672
- 1. call `l <- tupleSplit sizes`, where `sizes` is a list of the ;EvmSize; of
673
- the type of each field.
674
- 2. case on `l`. `l` will exactly `n` elements, where `n` is the number
675
- of fields with a type `T` such that `evmSize T` is ;EvmSize.static;
676
- 3. For each element `s` of `l`, we call:
677
- `fieldName <- BytesConsumer.local FromBytes.fromBytes s`
678
- 4. Then, for each field `f` with a dynamic ;EvmSize;, we call:
679
- `f <- FromBytes.fromBytes`
680
-
681
- For a concrete example, see the code below:
682
- --}
683
- instance
684
- FromBytes-Example : FromBytes Example :=
685
- FromBytes.mk@{
686
- fromBytes : BytesConsumer Example :=
687
- do {
688
- l <- tupleSplit
689
- [evmSize UInt32; evmSize ByteArray; evmSize Int256; evmSize Int32];
690
- case l of {
691
- | [sword; sint; sint32] :=
692
- do {
693
- -- static
694
- word <- BytesConsumer.local FromBytes.fromBytes sword;
695
- int <- BytesConsumer.local FromBytes.fromBytes sint;
696
- int32 <- BytesConsumer.local FromBytes.fromBytes sint32;
697
- -- dynamic
698
- bytearray <- FromBytes.fromBytes;
699
- pure
700
- Example.mk@{
701
- word;
702
- bytearray;
703
- int;
704
- int32;
705
- };
706
- }
707
- | _ := failwith "FromBytes-Example wrong number of static arguments"
708
- };
709
- };
710
- };
711
-
712
- instance
713
- Show-Example : Show Example :=
714
- Show.mk@{
715
- show (e : Example) : String :=
716
- Show.show (Example.word e)
717
- ++str ", "
718
- ++str Show.show (Example.bytearray e)
719
- ++str ", "
720
- ++str Show.show (Example.int e)
721
- ++str ", "
722
- ++str Show.show (Example.int32 e);
723
- };
724
-
725
- main : _ :=
726
- let
727
- n : List Byte := [3; 4; 5];
728
- b : ByteArray := ByteArray.mk n;
729
- i : Int256 := Int256.fromInt -88888888888888;
730
- i' : Int32 := Int32.fromInt -2147483647;
731
- example : Example :=
732
- Example.mk@{
733
- word := UInt32.fromNat (sub (pow 256 4) 1);
734
- bytearray := b;
735
- int := i;
736
- int32 := i';
737
- };
738
- encodedExample : ByteArray := toByteArray example;
739
- resDecodedExample : Result BytesConsumer.ConsumerError Example :=
740
- fromByteArray {Example} encodedExample;
741
- in trace (show example)
742
- >-> trace (show encodedExample)
743
- >-> case resDecodedExample of {
744
- | error err := false
745
- | ok decodedExample := decodedExample == example
746
- };
747
- end;
0 commit comments