asdinve added, probably fine - but none of the proof yet

asdinve/asdinve.gpr

@@ -0,0 +1,16 @@
+project Asdinve is
+
+   for Source_Dirs use ("src");
+   for Object_Dir use "obj";
+   for Main use ("asdinvemain.adb");
+
+   package Ide is
+      for Vcs_Kind use "git";
+   end Ide;
+
+   package Compiler is
+      for Switches ("ada") use ("-O3", "-funroll-loops", "-gnatp");
+   end Compiler;
+
+end Asdinve;
+

asdinve/src/asdinvelib.adb

@@ -0,0 +1,48 @@
+package body AsdinveLib with
+   SPARK_Mode
+is
+   subtype w_t is Positive;
+   type LR is (Left, Right);
+
+   type s;
+   type slrarr is array (LR) of access s;
+   type s is record
+      w : w_t;
+      t : Natural := 0;
+      c : slrarr := (null, null);
+   end record;
+
+   function result (A : arr) return Natural
+   is
+      t : Natural := 0;
+      r : access s := null;
+      p, q : access s;
+      c : LR;
+   begin
+      for u in A'Range loop
+         p := new s'(w => A(u), t => 0, c => (null, null));
+         if r = null then
+            r := p;
+         else
+            q := r;
+            loop
+               if p.w < q.w then
+                  t := t + 1 + q.t;
+                  c := Left;
+               else
+                  q.t := q.t + 1;
+                  c := Right;
+               end if;
+               if q.c(c) /= null then
+                  q := q.c(c);
+               else
+                  q.c(c) := p;
+                  exit;
+               end if;
+            end loop;
+         end if;
+      end loop;
+      return t;
+   end result;
+
+end AsdinveLib;

asdinve/src/asdinvelib.ads

@@ -0,0 +1,6 @@
+package AsdinveLib with
+SPARK_Mode
+is
+   type arr is array (Positive range <>) of Positive;
+   function result(A : arr) return Natural;
+end AsdinveLib;

asdinve/src/asdinvemain.adb

@@ -0,0 +1,20 @@
+with Ada.Integer_Text_IO;
+with AsdinveLib; use AsdinveLib;
+procedure AsdinveMain is
+   procedure run is
+      n : Positive range 2..10000;
+   begin
+      Ada.Integer_Text_IO.Get(n);
+      declare
+         a : arr (1..n);
+      begin
+         for i in a'Range loop
+            Ada.Integer_Text_IO.Get(a(i));
+         end loop;
+         Ada.Integer_Text_IO.Put(result(arr(a)));
+      end;
+   end run;
+
+begin
+   run;
+end AsdinveMain;