From mboxrd@z Thu Jan 1 00:00:00 1970 Return-path: Envelope-to: publicinbox@libre-riscv.org Delivery-date: Fri, 17 Jul 2020 19:52:14 +0100 Received: from localhost ([::1] helo=libre-riscv.org) by libre-soc.org with esmtp (Exim 4.92) (envelope-from ) id 1jwVSv-0002m7-Gh; Fri, 17 Jul 2020 19:52:13 +0100 Received: from lkcl.net ([217.147.94.29]) by libre-soc.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.92) (envelope-from ) id 1jwVSu-0002m1-Jk for libre-riscv-dev@lists.libre-riscv.org; Fri, 17 Jul 2020 19:52:12 +0100 DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=lkcl.net; s=201607131; h=Content-Type:To:Subject:Message-ID:Date:From:MIME-Version; bh=iCBFPD15M1WYplOBr5M4qrnKaBxrohZM8K6iAZR+X0w=; b=JfNOP0roC9K1vRxu3J7QhCV4kWl+1X/s6fKxg4GgJ3bsLBvpSgJX2dOlXF7O5N1/byzwmMeyU4awGlmK9idjVH/VfIuneCtIP8GA74syaeq9ZVtSGSE8vMyrP+PF3FRDwpA/Ldjfe2omIYm4XeD97jx/Df6B/7WryjZIQ/oZzFY=; Received: from mail-lj1-f174.google.com ([209.85.208.174]) by lkcl.net with esmtpsa (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.84_2) (envelope-from ) id 1jwVSu-0007EG-63 for libre-riscv-dev@lists.libre-riscv.org; Fri, 17 Jul 2020 18:52:12 +0000 Received: by mail-lj1-f174.google.com with SMTP id z24so13808334ljn.8 for ; Fri, 17 Jul 2020 11:51:56 -0700 (PDT) X-Gm-Message-State: AOAM531U0Nj5pSPNYrUMTZ2xDCnutTWaJn/J/iPOE4N64uFMDROXXrbq ZsOCXNYcTkLuYeTKT16aY5Ld7+IRR13uW76e+Ng= X-Google-Smtp-Source: ABdhPJzxMWaTclgHBtrX3zEO7IphsgHkBWexYKmsadYjrocMeGQuGPXCosqQBGAJTEexEHs5tlGQJHBmMkw33U396QE= X-Received: by 2002:a2e:9b19:: with SMTP id u25mr4608912lji.161.1595011911146; Fri, 17 Jul 2020 11:51:51 -0700 (PDT) MIME-Version: 1.0 From: Luke Kenneth Casson Leighton Date: Fri, 17 Jul 2020 19:51:40 +0100 X-Gmail-Original-Message-ID: Message-ID: To: Libre-RISCV General Development Subject: [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 List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Reply-To: Libre-RISCV General Development 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" Archived-At: List-Archive: c2FtdWVsOiBuZXh0IHN0ZXAgaXMgdG8gbW92ZSB0aGUgdGFzayB0byAiY29tcGxldGVkIgpodHRw czovL2xpYnJlLXNvYy5vcmcvU2FtdWVsX0FfRmFsdm9fSUkvCgpnaXZlbiB0aGF0IHlvdSdyZSBp biB0aGUgVS5TLiwgdW5sZXNzIHlvdSBvcGVuIHlvdXJzZWxmIGEgVHJhbnNmZXJ3aXNlCm9ubGlu ZSBiYW5rIGFjY291bnQgKGFjY2VwdGluZyBFVVIgY3VycmVuY3kpIE5MTmV0IGhhdmUgYXNrZWQg dXMgdG8Kc3VibWl0IG5vbi1FVSBSZXF1ZXN0cyBmb3IgUGF5bWVudCBhdCByZWFzb25hYmx5IGxh cmdlIGFtb3VudHMgc28gdGhhdApiYW5rIGZlZXMgYXJlIG5vdCBleHRvcnRpb25hdGUuICAoRVUg YWNjb3VudHMgaW5jbHVkaW5nIFRyYW5zZmVyd2lzZQpJbnRlcm5hdGlvbmFsIG9ubGluZSBhY2Nv dW50cyB0aGV5IGhhdmUgemVybyBiYW5rIGZlZXMpCgpiYXNpY2FsbHksIHBpY2sgeW91ciBuZXh0 IHByb29mIDopICBUcmFwLCBNVUwsIERJViwgb3IgU2hpZnRSb3QKInJvdGF0ZSBhbmQgY2xlYXIi LAp0aGV5IGFsbCBuZWVkIGRvaW5nLgoKb3IgaWYgeW91IGdldCBib3JlZCBvZiB0aGF0IHRoZXJl IGlzIGEga2V5IHN0cmF0ZWdpYyBwaWVjZSBvZiBjb2RlIHRoYXQgbmVlZHMKd3JpdGluZzogdGhl IExEU1RTcGxpdHRlci4KCmwuCgpfX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19f X19fX19fX19fXwpsaWJyZS1yaXNjdi1kZXYgbWFpbGluZyBsaXN0CmxpYnJlLXJpc2N2LWRldkBs aXN0cy5saWJyZS1yaXNjdi5vcmcKaHR0cDovL2xpc3RzLmxpYnJlLXJpc2N2Lm9yZy9tYWlsbWFu L2xpc3RpbmZvL2xpYnJlLXJpc2N2LWRldgo=