> John writes: > This "only" proves down to the binary API. Is there proven hardware?
Their effort is only "proven to binary" but they do manage to run Linux on it. There is a language called Verilog to specify "down to the wires and transistors" See https://www.utdallas.edu/~gxm112130/papers/iscas15.pdf There is "Project Oberon" which is designing a "complete desktop computer from scratch" staring from the wires and transistors. Their lowest layer is in Verilog on a Field Programmable Gate Array (FPGA): http://www.projectoberon.com/ https://www.inf.ethz.ch/personal/wirth/FPGA-relatedWork/RISC.pdf <https://www.inf.ethz.ch/personal/wirth/FPGA-relatedWork/RISC.pdf> The proof game at this level involve mealy/moore state machines since everything happens all at once on real hardware. I have an Altera Cyclone FPGA that can run their RISC-V Verilog http://daly.axiom-developer.org/AlteraCyclone.jpg but haven't yet had the time to run the Oberon code. So eventually the Coq proof runs from FPGA <-> Binary <-> Jitawa <-> Milawa <-> ACL2 / lisp <-> Axiom spad <-> algorithm spec <-> Coq proof. It will take longer than I expect but all of the parts are there. On Sun, Nov 11, 2018 at 7:09 PM Tim Daly <axiom...@gmail.com> wrote: > All, > > This paper about ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS > https://alastairreid.github.io/papers/popl19-isasemantics.pdf > is interesting. It seems to provide a "base case" for proving programs > correct. In particular, they seem to be able to generate proof code for > various provers, including Coq. > > One of the criticisms about "proven programs" is that they tend to > ignore implementation details. But given a lisp variant, Milaw, that > is proven to the hardware instructions this new step is really important. > > A proof of the machine instructions, a proof of milawa on top of those > instructions, a proof of lisp extensions on top of milawa, and a proof > of Axiom's spad language on top of lisp turns into a fully validated > tower. > > It appears that all of this (and it is an impressive pile) can be developed > in Coq. > > Also of interest, while I was part of the CMU CERT effort I developed > the ISA for the Intel 32 bit processor [0]. My program reads Intel binary > and generates "Conditional-Concurrent Assignment" semantics. I may > be able to re-target the back end to their Sail language which would > provide ISA semantics for Intel 32 in Coq. > > Tim > > [0] > > Daly, Timothy Intel Instruction Semantics Generator > <http://daly.axiom-developer.org/TimothyDaly_files/publications/sei/intel/intel.pdf> > SEI/CERT Research Report, March 2012 >
_______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer
