Re: [libre-riscv-dev] spr formal proof, NLNet RFPs

diff --git a/b2/2aa40301e1dd54183e7c40b7dac0aea7ab8ac2 b/b2/2aa40301e1dd54183e7c40b7dac0aea7ab8ac2
new file mode 100644 (file)
index 0000000..8f52eda
--- /dev/null
+++ b/b2/2aa40301e1dd54183e7c40b7dac0aea7ab8ac2
@@ -0,0 +1,93 @@
+Return-path: <libre-riscv-dev-bounces@lists.libre-riscv.org>
+Envelope-to: publicinbox@libre-riscv.org
+Delivery-date: Fri, 17 Jul 2020 21:16:04 +0100
+Received: from localhost ([::1] helo=libre-riscv.org)
+       by libre-soc.org with esmtp (Exim 4.92)
+       (envelope-from <libre-riscv-dev-bounces@lists.libre-riscv.org>)
+       id 1jwWm2-0004Bm-GL; Fri, 17 Jul 2020 21:16:02 +0100
+Received: from mail-io1-f50.google.com ([209.85.166.50])
+ by libre-soc.org with esmtps (TLS1.3:ECDHE_RSA_AES_128_GCM_SHA256:128)
+ (Exim 4.92) (envelope-from <sam.falvo@gmail.com>) id 1jwWm1-0004Bg-FP
+ for libre-riscv-dev@lists.libre-riscv.org; Fri, 17 Jul 2020 21:16:01 +0100
+Received: by mail-io1-f50.google.com with SMTP id q74so11747807iod.1
+ for <libre-riscv-dev@lists.libre-riscv.org>;
+ Fri, 17 Jul 2020 13:16:01 -0700 (PDT)
+DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025;
+ h=mime-version:references:in-reply-to:from:date:message-id:subject:to;
+ bh=4a0gKh42fF2Koprsf0XkCaItHClib325lDVMpFg4XC8=;
+ b=PMkTWNjc4ozHPrQSvNPy/NK34piUagrZ7k3SRlGsvuf9ySLi7AErhidGYRnI6oAAFn
+ xxOsHSM8FW/bWezxbjjXQYne8rNRElgBY5FKJtk/ae/OPU1295Okzg5A2ZjHOn11ab8k
+ a7Jz2jaxWM2tQ2SRl4zV38Hgac+yi0Tyb6PP7QCMn5kJSZ9JqWHcNg/8gkw9ZZ2BnepL
+ oJKXFVVxiRvFaA8j4nF1P6YYk1w/jer9ByJibF1DN2ZNYs6LeOoKpGbr+7GIDVkCBeSd
+ oGDo+i+G2tszrIBOTbjmflk/ewbIy5eKjekJy4vDOy2XEdSsWc78oO7e2ChDSjZ27382
+ ObdQ==
+X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
+ d=1e100.net; s=20161025;
+ h=x-gm-message-state:mime-version:references:in-reply-to:from:date
+ :message-id:subject:to;
+ bh=4a0gKh42fF2Koprsf0XkCaItHClib325lDVMpFg4XC8=;
+ b=ttWzEuztZKpnXWo6Sz/NH3tnKA41kqBOTGLTVRhW+9/fG/4JHyliHlZCtyHl6v+uFc
+ McITVw8cpYjJCJA+J/rYicFTIzILH+GhNFAT9xFqZ6YjDdQG05ZHOxwAcnv/KI87w56x
+ FifZbxl64vG9/G5mVSnfzZJVnbI6HjMft5QGYl4wZYrsBtlXu8P84jQMD9HH2gz9Qf/E
+ zVcyN+mDbksopTkWCPNQI2x5jXqkw6MU7LdQCN0Pg8/tqZ3Wz4b1vCn+eF4NDu/dEN18
+ /d0rSWFAt44eKOEnIk37f5xLW0LsCaf1cfGCpqx5MZRyDYc2n6+Ni/9cnVxBdGuWpyPU
+ gOfQ==
+X-Gm-Message-State: AOAM530ht0ruGdbsPZ7/cOdJVQhrVGAHmMVXH4bcEWKm98C58L6HLEVE
+ lVM5z0UEV4Cl7xRv/ROwEkhfiOcAMIHaim0in0G3qy+1
+X-Google-Smtp-Source: ABdhPJzjXSd7o9eJAAx3ZxPalrbtsXhvRz7Qmss4nE1oxsKyuVRkTrYpcf2dHauy3Zp89cr5n94qXpvd0J6vwpi1Ulc=
+X-Received: by 2002:a6b:3f57:: with SMTP id m84mr10261027ioa.99.1595016960064; 
+ Fri, 17 Jul 2020 13:16:00 -0700 (PDT)
+MIME-Version: 1.0
+References: <CAPweEDws_xR1OtcjP54qGo1RgKA7Gssy+=sYU_vGXN0mVXuS6g@mail.gmail.com>
+In-Reply-To: <CAPweEDws_xR1OtcjP54qGo1RgKA7Gssy+=sYU_vGXN0mVXuS6g@mail.gmail.com>
+From: Samuel Falvo II <sam.falvo@gmail.com>
+Date: Fri, 17 Jul 2020 13:15:49 -0700
+Message-ID: <CAEz=sokKL4aCbLYj7R4=_sedycOZvrcN0jHZUr9zH6EkUR2OBQ@mail.gmail.com>
+To: Libre-RISCV General Development <libre-riscv-dev@lists.libre-riscv.org>
+Subject: Re: [libre-riscv-dev] spr formal proof, NLNet RFPs
+X-BeenThere: libre-riscv-dev@lists.libre-riscv.org
+X-Mailman-Version: 2.1.23
+Precedence: list
+List-Id: Libre-RISCV General Development
+ <libre-riscv-dev.lists.libre-riscv.org>
+List-Unsubscribe: <http://lists.libre-riscv.org/mailman/options/libre-riscv-dev>, 
+ <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=unsubscribe>
+List-Archive: <http://lists.libre-riscv.org/pipermail/libre-riscv-dev/>
+List-Post: <mailto:libre-riscv-dev@lists.libre-riscv.org>
+List-Help: <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=help>
+List-Subscribe: <http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev>, 
+ <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=subscribe>
+Reply-To: Libre-RISCV General Development
+ <libre-riscv-dev@lists.libre-riscv.org>
+Content-Type: text/plain; charset="utf-8"
+Content-Transfer-Encoding: base64
+Errors-To: libre-riscv-dev-bounces@lists.libre-riscv.org
+Sender: "libre-riscv-dev" <libre-riscv-dev-bounces@lists.libre-riscv.org>
+
+UmVnaXN0ZXJlZCBhcyBhIHBlcnNvbmFsIGFjY291bnQgZm9yIHRoZSB0aW1lIGJlaW5nLgoKSSB0
+aGluaywgaW4gdGhlIGludGVyZXN0cyBvZiBqdXN0IHByYWN0aWNpbmcgb24gdGhlIGNvZGUtYmFz
+ZSwgSSdsbApzdGljayB3aXRoIHRoZSBBTFUgRlYgcmVxdWlyZW1lbnRzIGZvciB0aGUgdGltZSBi
+ZWluZy4gIEknbSBqdXN0CmJlY29taW5nIGNvbWZvcnRhYmxlIHdpdGggc3BlbHVua2luZyB0aGF0
+IGNvZGUuICBJJ2QgbGlrZSB0byBmZWVsCnVzZWZ1bCBmb3IgYSB3aGlsZSBiZWZvcmUgSSBzdGFy
+dCBhbm90aGVyIHRhc2suICA6KQoKCk9uIEZyaSwgSnVsIDE3LCAyMDIwIGF0IDExOjUyIEFNIEx1
+a2UgS2VubmV0aCBDYXNzb24gTGVpZ2h0b24KPGxrY2xAbGtjbC5uZXQ+IHdyb3RlOgo+Cj4gc2Ft
+dWVsOiBuZXh0IHN0ZXAgaXMgdG8gbW92ZSB0aGUgdGFzayB0byAiY29tcGxldGVkIgo+IGh0dHBz
+Oi8vbGlicmUtc29jLm9yZy9TYW11ZWxfQV9GYWx2b19JSS8KPgo+IGdpdmVuIHRoYXQgeW91J3Jl
+IGluIHRoZSBVLlMuLCB1bmxlc3MgeW91IG9wZW4geW91cnNlbGYgYSBUcmFuc2Zlcndpc2UKPiBv
+bmxpbmUgYmFuayBhY2NvdW50IChhY2NlcHRpbmcgRVVSIGN1cnJlbmN5KSBOTE5ldCBoYXZlIGFz
+a2VkIHVzIHRvCj4gc3VibWl0IG5vbi1FVSBSZXF1ZXN0cyBmb3IgUGF5bWVudCBhdCByZWFzb25h
+Ymx5IGxhcmdlIGFtb3VudHMgc28gdGhhdAo+IGJhbmsgZmVlcyBhcmUgbm90IGV4dG9ydGlvbmF0
+ZS4gIChFVSBhY2NvdW50cyBpbmNsdWRpbmcgVHJhbnNmZXJ3aXNlCj4gSW50ZXJuYXRpb25hbCBv
+bmxpbmUgYWNjb3VudHMgdGhleSBoYXZlIHplcm8gYmFuayBmZWVzKQo+Cj4gYmFzaWNhbGx5LCBw
+aWNrIHlvdXIgbmV4dCBwcm9vZiA6KSAgVHJhcCwgTVVMLCBESVYsIG9yIFNoaWZ0Um90Cj4gInJv
+dGF0ZSBhbmQgY2xlYXIiLAo+IHRoZXkgYWxsIG5lZWQgZG9pbmcuCj4KPiBvciBpZiB5b3UgZ2V0
+IGJvcmVkIG9mIHRoYXQgdGhlcmUgaXMgYSBrZXkgc3RyYXRlZ2ljIHBpZWNlIG9mIGNvZGUgdGhh
+dCBuZWVkcwo+IHdyaXRpbmc6IHRoZSBMRFNUU3BsaXR0ZXIuCj4KPiBsLgo+Cj4gX19fX19fX19f
+X19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX18KPiBsaWJyZS1yaXNjdi1kZXYg
+bWFpbGluZyBsaXN0Cj4gbGlicmUtcmlzY3YtZGV2QGxpc3RzLmxpYnJlLXJpc2N2Lm9yZwo+IGh0
+dHA6Ly9saXN0cy5saWJyZS1yaXNjdi5vcmcvbWFpbG1hbi9saXN0aW5mby9saWJyZS1yaXNjdi1k
+ZXYKCgoKLS0KU2FtdWVsIEEuIEZhbHZvIElJCgpfX19fX19fX19fX19fX19fX19fX19fX19fX19f
+X19fX19fX19fX19fX19fX19fXwpsaWJyZS1yaXNjdi1kZXYgbWFpbGluZyBsaXN0CmxpYnJlLXJp
+c2N2LWRldkBsaXN0cy5saWJyZS1yaXNjdi5vcmcKaHR0cDovL2xpc3RzLmxpYnJlLXJpc2N2Lm9y
+Zy9tYWlsbWFuL2xpc3RpbmZvL2xpYnJlLXJpc2N2LWRldgo=
+