@rajan.yadav I have updated the sci . Can you test that it still works? As a bonus, I added support for Raspberry Pi 400.

Thanks @soegaard2 I will try it out. BTW, I was having more issues while using packages on Ubuntu–18 that were created on Ubuntu–20 because of some glibc issues. To make progress, I have decided to do builds on Ubuntu–18 which run fine on Ubuntu–20

Hello racketeers, rosette question here: I’m hoping to include a short example demonstrating rosette’s automatic proving in a report. I’ve contrasted Coq’s interactivity with Dafny’s auto-active reasoning through the following proofs:

• forall P: Prop, P -> P and In 5 [1;2;3;4;5] in Coq • the above, plus the primality of 0,1,2, and 6 in Dafny Can anyone suggest a short Rosette program that proves the above (preferably entirely automatically)? If not, are there similarly short examples that I could include for Rosette that demonstrate how automatic it is?

(Disclaimer: I’ve never written a rosette program.)

I don’t know the answer to your question but there is a rosette template repo at https://github.com/racket-templates/rosette-template\|https://github.com/racket-templates/rosette-template

The template contains many Rosette example files.

synth.rkt: a sample program synthesizer (synthesis query) taken from Building a Program Synthesizer by James Bornholt. verify.rkt: a sample program verifier (verification query). sudoku.rkt: a sample Sudoku solver (angelic execution query) Detailed description is given in each file.

#lang rosette ;; Let x be any integer (define-symbolic x integer?) ;; Let b be any bool (define-symbolic b boolean?) ;; Verify that b => b for any boolean b (verify (assert (=> b b))) ;; Verify that \|x\| >= 0 for any integer x (define (abs x) (if (>= x 0) x (- x))) (verify (assert (>= (abs x) 0)))

In 5 [1;2;3;4;5] and “primality of 0,1,2, and 6” are kinda pointless in Rosette, since everything is known, so regular Racket computation would suffice to arrive to the answer.

Yah, I’ll still add them, but thanks!

Silly question, but is that program supposed to give (unsat) when I run it? I couldn’t find a clear explanation of what that means as an ouput.

Yes, unsat in the context of verification means no counterexample.

Is https://github.com/racket/racket/blob/84b58d9baefd4f5d234be036d515a604eb9974d9/racket/src/cs/racket.boot supposed to be checked in?

test-case seems to prevent the subprocess custodian from killing subprocesses when the Racket process ends. Here’s a strange example that leaves a process running, but only when the process is started in a test-case: https://gist.github.com/wilbowma/f6d3eeb1a49aa88aed1b51f7897c1c51