-
+ 98EAA2028C09D5ABFDBEB11C8665906E67392BD4E25CD0434565D0E350A9211EEDB31EE4327793BA9678722C15868C249E6CEAA06616F9CE27918375EE6BD69Affa/libffa/ffa.ads(0 . 0)(1 . 277)
792 ------------------------------------------------------------------------------
793 ------------------------------------------------------------------------------
794 -- This file is part of 'Finite Field Arithmetic', aka 'FFA'. --
795 -- --
796 -- (C) 2018 Stanislav Datskovskiy ( www.loper-os.org ) --
797 -- http://wot.deedbot.org/17215D118B7239507FAFED98B98228A001ABFFC7.html --
798 -- --
799 -- You do not have, nor can you ever acquire the right to use, copy or --
800 -- distribute this software ; Should you use this software for any purpose, --
801 -- or copy and distribute it to anyone or in any manner, you are breaking --
802 -- the laws of whatever soi-disant jurisdiction, and you promise to --
803 -- continue doing so for the indefinite future. In any case, please --
804 -- always : read and understand any software ; verify any PGP signatures --
805 -- that you use - for any purpose. --
806 -- --
807 -- See also http://trilema.com/2015/a-new-software-licensing-paradigm . --
808 ------------------------------------------------------------------------------
809 ------------------------------------------------------------------------------
810
811 with Words; use Words;
812 with FZ_Type; use FZ_Type;
813
814 with W_Pred;
815
816 with FZ_Lim;
817 with FZ_Basic;
818 with FZ_IO;
819 with FZ_Cmp;
820 with FZ_Pred;
821 with FZ_BitOp;
822 with FZ_Divis;
823 with FZ_ModEx;
824
825
826 -- FFA Exports
827 package FFA is
828
829 pragma Pure;
830
831 ----------------------------------------------------------------------------
832 --- Fundamental Types and Sizes
833 ----------------------------------------------------------------------------
834
835 subtype Word is Words.Word;
836 subtype WBool is Words.WBool;
837
838 subtype Nibble is Words.Nibble;
839
840 subtype FZ is FZ_Type.FZ;
841 subtype Indices is FZ_Type.Indices;
842
843 subtype Char_Count is FZ_IO.Char_Count;
844
845 Bitness : Positive renames Words.Bitness;
846
847 ----------------------------------------------------------------------------
848 --- Word Predicates
849 ----------------------------------------------------------------------------
850
851 -- Return 1 if N is equal to 0; otherwise return 0.
852 function FFA_Word_ZeroP(N : in Word) return WBool
853 renames W_Pred.W_ZeroP;
854
855 -- Return 1 if N is unequal to 0; otherwise return 0.
856 function FFA_Word_NZeroP(N : in Word) return WBool
857 renames W_Pred.W_NZeroP;
858
859 -- Return WBool-complement of N.
860 function FFA_Word_Not(N : in WBool) return WBool
861 renames W_Pred.W_Not;
862
863 -- Return 1 if N is odd; otherwise return 0.
864 function FFA_Word_OddP(N : in Word) return WBool
865 renames W_Pred.W_OddP;
866
867 -- Return 1 if A is equal to B ; otherwise return 0.
868 function FFA_Word_EqP(A : in Word; B : in Word) return WBool
869 renames W_Pred.W_EqP;
870
871 ----------------------------------------------------------------------------
872 --- FZ Limits
873 ----------------------------------------------------------------------------
874
875 FFA_Validity_Rule_Doc : String renames FZ_Lim.FZ_Validity_Rule_Doc;
876
877 -- Determine if a proposed FFA Bitness is valid.
878 function FFA_FZ_Valid_Bitness_P(B : in Positive) return Boolean
879 renames FZ_Lim.FZ_Valid_Bitness_P;
880
881 ----------------------------------------------------------------------------
882 --- FZ Basics
883 ----------------------------------------------------------------------------
884
885 -- Determine the Bitness of N
886 function FFA_FZ_Bitness(N : in FZ) return Bit_Count
887 renames FZ_Basic.FZ_Bitness;
888
889 -- N := 0
890 procedure FFA_FZ_Clear(N : out FZ)
891 renames FZ_Basic.FZ_Clear;
892
893 -- Set given FZ to a given truth value
894 procedure FFA_WBool_To_FZ(V : in WBool; N : out FZ)
895 renames FZ_Basic.WBool_To_FZ;
896
897 -- First Word of N := Source
898 procedure FFA_FZ_Set_Head(N : out FZ; Source : in Word)
899 renames FZ_Basic.FZ_Set_Head;
900
901 -- First Word of N
902 function FFA_FZ_Get_Head(N : in FZ) return Word
903 renames FZ_Basic.FZ_Get_Head;
904
905 -- Exchange X and Y
906 procedure FFA_FZ_Swap(X : in out FZ; Y : in out FZ)
907 with Pre => X'Length = Y'Length;
908
909 -- Constant-time MUX: Sel = 0: Result := X; Sel = 1: Result := Y
910 procedure FFA_FZ_Mux(X : in FZ; Y : in FZ; Result : out FZ; Sel : in WBool)
911 with Pre => X'Length = Y'Length and X'Length = Result'Length;
912
913 ----------------------------------------------------------------------------
914 --- FZ IO Operations
915 ----------------------------------------------------------------------------
916
917 -- Expand FZ N by nibble D, and determine whether this operation overflowed
918 procedure FFA_FZ_Insert_Bottom_Nibble(N : in out FZ;
919 D : in Nibble;
920 Overflow : out WBool)
921 renames FZ_IO.FZ_Insert_Bottom_Nibble;
922
923 -- Determine the number of ASCII characters required to represent N
924 function FFA_FZ_ASCII_Length(N : in FZ) return Char_Count
925 renames FZ_IO.FZ_ASCII_Length;
926
927 -- Write an ASCII hex representation of N into existing string buffer S
928 procedure FFA_FZ_To_Hex_String(N : in FZ; S : out String)
929 renames FZ_IO.FZ_To_Hex_String;
930
931 ----------------------------------------------------------------------------
932 --- Comparison Predicate Operations on FZ
933 ----------------------------------------------------------------------------
934
935 -- 1 iff X == Y (branch-free); else 0
936 function FFA_FZ_EqP(X : in FZ; Y: in FZ) return WBool
937 renames FZ_Cmp.FZ_EqP;
938
939 -- 1 iff X < Y (branch-free); else 0
940 function FFA_FZ_LessThanP(X : in FZ; Y : in FZ) return WBool
941 renames FZ_Cmp.FZ_LessThanP;
942
943 -- 1 iff X > Y (branch-free); else 0
944 function FFA_FZ_GreaterThanP(X : in FZ; Y : in FZ) return WBool
945 renames FZ_Cmp.FZ_GreaterThanP;
946
947 ----------------------------------------------------------------------------
948 --- Fundamental Predicate Operations on FZ
949 ----------------------------------------------------------------------------
950
951 -- 1 iff N == 0 (branch-free); else 0
952 function FFA_FZ_ZeroP(N : in FZ) return WBool
953 renames FZ_Pred.FZ_ZeroP;
954
955 -- 1 iff N != 0 (branch-free); else 0
956 function FFA_FZ_NZeroP(N : in FZ) return WBool
957 renames FZ_Pred.FZ_NZeroP;
958
959 -- 1 iff N is odd
960 function FFA_FZ_OddP(N : in FZ) return WBool
961 renames FZ_Pred.FZ_OddP;
962
963 ----------------------------------------------------------------------------
964 --- Bitwise Operations on FZ
965 ----------------------------------------------------------------------------
966
967 -- Result := X & Y
968 procedure FFA_FZ_And(X : in FZ; Y : in FZ; Result : out FZ)
969 with Pre => X'Length = Y'Length and X'Length = Result'Length;
970
971 -- N := N & W, W is a Word
972 procedure FFA_FZ_And_W(N : in out FZ; W : in Word)
973 renames FZ_BitOp.FZ_And_W;
974
975 -- Result := X | Y
976 procedure FFA_FZ_Or(X : in FZ; Y : in FZ; Result : out FZ)
977 with Pre => X'Length = Y'Length and X'Length = Result'Length;
978
979 -- N := N | W, W is a Word
980 procedure FFA_FZ_Or_W(N : in out FZ; W : in Word)
981 renames FZ_BitOp.FZ_Or_W;
982
983 -- Result := X ^ Y
984 procedure FFA_FZ_Xor(X : in FZ; Y : in FZ; Result : out FZ)
985 with Pre => X'Length = Y'Length and X'Length = Result'Length;
986
987 -- N := N ^ W, W is a Word
988 procedure FFA_FZ_Xor_W(N : in out FZ; W : in Word)
989 renames FZ_BitOp.FZ_Xor_W;
990
991 -- NotN := ~N ('ones complement')
992 procedure FFA_FZ_Not(N : in FZ; NotN : out FZ)
993 with Pre => N'Length = NotN'Length;
994
995 ----------------------------------------------------------------------------
996 --- Basic Arithmetic on FZ
997 ----------------------------------------------------------------------------
998
999 -- Sum := X + Y; Overflow := Carry
1000 procedure FFA_FZ_Add(X : in FZ;
1001 Y : in FZ;
1002 Sum : out FZ;
1003 Overflow : out WBool)
1004 with Pre => X'Length = Y'Length and X'Length = Sum'Length;
1005
1006 -- Difference := X - Y; Underflow := Borrow
1007 procedure FFA_FZ_Subtract(X : in FZ;
1008 Y : in FZ;
1009 Difference : out FZ;
1010 Underflow : out WBool)
1011 with Pre => X'Length = Y'Length and X'Length = Difference'Length;
1012
1013 ----------------------------------------------------------------------------
1014 --- Division on FZ
1015 ----------------------------------------------------------------------------
1016
1017 -- Dividend is divided by Divisor, producing Quotient and Remainder.
1018 -- WARNING: NO div0 test here! Caller must test.
1019 procedure FFA_FZ_IDiv(Dividend : in FZ;
1020 Divisor : in FZ;
1021 Quotient : out FZ;
1022 Remainder : out FZ)
1023 renames FZ_Divis.FZ_IDiv;
1024
1025 -- Exactly same thing as IDiv, but keep only the Quotient
1026 procedure FFA_FZ_Div(Dividend : in FZ;
1027 Divisor : in FZ;
1028 Quotient : out FZ)
1029 renames FZ_Divis.FZ_Div;
1030
1031 -- Modulus.
1032 procedure FFA_FZ_Mod(Dividend : in FZ;
1033 Divisor : in FZ;
1034 Remainder : out FZ)
1035 renames FZ_Divis.FZ_Mod;
1036
1037 ----------------------------------------------------------------------------
1038 --- Multiplication on FZ
1039 ----------------------------------------------------------------------------
1040
1041 -- Multiplier. Preserves the inputs.
1042 procedure FFA_FZ_Multiply(X : in FZ;
1043 Y : in FZ;
1044 XY_Lo : out FZ;
1045 XY_Hi : out FZ)
1046 with Pre => X'Length = Y'Length and
1047 XY_Lo'Length = XY_Hi'Length and
1048 XY_Lo'Length = ((X'Length + Y'Length) / 2);
1049
1050 ----------------------------------------------------------------------------
1051 --- Modular Operations on FZ
1052 ----------------------------------------------------------------------------
1053
1054 -- Modular Multiply: Product := X*Y mod Modulus
1055 procedure FFA_FZ_Modular_Multiply(X : in FZ;
1056 Y : in FZ;
1057 Modulus : in FZ;
1058 Product : out FZ)
1059 renames FZ_ModEx.FZ_Mod_Mul;
1060
1061 -- Modular Exponent: Result := Base^Exponent mod Modulus
1062 procedure FFA_FZ_Modular_Exponentiate(Base : in FZ;
1063 Exponent : in FZ;
1064 Modulus : in FZ;
1065 Result : out FZ)
1066 renames FZ_ModEx.FZ_Mod_Exp;
1067
1068 end FFA;