Release BLAKE2S patch version 0.1.3

Changes in this release:
- Switch from GNU Make to AST NMAKE, vastly simplifying project
Makefiles with the latter's native Ada support.
- Support for building the b2ssum utility using GPRBuild.

* .github/workflows/blake2s.yml: Run CI with AST NMAKE.
* README.md:
- Switch from inline to reference style URLS.
- Reformat for 80 columns.
- Document that AST NMAKE is required now for building.
* alire.toml: Removed as ALIRE packages are created manually now.
* b2ssum.gpr: New GPRBuild project file for the b2ssum file hash
utility.
* bin/b2ssum.adb:
- Switch from renaming operators to 'use type', as b2ssum is written
in the 1995 version of Ada and the former causes GNAT to emit warnings
about hiding standard definitions.
- Quash false positive emitted by newer versions of AdaControl (as
shipped by Debian/Ubuntu).
* blake2s.gpr:
- Increment version to 0.1.3.
- Place object files in gnat/obj and libraries in gnat/lib. The sobj
and slib directories were a holdover from the prior GNU Make setup;
NMAKE allows for building static and dynamic libraries in the same
directory.
- Per the new Alire default, disable runtime checks and contracts.
* blake2s.nmk: New Nmakefile containing project defaults.
* blake2sn.aru
* blake2so.aru:
- Add MIT-0 copyright header.
- Add clarifying comments.
- Give unnecessary_use_clause a name (Use_Rule).
* gnat/makefile.nmk: New Nmakefile for building the BLAKE2s library
and executables using GNAT.
* makefile.nmk: New Nmakefile for toolchain-agnostic operations.

Author: Lev Kujawski

.github/workflows/ada.yml

@@ -0,0 +1,44 @@
+name: BLAKE2S CI
+
+on:
+  push:
+    branches: [ trunk ]
+  pull_request:
+    branches: [ trunk ]
+
+jobs:
+  ubuntu:
+
+    runs-on: ubuntu-20.04
+
+    env:
+      TZ: UTC
+    steps:
+    - name: Checkout
+      uses: actions/checkout@v2
+
+    - name: Install Dependencies
+      run: >
+        sudo apt-get update &&
+        sudo apt-get install adacontrol gnat libdb5.3-dev
+
+    - name: Build AST NMAKE
+      run: >
+        git clone https://github.com/lkujaw/ast.git &&
+        cd ast && ./bin/package flat make
+
+    - name: Report (AdaControl)
+      run: |
+        export PATH="${PWD}/ast/bin:$PATH"
+        nmake adactl
+        cd gnat && nmake adactl && nmake clobber
+
+    - name: Build
+      run: |
+        export PATH="${PWD}/ast/bin:$PATH"
+        cd gnat && nmake
+
+    - name: Test
+      run: |
+        export PATH="${PWD}/ast/bin:$PATH"
+        cd gnat && nmake test

.github/workflows/blake2s.yml

@@ -1,37 +1,69 @@
 [![Alire](https://img.shields.io/endpoint?url=https://alire.ada.dev/badges/blake2s.json)](https://alire.ada.dev/crates/blake2s.html)
 
-# BLAKE2s for Ada #
+# BLAKE2s for Ada
 
-This is a SPARK83 implementation of the [BLAKE2s](https://www.blake2.net/) hash function. As SPARK83 is a strict subset of Ada 87 (ISO-8652:1987), this package should be usable with any standard-compliant Ada compiler.
+This is a SPARK83 implementation of the [BLAKE2s][1] hash function.
+As SPARK83 is a strict subset of Ada 1987 (ISO-8652:1987), this
+package should be usable with any standard-compliant Ada compiler.
 
-## BLAKE2s advantages ##
+## BLAKE2s advantages
 
-Like SHA-256, BLAKE2s operates on 32-bit words, but is not susceptible to the length extension attacks of the former. Although the FIPS hash functions SHA-512/256 and SHA-3 mitigate the length extension vulnerability of SHA-256, they require 64-bit words for decent performance. Thus, BLAKE2s fills a niche for resource-constrained platforms. It also enjoys a high security margin, as each of the ten BLAKE2s rounds is the equivalent of two ChaCha rounds.
+Like SHA-256, BLAKE2s operates on 32-bit words, but is not susceptible
+to the length extension attacks of the former.  Although the FIPS hash
+functions SHA-512/256 and SHA-3 mitigate the length extension
+vulnerability of SHA-256, they require 64-bit words for decent
+performance.  Thus, BLAKE2s fills a niche for resource-constrained
+platforms. It also enjoys a high security margin, as each of the ten
+BLAKE2s rounds is the equivalent of two ChaCha rounds.
 
-## Build instructions for GNAT ##
+## Build instructions for GNAT
 
-To compile the blake2s library and executables, you will need a copy of GCC within your path that includes the GNAT Ada front-end.
+To compile the BLAKE2s library and executables, you will need to have
+installed and accessible within your path copies of [AST NMAKE][2]
+with Ada support and the GCC compiler built with the GNAT Ada
+front-end enabled.
 
-To use the included Makefile, run "cd gnat && make" .
+Once the prerequisites are available, simply run `cd gnat && nmake` .
 
-## SPARK and Isabelle verification ##
+## SPARK and Isabelle verification
 
-This project uses a combination of the original, annotation-based SPARK tool set (search [AdaCore Libre](https://libre.adacore.com/) for the 2012 GPL release) and the HOL-SPARK library bundled within [Isabelle](https://isabelle.in.tum.de/) 2021 to prove the absence of runtime errors.
+This project uses a combination of the original, annotation-based
+SPARK tool set (search [AdaCore Libre][3] for the 2012 GPL release)
+and the HOL-SPARK library bundled within [Isabelle][4] 2021 to prove
+the absence of runtime errors.
 
-To verify the proofs, check the Makefile within the project root first to ensure that you have the necessary programs (including the 'isabelle' command) installed within your path.
+To verify the proofs, check the file named `makefile.nmk` within the
+project root first to ensure that you have the necessary programs
+(including the `isabelle` command) installed within your path.
 
-If everything is functioning as it should, there should be no undischarged verification conditions.
+If everything is functioning as it should, there should be no
+undischarged verification conditions.
 
-## Ada 87 compatibility note ##
+## Ada 1987 compatibility note
 
-This package utilizes the Ada 95 pragma "Pure" in the following package specifications:
+This package utilizes the Ada 1995 pragma "Pure" in the following
+package specifications:
 
 * BLAKE2S (common/blake2s.ads)
 * Octets (common/octets.ads)
 * Octet_Arrays (common/octearra.ads)
 
-Per section 2.8 of the Ada 87 Language Reference Manual, "[a] pragma that is not language-defined has no effect if its identifier is not recognized by the (current) implementation." However, as the pragma is merely advisory to the compiler, it may be removed without adverse effect from these files should it cause any issues.
-
-## Credits
-
-Thanks to Aumasson et al. for releasing the excellent BLAKE hash functions into the public domain, and the [GNAT, SPARK](https://libre.adacore.com/), [Isabelle](https://isabelle.in.tum.de/), and [AdaControl](https://www.adalog.fr/en/adacontrol.html) developers for publishing their tremendously helpful [free software](https://www.gnu.org/philosophy/free-sw.html).
+Per section 2.8 of the Ada 1987 Language Reference Manual, "[a] pragma
+that is not language-defined has no effect if its identifier is not
+recognized by the (current) implementation." However, as the pragma is
+merely advisory to the compiler, it may be removed without adverse
+effect from these files should it cause any issues.
+
+## Acknowledgments
+
+Thanks to Aumasson et al. for releasing the excellent BLAKE hash
+functions into the public domain, and the [GNAT, SPARK][3],
+[Isabelle][4], and [AdaControl][5] developers for publishing their
+tremendously helpful [free software][6].
+
+[1]: https://www.blake2.net/
+[2]: https://sr.ht/~lev/ast/
+[3]: https://libre.adacore.com/
+[4]: https://isabelle.in.tum.de/
+[5]: https://www.adalog.fr/en/adacontrol.html
+[6]: https://www.gnu.org/philosophy/free-sw.html

Makefile

@@ -0,0 +1,102 @@
+------------------------------------------------------------------------------
+--  Copyright (c) 2021, Lev Kujawski.
+--
+--  Permission is hereby granted, free of charge, to any person obtaining a
+--  copy of this software and associated documentation files (the "Software")
+--  to deal in the Software without restriction, including without limitation
+--  the rights to use, copy, modify, merge, publish, distribute, sublicense,
+--  and sell copies of the Software, and to permit persons to whom the
+--  Software is furnished to do so.
+--
+--  THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+--  IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+--  FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL
+--  THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+--  LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
+--  FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
+--  DEALINGS IN THE SOFTWARE.
+--
+--  SPDX-License-Identifier: MIT-0
+------------------------------------------------------------------------------
+
+with "blake2s.gpr";
+
+project B2SSUM is
+
+   for Source_Dirs use ("bin");
+   for Object_Dir use "gnat/obj";
+   for Exec_Dir use "gnat/bin";
+   for Create_Missing_Dirs use "True";
+   for Main use ("b2ssum.adb");
+
+   type Enabled_Kind is ("enabled", "disabled");
+   Compile_Checks : Enabled_Kind :=
+      External ("B2SSUM_COMPILE_CHECKS", "disabled");
+   Runtime_Checks : Enabled_Kind :=
+      External ("B2SSUM_RUNTIME_CHECKS", "disabled");
+   Style_Checks : Enabled_Kind :=
+      External ("B2SSUM_STYLE_CHECKS", "disabled");
+   Contracts_Checks : Enabled_Kind :=
+      External ("B2SSUM_CONTRACTS", "disabled");
+
+   type Build_Kind is ("debug", "optimize");
+   Build_Mode : Build_Kind := External ("B2SSUM_BUILD_MODE", "optimize");
+
+   Compile_Checks_Switches := ();
+   case Compile_Checks is
+      when "enabled" =>
+         Compile_Checks_Switches :=
+           ("-gnatVa",   --  Enable all validity checks
+            "-gnatwaJ",  --  Enable warnings, minus obsolescent
+            "-gnatwe");  --  Set Warnings as errors
+      when others => null;
+   end case;
+
+   Runtime_Checks_Switches := ();
+   case Runtime_Checks is
+      when "enabled" => null;
+      when others =>
+         Runtime_Checks_Switches :=
+           ("-gnatp");  --  Suppress checks
+   end case;
+
+   Style_Checks_Switches := ();
+   case Style_Checks is
+      when "enabled" =>
+         Style_Checks_Switches :=
+           ("-gnaty3abcefhiklM78nprtux");
+      when others => null;
+   end case;
+
+   Contracts_Switches := ();
+   case Contracts_Checks is
+      when "enabled" =>
+         Contracts_Switches :=
+           ("-gnata");  --  Enable assertions and contracts
+      when others => null;
+   end case;
+
+   Build_Switches := ();
+   case Build_Mode is
+      when "optimize" =>
+         Build_Switches := ("-O3",      --  Optimization
+                            "-gnatN");  --  Enable front-end inlining
+      when "debug" =>
+         Build_Switches := ("-g",    --  Emit debugging data
+                            "-Og");  --  Disable optimization
+   end case;
+
+   package Compiler is
+      for Default_Switches ("Ada") use
+        Compile_Checks_Switches &
+        Build_Switches &
+        Runtime_Checks_Switches &
+        Style_Checks_Switches &
+        Contracts_Switches;
+   end Compiler;
+
+   package Binder is
+      for Switches ("Ada") use ("-Es");  --  Enable symbolic tracebacks
+   end Binder;
+
+end B2SSUM;

README.md

@@ -45,20 +45,18 @@ with Ada.Text_IO.Text_Streams;
 with Ada.Strings.Unbounded;
 
 with BLAKE2S;
+use type BLAKE2S.Digest_T;
+--  Quash false positive from AdaControl:
+--! rule off Use_Rule
+use type BLAKE2S.Status_T;
+--! rule on Use_Rule
 
 with Octets;
 use type Octets.T;
 
 with Octet_Arrays;
 
 procedure B2SSum is
-   function "=" (Left  : in BLAKE2S.Digest_T;
-                 Right : in BLAKE2S.Digest_T) return Boolean
-     renames BLAKE2S."=";
-
-   function "=" (Left  : in BLAKE2S.Status_T;
-                 Right : in BLAKE2S.Status_T) return Boolean
-     renames BLAKE2S."=";
 
    package ACH renames Ada.Characters.Handling;
    package ACL renames Ada.Command_Line;

alire.toml

@@ -22,16 +22,16 @@
 project BLAKE2S is
 
    for Library_Name use "b2sa";
-   for Library_Version use "0.1.2";
+   for Library_Version use "0.1.3";
 
    type Library_Type_Type is ("relocatable", "static", "static-pic");
    Library_Type : Library_Type_Type :=
      external ("BLAKE2S_LIBRARY_TYPE", external ("LIBRARY_TYPE", "static"));
    for Library_Kind use Library_Type;
 
    for Source_Dirs use ("gnat", "common");
-   for Object_Dir use "gnat/sobj";
-   for Library_Dir use "gnat/slib";
+   for Object_Dir use "gnat/obj";
+   for Library_Dir use "gnat/lib";
    for Create_Missing_Dirs use "True";
 
    package Naming is
@@ -48,11 +48,11 @@ project BLAKE2S is
    Compile_Checks : Enabled_Kind :=
       External ("BLAKE2S_COMPILE_CHECKS", "disabled");
    Runtime_Checks : Enabled_Kind :=
-      External ("BLAKE2S_RUNTIME_CHECKS", "enabled");
+      External ("BLAKE2S_RUNTIME_CHECKS", "disabled");
    Style_Checks : Enabled_Kind :=
       External ("BLAKE2S_STYLE_CHECKS", "disabled");
    Contracts_Checks : Enabled_Kind :=
-      External ("BLAKE2S_CONTRACTS", "enabled");
+      External ("BLAKE2S_CONTRACTS", "disabled");
 
    type Build_Kind is ("debug", "optimize");
    Build_Mode : Build_Kind := External ("BLAKE2S_BUILD_MODE", "optimize");