sel4 / l4v

seL4 specification and proofs

The seL4 microkernel

This project contains the source code of seL4 microkernel.

For details about the seL4 microkernel, including details about its formal correctness proof, please see the sel4.systems website and associated FAQ.

DOIs for citing recent releases of this repository:

• 

We welcome contributions to seL4. Please see the website for information on how to contribute.

This repository is usually not used in isolation, but as part of the build system in a larger project.

seL4 Basics

• Tutorials
• Documentation
• seL4 libraries
• seL4Test
• Debugging guide
• Benchmarking guide
• Virtualization on seL4
• Host Build Dependencies
• Porting seL4

Community

• Forums:
  • Discourse
  • seL4 Announce
  • seL4 Devel
• Suggested projects
• Community projects

See the contact links on the seL4 website for the full list.

Reporting security vulnerabilities

If you believe you have found a security vulnerability in seL4 or related software, we ask you to follow our vulnerability disclosure policy.

Manual

A hosted version of the manual for the most recent release can be found here.

A web version of the API can be found here

Repository Overview

• include and src: C and ASM source code of seL4
• tools: build tools
• libsel4: C bindings for the seL4 ABI
• manual: LaTeX sources of the seL4 reference manual

Build Instructions

See the seL4 website for build instructions.

Status

A list of releases and current project status can be found under seL4 releases.

• Roadmap: new features in development
• Hardware Support: information about hardware platform ports
• Kernel Features: information about available kernel features
• Userland Components and Drivers: available device drivers and userland components

License

See the file LICENSE.md.

l4v's Issues

autocorres build failure.please help me!

@lsf37 hello,autocorres build failure, please help me!thank you very much!

root@ubuntu:/home/ubuntu/verification/l4v# L4V_ARCH=ARM misc/regression/run_tests.py AutoCorres
Running 3 test(s)...
Started isabelle ...
Finished isabelle passed ( 0:00:33 real, 0:00:43 cpu, 0.49GB)
Started CParser ...
Finished CParser passed ( 0:00:22 real, 0:00:46 cpu, 0.75GB)
Started AutoCorres ...
Finished AutoCorres FAILED * ( 0:01:15 real, 0:01:44 cpu, 1.68GB)

---

TEST FAILED: AutoCorres

...
'a -> Proof.state -> bool * (string * 'b list)

theory "Lib.NICTATools"

2.585s elapsed time, 2.559s cpu time, 0.000s GC time

Loading theory "Lib.Value_Abbreviation" (required by "AutoCorres.AutoCorres" via "AutoCorres.SimplConv" via "AutoCorres.L1Defs" via "AutoCorres.CCorresE" via "AutoCorres.NonDetMonadEx" via "Lib.NonDetMonadLemmaBucket" via "Lib.NonDetMonadVCG" via "Lib.NonDetMonadLemmas" via "Lib.NonDetMonad" via "Lib.Lib")
structure Value_Abbreviation:
sig
val value_and_abbreviation:
Syntax.mode ->
binding -> string -> bool -> Proof.context -> local_theory
end
value_abbreviation_test_important_magic_number <equiv> 16777184
value_abbreviation_test_range_of_options <equiv>
[24, 23, 22, 21, 20, 19, 18, 17, 16, 15, 14, 13, 12, 11, 10, 9, 8, 7, 6, 5]

theory "Lib.Value_Abbreviation"

1.148s elapsed time, 1.142s cpu time, 0.027s GC time

Loading theory "Lib.Lib" (required by "AutoCorres.AutoCorres" via "AutoCorres.SimplConv" via "AutoCorres.L1Defs" via "AutoCorres.CCorresE" via "AutoCorres.NonDetMonadEx" via "Lib.NonDetMonadLemmaBucket" via "Lib.NonDetMonadVCG" via "Lib.NonDetMonadLemmas" via "Lib.NonDetMonad")
consts
delete :: "'a <Rightarrow> 'a list <Rightarrow> 'a list"
consts
theRight :: "'a + 'b <Rightarrow> 'b"
consts
theLeft :: "'a + 'b <Rightarrow> 'a"
consts
opt_rel ::
"('a <Rightarrow> 'b <Rightarrow> bool)
<Rightarrow> 'a option <Rightarrow> 'b option <Rightarrow> bool"

theory "Lib.Lib"

17.886s elapsed time, 17.549s cpu time, 0.730s GC time

*** exception THM 0 raised (line 105 of "global_theory.ML"):
*** Duplicate use of derivation identity for Lib.exception_set_finite_1 vs. Lib.exception_set_finite(1)
*** finite {x. ?P x} <Longrightarrow>
*** finite {x. (x = ?y <longrightarrow> ?Q x) <and> ?P x}
*** At command "end" (line 2622 of "/home/ubuntu/verification/l4v/lib/Lib.thy")
Unfinished session(s): AutoCorres

Finished at Mon Jul 26 03:41:29 GMT 2021
0:01:11 elapsed time, 0:00:46 cpu time, factor 0.65
../../misc/isa-common.mk:45: recipe for target 'AutoCorres' failed
make: *** [AutoCorres] Error 2

error building doc for haskell prototype

I ran make in l4v/spec/haskell/doc and I got the following error:

figures/clientkernel.mp figures/clientkernel.mps

Sorry, I can't find the 'mpost' preload file; will try 'plain'.
I can't find the 'plain' preload file!
make: *** [figures/clientkernel.mps] Error 1

ARM-HYP: factor out VCPU functions

In the abstract specification we had put a lot of VCPU content into ArchVSpace and ArchVSpaceAcc, even though VCPUs aren't really very related to VSpace. This content has now been factored out for AArch64 and we should do the same for ARM-HYP as well.

See d79032a for the AArch64 refactoring.

should corres_underlying imply failure preservation?

While discussing the monadic rewrite framework in #487, we realised that monadic_rewrite demands that failure on the concrete side implies failure of the abstract side. This is a general refinement principle, but it is not the case in our current definition of corres_underlying.

This is not a problem for the strength of our current refinement theorems, because corres_underlying has these failure flags that control which failures we need to prove and which we can assume, and the way we use them has the correct properties (implies absence of failure in the refinement stack).

One could still make the argument that this makes corres_underlying a bit strange in terms of refinement definitions. If it had the implication, we would get the expected standard definition of refinement when the state space of abstract and concrete are equal (i.e. just subset and failure implication). Currently, one would have to add the failure implication separately. Apart from philosophical niceness, this also has an impact on the relationship between monadic_rewrite (which does this correctly) and corres_underlying (where it is ad-hoc).

It'd be easy to change the definition, but the usual worry is that too many proofs would need to be updated. We should investigate how bad it really would be to do that.

use datatype package selectors, discriminators etc in ASpec and ExecSpec

ASpec and ExecSpec were written before the "new" datatype package existed, which introduced selectors (named fields) and discriminators (is_Cons) for data types. In a number of places, we still have old definitions that duplicate these. We should get rid of them.

This is not entirely non-trivial, because the datatype package adds default dest, simp, etc rules which will break some proofs.

PR #340 did an experiment on this on the rt branch for thread_state. This was successful but shows there is some proof work associated with it. In particular it sounds like the generated distinct_disc rule set sometimes leads to non-termination.

See also VER-957 for potential follow-on issues.

errors happen using proof count

Hi, I am using proofcount with Isabelle 2016 in Ubuntu. Some errors occur as follows.

Could you help to correct them? thanks.

---

zhaoyw@zhaoyw-VirtualBox:~/research$ isabelle proofcount -x xkernel.xml -d xkernel -L XKernel -T SK_L2Spec
Starting ProofCount...
Making new metric file at /home/zhaoyw/research/xkernel.xml. Running Isabelle...
Building XKernel ...
Document at /home/zhaoyw/research/xkernel/output/document.pdf
Finished XKernel (0:05:53 elapsed time, 0:06:38 cpu time, factor 1.12)
Running ProofCount_Exec ...

ProofCount_Exec FAILED
(see also /home/zhaoyw/.isabelle/Isabelle2016/heaps/polyml-5.6_x86_64-linux/log/ProofCount_Exec)

*** ML error (line 86 of "/software/proofcount/proof_count.ML"):
*** Type error in function application.
*** Function: wrap_lthy' :
*** Keyword.keywords ->
*** (Token.T list -> ('a -> Proof.context -> Proof.context) * 'b) ->
*** Token.T list -> ('a -> Proof.context -> Proof.context) * 'b
*** Argument: "lemmas" : string
*** Reason:
*** Can't unify Keyword.keywords with string (In Basis)
*** (Different type constructors)
*** ML error (line 86 of "/software/proofcount/proof_count.ML"):
*** Value or constructor (lemmaK) has not been declared in structure Thm
*** ML error (line 188 of "/software/proofcount/proof_count.ML"):
*** Type error in function application.
*** Function: add_new_lemmas thy thy' pos pos : Keyword.keywords -> unit
*** Argument: name : string
*** Reason:
*** Can't unify Keyword.keywords with string (In Basis)
*** (Different type constructors)
*** At command "ML_file" (line 15 of "/software/proofcount/ProofCount.thy")
Unfinished session(s): ProofCount_Exec
0:06:34 elapsed time, 0:06:58 cpu time, factor 1.06
isabelle processing proofcount failed

Reduce C parser dependencies

Check if there are C parser dependencies that can be removed before we factor out the tool into its own repository.

write docs + tests for AddUpdSimps

AddUpdSimps.thy should probably be used more, but has no documentation, is hard to discover and has no examples/test cases.

This is issue is for rectifying docs, examples, and tests.

add `crunches` lifting syntax

Raf's idea: one thing that is annoying to type in crunches is longer lambda expressions in crunches, e.g. the common pattern

"%s. P (machine_state s)"

We could add syntax for doing this automatically, e.g.

crunches some_fun
  for machine_state: (lift) "machine_state"

to be equivalent to

crunches some_fun
  for machine_state: "%s. P (machine_state s)"

Edit: Raf suggested (lift) instead of (lifted). Bit shorter and I think it fits better.

run_tests needs certain latex packages such as texlive-latex-extra (ubuntu linux)

I recently got "run_tests" in the l4v repository to pass on an Ubuntu 14.04 Linux system and needed to install several additional packages in order for the latex calls to succeed. I recommend adding the following to the instructions in README.md:

$ sudo apt-get install texlive-fonts-recommended texlive-latex-extra texlive-metapost texlive-bibtex-extra

In case it matters, here is what each package is needed for:

• Test CamkesAdlSpec (among others) fails due to missing font "ptmr7t" without texlive-fonts-recommended.
• Tests ASpec fails due to missing "fixme.sty" without texlive-latex-extra.
• Test HaskellKernel fails due to mpost missing its preload files without texlive-metapost. (This one seems to be in part due to an Ubuntu packaging error.)
• Test AutoCorresDoc fails due to missing "plainurl.bst" without texlive-bibtex-extra.

sync testing

body

Reduce Monad lib dependencies

To factor AutoCorres out from l4v, the monad libraries will need to move with them. They currently depend on most of l4v/lib, which should not be necessary.

This issue is for reducing these dependencies.

vcpu: investigate if check in vppi_event can be dropped

Currently, vppi_event is defined as

  "vppi_event irq = do
     cur_vcpu ← gets (arm_current_vcpu ∘ arch_state);
     case cur_vcpu
       of Some (vcpu_ptr, True) ⇒ do
            do_machine_op $ maskInterrupt True irq;
            vppi ← return $ the $ irq_vppi_event_index irq;
            vcpu_update vcpu_ptr
                        (λvcpu. vcpu⦇ vcpu_vppi_masked := (vcpu_vppi_masked vcpu)(vppi := True) ⦈);
            ct ← gets cur_thread;
            st ← get_thread_state ct;
            ― ‹until a proof links active current vcpu to runnable current thread, we need this
               check: @{term handle_fault} needs a runnable current thread›
            when (runnable st) $ handle_fault ct $ ArchFault $ VPPIEvent irq
          od
        | _ ⇒ return ()
   od"

Since we now have an invariant that the current thread and active vcpu are linked, we might have enough information to drop this check (and any corresponding checks in C).

Question: Fail to parse function pointers

I am trying to parse a program that uses function pointers, they are only void functions that returns void, arguments are modified through global variables.

Basically there is only a function pointer that can be set to a given routine, in the example below I set it to point to foo() function, but still there is not enough data to ensure that only the global variables are modified?

static int counter;

void foo(void) {
	counter++;
}

void (*p_fun)(void);

void set_function(void) {
	p_fun = foo;
}

void call_function(void) {
	if(p_fun) p_fun();
}

`Tactic failed 
The error(s) above occurred for the goal statement⌂:
∀σ. Γ⊢⇘/UNIV⇙ {σ} Call foo_'proc
               {t. t may_only_modify_globals σ in [counter]`

Make sizes of C structs available in higher level specs

It would be convenient to have direct and automatic access to the sizes of C structs in the higher level specs, namely the abstract spec and the design spec, and in AInvs and Refine.

An example is the size of the scheduling context struct. This is currently hard coded in the abstract spec as a natural number, and used in several important places in Refine, but must be manually updated in the abstract spec whenever a change to the C struct is made.

These sizes are currently generated within CKernel, and will produce a constant struct_size_of. It would be ideal, however, to not require the entire CKernel session to produce these constants.

A further idea due to @Xaphiosis is to have a separate session that would perform sanity checks for constants which occur in both the abstract spec and at the C level.

fix CI for SimplExportAndRefine on MCS

We're currently attempting to build SimplExportAndRefine and CKernel for the MCS config of seL4 from the master branch of l4v. This was convenient because it kept the CI workflow simple.

It also used to work fine, but now breaks since we have added annotations to the C code that need concepts only available on the rt branch.

This is issue for fixing the CI test so proof updates are deployed again to the manifest. An intermediate step could be to just disable this step. Longer term, we want to switch l4v to the rt branch. This might be as simple as supplying a branch argument to the test, but I'm sure complications will arise as they always do.

Confusing version number for Abstract Specification

The abstract specification *.pdf file generated by building the ASpec session is labeled with the seL4 API version number, which has not changed in the past four years. However, it seems that the abstract specification has undergone some substantial changes over that time period. I have encountered multiple seL4 specifications which are quite different from one another, yet list the same version number.

I found this confusing. Wouldn't it be better to label the abstract specification with the seL4 version number, e.g. 7.0.0?

Refine, Bisim, Acess I/O error message

Hi All,

I am trying to run the Refine, Bisim, and Access tests in my new installation of Sel4 on a dual boot ubuntu 16.04-1 LTL (Xenial Xerus) . I did not get what the error message means, it is quite short (please see the example below). If someone can help I will appreciate that a lot.

One note: the first time I ran the tests on my dual boot machine the tests were interrupted due to the small Ubuntu partition size (~50 G at that time) the tests Refine, Bisim, and Acess all have been executing at that time and they failed due to lack of memory and nothing was written. Later I expanded the ubuntu partition (to 138 G), all tests- except these three-worked (some skipped due to dependencies). Moreover, when I
use:
" find $HOME -iname 'Refine.*' -size 0M " it returns :
/home/ssrgv/.isabelle/heaps-ARM-home-ssrgv-Desktop-verification-isabelle/polyml-5.6_x86_64-linux/log/Refine.gz

the same happens for Bisim and Access.

Does this mean the size is 0 and probably nothing is written in this file? So there is no input and thus no output? If so can you please advise how to solve it?

Example:
:~/Desktop/verification/l4v$ ./isabelle/bin/isabelle build -d . -v -b Refine
Started at Tue Dec 20 11:44:16 EST 2016 (polyml-5.6_x86_64-linux on ssrgv-ThinkPad-T440p)
ISABELLE_BUILD_OPTIONS=""

ISABELLE_BUILD_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx2560m -Xss4m"

ML_PLATFORM="x86_64-linux"
ML_HOME="/home/ssrgv/.isabelle/contrib/polyml-5.6-1/x86_64-linux"
ML_SYSTEM="polyml-5.6"
ML_OPTIONS="-H 2000"

Session Pure/Pure
Session HOL/HOL (main)
Session HOL/HOL-Word (main)
Session Unsorted/Word_Lib
Session Specifications/ASpec
Session Proofs/AInvs
Session Proofs/BaseRefine
Session Proofs/Refine
*** I/O error
Finished at Tue Dec 20 11:44:19 EST 2016
0:00:03 elapsed time, 0:00:17 cpu time

HaskellKernel fails to build on a fresh setup

Due to missing cabal database. I suggest adding a call to $(CABAL) update to the sandbox target.

`cinit lift: name` does not substitute `name = t` assumptions

Currently cinit lift: x_' leaves an assumption of the form x = t in the assumptions, where x is a new parameter (the lifted x_') and x occurs in the procedure body.

According to the ML code in substutite_asm_eqs in ctac-method.ML the intention is that these equations should be used for substitution so that the procedure body instead contains t.

It's not clear to me since when this stopped working or if it ever worked in the first place.

Instead of custom code, we can probably call bound_hyp_subst_tac or hyp_subst_tac directly here to the the intended effect. Any fallout from that should be relatively easy to fix (famous last words).

Question: Some problems encountered when using Isabelle to create a new rule base

Recently, I encountered some problems while studying Isabelle. Is there any great god who can help me solve them?Thank you.

1. When I try to create a new rule base, copy the Ex exist quantifier that has been defined in "Isabelle2017\src\HOL\HOL.thy", it will report an error, and use code_Q for mapping will also report an error.

2. "Isabelle2017\src\HOL\HOL.thy" is a built-in rule, why will it report an error when it is opened?

[autocorres] Arrays in binary search example

TL;DR: Why is the array handling in tools/autocorres/tests/examples/BinarySearch.thy so complicated?
Type of Issue: Question
Possible Fix: Comment at the top of the file.
Severity: none

---

Hi,

I was just browsing through the autocorres examples. The binary search example (binary_search.c) appeared interesting. However, the theory file (BinarySearch.thy) was slightly intimidating. First, a generic array abstraction is defined in this example file. Doesn't autocorres provide magic to lift arrays to HOL types? What about an array abstraction in a library? Second, the proof(s) are full of low-level details and. I don't want to Sweat the Small Stuff (reference intended) 😄.

What is the current state of this binary search example?
Is it just slightly outdated and doesn't use most of the autocorres automation?
Does it deliberately demonstrate how to implement new abstractions (here: an array)?
Could autocorres currently provide more automation to simplify the example?

Thanks is advance
Cornelius

should we remove unused `Eval_Bool` from Lib?

The Eval_Bool theory defines a simp_proc and a proof method for reducing bool terms to values via the code generator.

This is not a bad idea, but despite it being set up in AInvs for all architectures it is entirely unused otherwise and removing the setup affects none of our proofs.

We could decide to actually use the method or simp_proc, but invoking the code generator on every term all the time is too expensive, so we can't make the simp_proc global. Remembering that the method exists in the cases where it would help doesn't seem to have worked so far. So in the interest of reducing maintenance, I would vote for removing it.

There is as usual one wrinkle: the theory also defines a gadget for getting code generator equations out of locales. I haven't looked at whether this is still necessary in Isabelle2021-1 (this is from 2017), but we of course do have a lot of stuff in locales and enabling code generator equations for it could come in handy at some point, e.g. for quickcheck. Then again, current proofs are entirely unaffected if removed, so it doesn't seem to be making a big difference.

We can always resurrect this from history if we do need it at some point.

MCS replies from kernel need a thorough review

The PR seL4/seL4#243 fixes an issue in PageGetAddr and SchedContextYield + SchedContextConsumed. The underlying problem in that issue is that in the (already verified) PageGetAddr we do not use the spec convention for passing back a reply from the user to the kernel.

That reply-from-kernel convention in the spec (and Haskell) is that the the perform* functions return a list, which contains the reply, and handleInvocation then sets message info etc correspondingly and also handles the thread state correctly.

Whoever wrote PageGetAddr in C didn't know about that protocol and got the thread state update wrong. Whoever did the spec+proof update didn't know the protocol either and modelled explicit setting of message registers and message info (IPC buffer etc). In X64 you can see an attempt to get the thread state, presumably to later set it, which then probably didn't work in CRefine. In any case, we end up with quite a bit of effort in the spec to get to the result that both spec and C are wrong (correctly modelling each other). I'm working on fixing this for PageGetAddr, which is reasonably small and should also make the proofs a bit nicer.

Why does this affect MCS: in looking at the fix for SchedContextYield + SchedContextConsumed I realised that the protocol for replies to the user is completely broken/absent in most new MCS calls. This is pretty bad. It likely means that we have bugs for correct thread state setting, which the proofs will not find, because there is no property that enforces this, only that protocol. As a user, you only notice these if you are actually trying to read the reply from the kernel, which apparently does not happen that often (nobody noticed it until that PR above).

So. I think what we need to do is look at this fairly deeply in both C and all spec levels and refactor the code to actually follow the reply-from-kernel protocol. This is going to be a bit hairy, because MCS sets message registers and IPC buffer content often fairly deep in the function call graph. For instance in setConsumed in schedContextCompleteYieldTo. Basically, any time an IPC buffer pointer is passed around in a call that is not an IPC is a red flag for this protocol, and there are quite a few of them. Another complication is that a lot of this reply message setting is conditional, i.e. mostly that list that the top-level invocation should return is empty, but sometimes it is not.

I don't think we can leave it as is. I also don't think we can easily move the generation of the messages to later points higher in the call graph. Not entirely sure what a good solution is. Passing the message (which is usually one word) back up the call graph is fine in the spec, but could become awkward and unidiomatic in C, where it does make more sense to just write to the buffer directly. But this brings it out of sync with the spec if the spec follows the protocol (which in turn is the only thing that guards against the thread state bugs we see in the PR).

CParser build fails

The file tools/c-parser/CTranslation.thy references three files that do not exist:

l4v/tools/c-parser/CTranslation.thy

Lines 66 to 68 in 3abbdd7

	ML_file "StrictC.grm.sig"
	ML_file "StrictC.grm.sml"
	ML_file "StrictC.lex.sml"

It looks like these files existed in 6.0.0, but were removed some time before 7.0.0.

From the l4v directory, I ran

$ ./isabelle/bin/isabelle build -d . AutoCorres
*** I/O error: StrictC.grm.sig (No such file or directory)
*** The error(s) above occurred in session "CParser" (line 17 of "ROOT")

Unable to build Autocorres due to Z3 terminating with error code 110

Hello,

I hope this is the correct place to ask. I am trying to use autocorres to run the cogent compiler. I followed all the instructions
displayed in the .README (including isabelle) however, when I try to run the MAKEFILE in the /verification/l4v/tools/autocorres/ directory I get the following error.

Word_Lib FAILED
(see also /home/maxstoll94/.isabelle/heaps/polyml-5.8.1_x86_64_32-linux/log/Word_Lib)
### 0.598s elapsed time, 3.156s cpu time, 0.109s GC time
*** Solver z3: Solver terminated abnormally with error code 110
*** At command "by" (line 4111 of "~/verification/l4v/lib/Word_Lib/Word_Lemmas.thy")
*** Solver z3: Solver terminated abnormally with error code 110
*** At command "by" (line 4728 of "~/verification/l4v/lib/Word_Lib/Word_Lemmas.thy")
*** Solver z3: Solver terminated abnormally with error code 110
*** At command "by" (line 5521 of "~/verification/l4v/lib/Word_Lib/Word_Lemmas.thy")
*** Solver z3: Solver terminated abnormally with error code 110
*** At command "apply" (line 5554 of "~/verification/l4v/lib/Word_Lib/Word_Lemmas.thy")
*** Solver z3: Solver terminated abnormally with error code 110
*** At command "by" (line 5755 of "~/verification/l4v/lib/Word_Lib/Word_Lemmas.thy")
*** Solver z3: Solver terminated abnormally with error code 110
*** At command "by" (line 5932 of "~/verification/l4v/lib/Word_Lib/Word_Lemmas.thy")
*** Solver z3: Solver terminated abnormally with error code 110
*** At command "by" (line 6100 of "~/verification/l4v/lib/Word_Lib/Word_Lemmas.thy")
*** Solver z3: Solver terminated abnormally with error code 110
*** At command "by" (line 6105 of "~/verification/l4v/lib/Word_Lib/Word_Lemmas.thy")
*** Solver z3: Solver terminated abnormally with error code 110
*** At command "by" (line 6233 of "~/verification/l4v/lib/Word_Lib/Word_Lemmas.thy")
isabelle document -d /home/maxstoll94/.isabelle/browser_info/Lib/Word_Lib/document -o pdf -n document
*** Solver z3: Solver terminated abnormally with error code 110
*** At command "by" (line 6233 of "~/verification/l4v/lib/Word_Lib/Word_Lemmas.thy")
*** Solver z3: Solver terminated abnormally with error code 110
*** At command "by" (line 6105 of "~/verification/l4v/lib/Word_Lib/Word_Lemmas.thy")
*** Solver z3: Solver terminated abnormally with error code 110
*** At command "by" (line 6100 of "~/verification/l4v/lib/Word_Lib/Word_Lemmas.thy")
*** Solver z3: Solver terminated abnormally with error code 110
*** At command "by" (line 5932 of "~/verification/l4v/lib/Word_Lib/Word_Lemmas.thy")
*** Solver z3: Solver terminated abnormally with error code 110
*** At command "by" (line 5755 of "~/verification/l4v/lib/Word_Lib/Word_Lemmas.thy")
*** Solver z3: Solver terminated abnormally with error code 110
*** At command "apply" (line 5554 of "~/verification/l4v/lib/Word_Lib/Word_Lemmas.thy")
*** Solver z3: Solver terminated abnormally with error code 110
*** At command "by" (line 5521 of "~/verification/l4v/lib/Word_Lib/Word_Lemmas.thy")
*** Solver z3: Solver terminated abnormally with error code 110
*** At command "by" (line 4728 of "~/verification/l4v/lib/Word_Lib/Word_Lemmas.thy")
*** Solver z3: Solver terminated abnormally with error code 110
*** At command "by" (line 4111 of "~/verification/l4v/lib/Word_Lib/Word_Lemmas.thy")
*** Solver z3: Solver terminated abnormally with error code 110
*** At command "by" (line 37 of "~/verification/l4v/lib/Word_Lib/Word_EqI.thy")

At first I thought it was my z3 version, so I installed 4.8.10 (built locally from master), 4.8.9 (apt-get) and 4.4.0 (built locally). I also tried building 4.3.1 but unfortunately I am unable to build those because of some other error unrelated to this and cannot find the binaries online either.

I also noticed that even if I do not have z3 installed I get the same error, so I am not sure if it uses some other binary that I am unaware of. Please could you let me know if there is something I have missed? I am running Ubuntu 20.04.1 LTS.

different types for same word length

We currently have multiple word types in the abstract spec (and others) that are type synonyms with machine_word (obj_ref, paddr, vspace_ref etc). This means we get different names in input, but just 64 word or 32 word in output, and no feedback from the type checker if we accidentally mix them.

This hasn't been a great problem in the past, so maybe we don't need to do anything about it, but it occurs to me that for word specifically, we can get different types very easily without needing to lift theorems into the new type every time:

We can use typedef to define new types that all come out to the same word length. We need to instantiate all of these types into the len and len0 class, but that is all the boilerplate that is needed. After that, all word theorems hold for these words, the type checker will complain if they are mixed, and we can convert between them without loss with ucast.

An example is the vs_index_len type in AARCH64 (this uses typedef for another reason, but it sparked this idea).

It's not a high priority item, but if someone is looking for a side project that would make things slightly nicer, this could be a candidate.

【corres_underlying】How to use corres_underlying to prove the correspondence between two whileLoops's nondet_monad?

Dear，

I want to use predicate corres_underlying to prove the correspondence between two whileLoop or two whileLoopE, but I have not found the relevant lemma in the file corresponding_UL.thy. Does it exist in other files? Is there any good way?

Many Thanks
Gao.

missing error message for 0-length array

See discussion on seL4/seL4#443 -- the parser should produce an error message for this case, not just fail silently.

check that MCS invariants imply orphanage invariants

The "Orphanage" theory in the Refine session was added to make sure that thread states correspond to the scheduler queues, i.e. that no running threads can become orphaned by being left out of the scheduler queues.

AFAIR, the standard MCS invariants already include this property (and on the abstract spec level already, because these queues are now visible there), but I'm not sure we state this in a form that is obviously equivalent with no_orphans.

For reference no_orphans is

 ∀ tcb_ptr.
         tcb_ptr : all_active_tcb_ptrs s
         ⟶
         tcb_ptr = ksCurThread s ∨ tcb_ptr : all_queued_tcb_ptrs s ∨
         ksSchedulerAction s = SwitchToThread tcb_ptr

This issue is for checking what the actual status is and potentially adding a lemma to the abstract invariants in MCS that show something like invs s ==> no_orphans s

Make ASpec error

Hi, I'm an isabelle and seL4 beginner and try to make readable abstract spec, but I got below output when I make ASpec in macOS 11.4 and ubuntu21.04. Is there anyone who could help me figure it out? Thank you. :)

Started at Sun Sep 26 16:42:47 GMT+8 2021 (polyml-5.8.2_x86_64_32-darwin on Ivan)
ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m"
ISABELLE_BUILD_OPTIONS=""

ML_PLATFORM="x86_64_32-darwin"
ML_HOME="/Applications/Isabelle2021.app/contrib/polyml-test-f86ae3dc1686/x86_64_32-darwin"
ML_SYSTEM="polyml-5.8.2"
ML_OPTIONS="--minheap 500"

*** Bad parent session "HOL-Word" for "Word_Lib" (line 9 of "/Users/yangwenzhang/workspace/formalMethod/l4v/lib/Word_Lib/ROOT")

AutoCorres abstraction allows me to prove an invalid Hoare triple

Using AutoCorres 1.2 to abstract some C code, I discovered that I was able to prove some invalid Hoare triples. But I was not able to prove those same Hoare triples on the C-SIMPL output, which leads me to believe that this is specifically an AutoCorres issue. In brief, it seems that reading/writing from/to heap memory using a pointer, automatically asserts that the pointer is properly aligned and non-null.

I have provided code which demonstrates the issue. The function bar() increments a static pointer, which should not preserve the invariant c_guard on the pointer. Indeed, the invariant is unprovable. The function foo() also increments the pointer, but additionally writes to the pointed-to memory. This somehow makes the c_guard invariant provable.

Any assistance would be much appreciated. If this isn't the right place to post an AutoCorres issue, please let me know.

Scott Constable

Test.zip

HaskellKernel times out running tests in a clean repo

user@in-container:/host/r/l4v$ time ./run_tests  -j1 HaskellKernel
Testing for L4V_ARCH=ARM:
Testing Orphanage for ARM
Running 1 test(s)...
  Started HaskellKernel ...         
  Finished HaskellKernel             TIMEOUT *   ( 0:01:56 real,  0:30:03 cpu,  0.77GB)

------------------------------------------------------------------------
TEST TIMEOUT: HaskellKernel

...
[18 of 75] Compiling SEL4.Machine     ( src/SEL4/Machine.lhs, dist/arm/build/SEL4/Machine.o )
[19 of 75] Compiling SEL4.API.InvocationLabels ( src/SEL4/API/InvocationLabels.lhs, dist/arm/build/SEL4/API/InvocationLabels.o )
[20 of 75] Compiling SEL4.API.Failures.ARM ( src/SEL4/API/Failures/ARM.lhs, dist/arm/build/SEL4/API/Failures/ARM.o )
[21 of 75] Compiling SEL4.API.Types.ARM ( src/SEL4/API/Types/ARM.lhs, dist/arm/build/SEL4/API/Types/ARM.o )
[22 of 75] Compiling SEL4.API.Types   ( src/SEL4/API/Types.lhs, dist/arm/build/SEL4/API/Types.o )
[23 of 75] Compiling SEL4.API.Failures ( src/SEL4/API/Failures.lhs, dist/arm/build/SEL4/API/Failures.o )
[24 of 75] Compiling SEL4.Machine.Target ( src/SEL4/Machine/Target.lhs, dist/arm/build/SEL4/Machine/Target.o )
[25 of 75] Compiling SEL4.Object.Structures[boot] ( src/SEL4/Object/Structures.lhs-boot, dist/arm/build/SEL4/Object/Structures.o-boot )
[26 of 75] Compiling SEL4.Object.Structures.ARM ( src/SEL4/Object/Structures/ARM.lhs, dist/arm/build/SEL4/Object/Structures/ARM.o )
[27 of 75] Compiling SEL4.Object.Structures ( src/SEL4/Object/Structures.lhs, dist/arm/build/SEL4/Object/Structures.o )
[28 of 75] Compiling SEL4.Model.PSpace[boot] ( src/SEL4/Model/PSpace.lhs-boot, dist/arm/build/SEL4/Model/PSpace.o-boot )
[29 of 75] Compiling SEL4.API.Invocation.ARM ( src/SEL4/API/Invocation/ARM.lhs, dist/arm/build/SEL4/API/Invocation/ARM.o )
[30 of 75] Compiling SEL4.API.Invocation ( src/SEL4/API/Invocation.lhs, dist/arm/build/SEL4/API/Invocation.o )
[31 of 75] Compiling SEL4.Model.StateData.ARM ( src/SEL4/Model/StateData/ARM.lhs, dist/arm/build/SEL4/Model/StateData/ARM.o )
[32 of 75] Compiling SEL4.Model.StateData ( src/SEL4/Model/StateData.lhs, dist/arm/build/SEL4/Model/StateData.o )
[33 of 75] Compiling SEL4.Model.Preemption ( src/SEL4/Model/Preemption.lhs, dist/arm/build/SEL4/Model/Preemption.o )
[34 of 75] Compiling SEL4.Model.PSpace ( src/SEL4/Model/PSpace.lhs, dist/arm/build/SEL4/Model/PSpace.o )
[35 of 75] Compiling SEL4.Model.Failures ( src/SEL4/Model/Failures.lhs, dist/arm/build/SEL4/Model/Failures.o )
[36 of 75] Compiling SEL4.Model.Syscall ( src/SEL4/Model/Syscall.lhs, dist/arm/build/SEL4/Model/Syscall.o )
[37 of 75] Compiling SEL4.Model       ( src/SEL4/Model.lhs, dist/arm/build/SEL4/Model.o )
[38 of 75] Compiling SEL4.Object.Interrupt[boot] ( src/SEL4/Object/Interrupt.lhs-boot, dist/arm/build/SEL4/Object/Interrupt.o-boot )
[39 of 75] Compiling SEL4.Object.Instances.ARM ( src/SEL4/Object/Instances/ARM.lhs, dist/arm/build/SEL4/Object/Instances/ARM.o )
[40 of 75] Compiling SEL4.Object.Instances ( src/SEL4/Object/Instances.lhs, dist/arm/build/SEL4/Object/Instances.o )
[41 of 75] Compiling SEL4.Object.Endpoint[boot] ( src/SEL4/Object/Endpoint.lhs-boot, dist/arm/build/SEL4/Object/Endpoint.o-boot )
[42 of 75] Compiling SEL4.Object.CNode[boot] ( src/SEL4/Object/CNode.lhs-boot, dist/arm/build/SEL4/Object/CNode.o-boot )
[43 of 75] Compiling SEL4.Kernel.VSpace[boot] ( src/SEL4/Kernel/VSpace.lhs-boot, dist/arm/build/SEL4/Kernel/VSpace.o-boot )
[44 of 75] Compiling SEL4.Kernel.Thread[boot] ( src/SEL4/Kernel/Thread.lhs-boot, dist/arm/build/SEL4/Kernel/Thread.o-boot )
[45 of 75] Compiling SEL4.Kernel.Init[boot] ( src/SEL4/Kernel/Init.lhs-boot, dist/arm/build/SEL4/Kernel/Init.o-boot )
[46 of 75] Compiling SEL4.Kernel.CSpace[boot] ( src/SEL4/Kernel/CSpace.lhs-boot, dist/arm/build/SEL4/Kernel/CSpace.o-boot )
[47 of 75] Compiling SEL4.Object.Interrupt.ARM ( src/SEL4/Object/Interrupt/ARM.lhs, dist/arm/build/SEL4/Object/Interrupt/ARM.o )
[48 of 75] Compiling SEL4.Kernel.BootInfo ( src/SEL4/Kernel/BootInfo.lhs, dist/arm/build/SEL4/Kernel/BootInfo.o )
[49 of 75] Compiling SEL4.Object.TCB[boot] ( src/SEL4/Object/TCB.lhs-boot, dist/arm/build/SEL4/Object/TCB.o-boot )
[50 of 75] Compiling SEL4.Object.Notification ( src/SEL4/Object/Notification.lhs, dist/arm/build/SEL4/Object/Notification.o )
[51 of 75] Compiling SEL4.Object.Interrupt ( src/SEL4/Object/Interrupt.lhs, dist/arm/build/SEL4/Object/Interrupt.o )
[52 of 75] Compiling SEL4.Object.Endpoint ( src/SEL4/Object/Endpoint.lhs, dist/arm/build/SEL4/Object/Endpoint.o )
[53 of 75] Compiling SEL4.Kernel.VSpace.ARM ( src/SEL4/Kernel/VSpace/ARM.lhs, dist/arm/build/SEL4/Kernel/VSpace/ARM.o )
make: *** [Makefile:40: build-arm] Interrupt
No timing log for HaskellKernel was found.
  (in /isabelle/ARM/log/HaskellKernel_times.txt)

------------------------------------------------------------------------


0/1 tests succeeded.

Tests failed.


real    1m56.859s
user    10m48.749s
sys     7m39.359s
user@in-container:/host/r/l4v$ nproc
64
user@in-container:/host/r/l4v$ git clean -dfx
Removing misc/regression/__pycache__/
Removing spec/haskell/.cabal-sandbox/
Removing spec/haskell/.stack-work/
Removing spec/haskell/cabal.sandbox.config
Removing spec/haskell/dist/
Removing spec/haskell/src/SEL4/Kernel/CSpace.lhs-boot
Removing spec/haskell/src/SEL4/Kernel/FaultHandler.lhs-boot
Removing spec/haskell/src/SEL4/Kernel/Init.lhs-boot
Removing spec/haskell/src/SEL4/Kernel/Thread.lhs-boot
Removing spec/haskell/src/SEL4/Kernel/VSpace.lhs-boot
Removing spec/haskell/src/SEL4/Model/PSpace.lhs-boot
Removing spec/haskell/src/SEL4/Object/CNode.lhs-boot
Removing spec/haskell/src/SEL4/Object/Endpoint.lhs-boot
Removing spec/haskell/src/SEL4/Object/IOPort/X64.lhs-boot
Removing spec/haskell/src/SEL4/Object/Interrupt.lhs-boot
Removing spec/haskell/src/SEL4/Object/ObjectType.lhs-boot
Removing spec/haskell/src/SEL4/Object/TCB.lhs-boot
Removing spec/haskell/stack.yaml.lock
user@in-container:/host/r/l4v$ time ./run_tests  -j1 HaskellKernel --no-timeouts
Testing for L4V_ARCH=ARM:
Testing Orphanage for ARM
Running 1 test(s)...
  Started HaskellKernel ...         
  Finished HaskellKernel             passed      ( 0:02:48 real,  1:23:51 cpu,  0.75GB)


1/1 tests succeeded.

All tests passed.


real    2m49.177s
user    48m45.059s
sys     35m36.153s

Some examples of using whileLoop in Monad_WP

Dear,
Do you have some examples of using whileLoop in Monad_WP?
In the source code, I only found the definition, but no examples and explaination.
It is really not easy to follow it.

Thanks.

add CI for different `numDomains` settings

When PR #410 is merged, the proofs will be generic in the number of protection domains.

Testing that fact with every CI job is going to be too resource-intensive, but we should test at least values of 1, 2, and something like 16 in the weekly job so we get an alert when we accidentally break this genericity.

Question: Is Owicki-Gries's Hoare logic used in seL4 verification?

I am fairly new to Isabelle, I recently found out that Owicki-Gries's Hoare logic is implemented in Isabelle/HO - Hoare_Parallel theory.

In sel4, I thought that the same theory would be used for most of the kernel components but cannot find this theory used in any of the sel4 lemmas.

For example, taking the interrupts intro consideration, the "irq_timer" is enabled for x86 processors, but crefine/x86 theories don't mention using the OG logic.

My question is how the interrupts, endpoints or any other form of concurrency and synchronization is handled in sel4?
If you can point some documentation or the related theories in this repo, I would be grateful.

Lib.find vs. List.find

Hi,

I'm using l4v at revision 7e9b822.

I noticed that in Lib there is a function find which is equal to Isabelle's List.find (loaded by Main).

Is there a specific reason for this?

more testing

...

Autocorres on Win10

I use Isabelle on Windows, and Autocorres 1.6.1. However, an error occured as follows:

install_C_file "alloc.c"

The output tab shows:
Illegal character ":" in path element "D:\temp\MLTEMPb06820"
The error(s) above occurred in "D:\temp\MLTEMPb06820"

How can I modify the sources to remove it?
Thanks.

overview document for available custom commands in lib/

We have lots of custom commands and automation available in lib/ but they are hard to discover, some are undocumented, and are therefore in danger of falling out of use or being reinvented.

We should at the very least an overview document that summarises what each command does in a paragraph (still short, but more detail and less cryptic than what print_commands will give you).

This could be an .md file in docs.

AutoCorres 1.8 fails to build on Isabelle 2021-1 - Cannot load theory "HOL-Library.Bit_Operations"

Hi. Being interested in formal verification of C programs as well as getting a better understanding the extent of the seL4 proof, I decided to download Isabelle and follow UNSW's COMP4161. After two readings, most of the content of the course is clear to me, and I have even managed to prove a few unrelated things on my own, but when comes time to use AutoCorres, I get stuck right at the building phase.

My GNU/Linux distribution is Arch, and I installed Isabelle 2021-1 by unpacking its archive into /opt/isabelle/ and placing the following shell script in /usr/bin/isabelle (probably not written by me since that's not how I would do it):

#!/usr/bin/env bash

exec "/opt/isabelle/bin/isabelle" "$@"

I then extracted the AutoCorres 1.8 archive in the same directory as the theory files for the course and ran the following command from that same directory:

L4V_ARCH=X64 isabelle build -v -b -d autocorres-1.8 AutoCorres

The building fails with the following log (hostname and home directory name omitted):

Started at Mon Jun 6 21:43:18 GMT+2 2022 (polyml-5.9_x86_64_32-linux on hostname)
ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m"
ISABELLE_BUILD_OPTIONS=""

ML_PLATFORM="x86_64_32-linux"
ML_HOME="/opt/isabelle/contrib/polyml-5.9/x86_64_32-linux"
ML_SYSTEM="polyml-5.9"
ML_OPTIONS="--minheap 500"

Session Pure/Pure
Session FOL/FOL
Session Tools/Tools
Session HOL/HOL (main)
Session HOL/HOL-Library (main timing)
Session HOL/HOL-Combinatorics (main timing)
Session HOL/HOL-Computational_Algebra (main timing)
Session HOL/HOL-Analysis (main timing)
Session HOL/HOL-Eisbach
Session HOL/HOL-Statespace
Session Lib/Word_Lib (lib)
*** Cannot load theory "HOL-Library.Bit_Operations"
*** The error(s) above occurred in session "Word_Lib" (line 9 of "~/doc/COMP4161/autocorres-1.8/lib/Word_Lib/ROOT")

The file /opt/isabelle/src/HOL/Bit_Operations.thy exists, though when open with jEdit it shows the following error on line 6:

Cannot update finished theory "HOL.Bit_Operations"

This is probably not an actual error since it does the same thing on Main.thy. I have tried reinstalling Isabelle with no success, and I cannot find older Isabelle versions which don't seem to be archived. I also could not find this issue being mentioned while searching for Isabelle or AutoCorres.

What may be the source of this error?

Thank you for your attention.

Writing general heap proofs with locales (Autocorres)

So I have a bunch of theorems that use autocorres heap constructs (in particular "heap_w32, heap_w32_update, etc.") that I would like to use across multiple runs of AutoCorres. The way it looks like this is done internally is with the "valid_typ_heap" function.

However, as is written here (page 154), this is a good use case for locales. So, to start with, I have the locale:

locale heap_abs =
  fixes st :: "'s ⇒ 't"
    and getter :: "'t ⇒ word32 ptr ⇒ word32"
    and setter :: "((word32 ptr ⇒ word32) ⇒ (word32 ptr ⇒ word32)) ⇒ 't ⇒ 't"
    and vgetter :: "'t ⇒ word32 ptr ⇒ bool"
    and vsetter :: "((word32 ptr ⇒ bool) ⇒ (word32 ptr ⇒ bool)) ⇒ 't ⇒ 't"
    and t_hrs :: "'s ⇒ heap_raw_state"
    and t_hrs_update :: "(heap_raw_state ⇒ heap_raw_state) ⇒ 's ⇒ 's"
  assumes is_valid_typ_heap: "valid_typ_heap st getter setter vgetter vsetter t_hrs t_hrs_update"

This is alright for my use cases (meaning I can transfer my proofs into the locale no problem). Then when I want to create an interpretation of this to use with a specific C file, I can write (in a given file after loading AutoCorres):

interpretation H: heap_abs 
  "lift_global_heap :: globals ⇒ lifted_globals"
  "heap_w32 :: lifted_globals ⇒ word32 ptr ⇒ word32"
  "heap_w32_update :: ((word32 ptr ⇒ word32) ⇒ (word32 ptr ⇒ word32)) ⇒ lifted_globals ⇒ lifted_globals"
  "is_valid_w32 :: lifted_globals ⇒ word32 ptr ⇒ bool"
  "is_valid_w32_update :: ((word32 ptr ⇒ bool) ⇒ (word32 ptr ⇒ bool)) ⇒ lifted_globals ⇒ lifted_globals"
  "t_hrs_' :: globals ⇒ heap_raw_state"
  "t_hrs_'_update :: (heap_raw_state ⇒ heap_raw_state) ⇒ globals ⇒ globals"

The problem is proving this interpretation is correct. I know through much reading and troubleshooting that internally, AutoCorres proves that:

valid_typ_heap lift_global_heap heap_w32 heap_w32_update
    is_valid_w32 is_valid_w32_update t_hrs_' t_hrs_'_update

However, I see no way to convince isabelle of that fact. Until now, I had manually re-proved the valid_typ_heap condition, but this is very fragile, and breaks when, for example, new types are introduced to the C file. Is there any way I could access the valid_typ_heap proof to prove my interpretation here?

Are there any other suggestions for writing these general proofs? Using valid_typ_heap as a precondition is too restrictive in general, as it makes it much more difficult to generalize constructs such as functions that would otherwise live within the locale.

psutil methods with get_ prefix are deprecated

psutil as of 2.0.0 renamed all getters to avoid the get_ prefix, in March 2014, leaving behind a deprecation warning.

The 3.0.0 release in June this year removed them.

Unfortunately, Ubuntu/Debian still ship an ancient psutil version. Other Linux distros are using the new version, and the new versions are what can be obtained from pip. I'm not sure what the best way forward is here.

'nslookup' tool missing while executing "./build.sh -b l4v"

I cloned this repo and executed this command "./build.sh -b l4v", then got message :

.....
cabal-install    > Linking .stack-work/dist/x86_64-linux-tinfo6/Cabal-3.4.1.0/build/cabal/cabal ...
cabal-install    > copy/register
cabal-install    > Installing executable cabal in /root/.stack/snapshots/x86_64-linux-tinfo6/f04d0d45be1db2d1a4535c7134bb900ee49fac5cd84a673d5abb9a8554c6afdd/9.0.2/bin
Completed 22 action(s).
stack exec -- ./stack-path cabal v2-update
Config file path source is default config file.
Config file /root/.cabal/config not found.
Writing default configuration to /root/.cabal/config
Warning: 'nslookup' tool missing - can't locate mirrors

I waited for an hour and it seems stucked here.

So i added dnsutils in scripts/l4v.sh and got no warning about nslookup. But it still stucked here:

.....
cabal-install    > Linking .stack-work/dist/x86_64-linux-tinfo6/Cabal-3.4.1.0/build/cabal/cabal ...
cabal-install    > copy/register
cabal-install    > Installing executable cabal in /root/.stack/snapshots/x86_64-linux-tinfo6/f04d0d45be1db2d1a4535c7134bb900ee49fac5cd84a673d5abb9a8554c6afdd/9.0.2/bin
Completed 22 action(s).
stack exec -- ./stack-path cabal v2-update
Config file path source is default config file.
Config file /root/.cabal/config not found.
Writing default configuration to /root/.cabal/config

Did I miss something? Any idea to solve this problem? Thanks a lot.

c-parser timeout error

hello
l4v version：l4v-isabelle-2021,isabelle version:Isabelle2021

C-parser compile has this error,command is isabelle env make CParser. help me!thanks!

ubuntu@ubuntu:/l4v-isabelle-2021/tools/c-parser$ export L4V_ARCH=X64
ubuntu@ubuntu:/l4v-isabelle-2021/tools/c-parser$ isabelle env make CParser
/home/ubuntu/isabelle/bin/isabelle build -d ../.. -b -v CParser
Started at Thu Jul 22 09:11:37 GMT 2021 (polyml-5.8.2_x86_64_32-linux on ubuntu)
ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m"
ISABELLE_BUILD_OPTIONS=""

ML_PLATFORM="x86_64_32-linux"
ML_HOME="/home/ubuntu/isabelle/contrib/polyml-test-f86ae3dc1686/x86_64_32-linux"
ML_SYSTEM="polyml-5.8.2"
ML_OPTIONS="--minheap 500"

Session Pure/Pure
Session FOL/FOL
Session Tools/Tools
Session HOL/HOL (main)
Session HOL/HOL-Library (main timing)
Session HOL/HOL-Computational_Algebra (main timing)
Session HOL/HOL-Analysis (main timing)
Session HOL/HOL-Eisbach
Session HOL/HOL-Statespace
Session Lib/Word_Lib (lib)
Session Lib/Lib (lib)
Session C-Parser/Simpl-VCG
Session C-Parser/CParser
Building Word_Lib ...
Word_Lib: theory HOL-Eisbach.Eisbach
Word_Lib: theory HOL-Eisbach.Eisbach_Tools
Word_Lib: theory HOL-Library.Boolean_Algebra
Word_Lib: theory HOL-Library.Bit_Operations
Word_Lib: theory HOL-Library.Phantom_Type
Word_Lib: theory HOL-Library.Cardinality
Word_Lib: theory HOL-Library.Numeral_Type
Word_Lib: theory HOL-Library.Type_Length
Word_Lib: theory HOL-Library.Word
Word_Lib: theory Word_Lib.Bit_Comprehension
Word_Lib: theory Word_Lib.Hex_Words
Word_Lib: theory Word_Lib.Legacy_Aliases
Word_Lib: theory Word_Lib.More_Divides
Word_Lib: theory Word_Lib.Signed_Words
Word_Lib: theory Word_Lib.Word_Names
Word_Lib: theory Word_Lib.Type_Syntax
Word_Lib: theory Word_Lib.Word_Syntax
Word_Lib: theory HOL-Library.Signed_Division
Word_Lib: theory Word_Lib.Signed_Division_Word
Word_Lib: theory HOL-Library.Sublist
Word_Lib: theory HOL-Library.Prefix_Order
Word_Lib: theory Word_Lib.More_Sublist
Word_Lib: theory Word_Lib.Enumeration
Word_Lib: theory Word_Lib.Even_More_List
Word_Lib: theory Word_Lib.More_Arithmetic
Word_Lib: theory Word_Lib.More_Word
Word_Lib: theory Word_Lib.Enumeration_Word
Word_Lib: theory Word_Lib.Many_More
Word_Lib: theory Word_Lib.Distinct_Prop
Word_Lib: theory Word_Lib.Strict_part_mono
Word_Lib: theory Word_Lib.Traditional_Infix_Syntax
Word_Lib: theory Word_Lib.Bits_Int
Word_Lib: theory Word_Lib.Least_significant_bit
Word_Lib: theory Word_Lib.Norm_Words
Word_Lib: theory Word_Lib.Rsplit
Word_Lib: theory Word_Lib.Word_16
Word_Lib: theory Word_Lib.Word_EqI
Word_Lib: theory Word_Lib.Most_significant_bit
Word_Lib: theory Word_Lib.Generic_set_bit
Word_Lib: theory Word_Lib.More_Misc
Word_Lib: theory Word_Lib.Typedef_Morphisms
Word_Lib: theory Word_Lib.Aligned
Word_Lib: theory Word_Lib.Next_and_Prev
Word_Lib: theory Word_Lib.Word_Lemmas
*** Timeout
Word_Lib FAILED
(see also /home/ubuntu/.isabelle/Isabelle2021/heaps/polyml-5.8.2_x86_64_32-linux/log/Word_Lib)
*** Interrupt
Simpl-VCG CANCELLED
CParser CANCELLED
Unfinished session(s): CParser, Simpl-VCG, Word_Lib

Finished at Thu Jul 22 09:16:58 GMT 2021
0:05:20 elapsed time, 0:04:54 cpu time, factor 0.92
Makefile:42: recipe for target 'CParser' failed
make: *** [CParser] Error 142
ubuntu@ubuntu:/l4v-isabelle-2021/tools/c-parser$ cat /home/ubuntu/.isabelle/Isabelle2021/heaps/polyml-5.8.2_x86_64_32-linux/log/Word_Lib
*** Interrupt
ubuntu@ubuntu:/l4v-isabelle-2021/tools/c-parser$

Reduce AutoCorres dependencies

Check if there are further dependencies (in addition to #543) that can be removed from AutoCorres.

C- Parser install and use questions/ solved!

The environment variable $L4V_ARCH was not seen by invoking Isabelle by double clicking on it. But using the run from shell isabelle/bin/isabelle jedit filename from the command shell it was seen and now I can see the output.

Thanks

Haskellkernel test in the latest Sel4 release on ubuntu 16.04-1 LTL (Xenial Xerus)

Hi All,

First of all, i would to say , thanks a lot for Sel4 developers for their great job!

Next, I would like to share this experience and its solution. Probably, some people will find it useful.

---

After running the test haskellkernel on ubuntu 16.04-1 LTL (Xenial Xerus) you may get this error:

src/SEL4/Object/Interrupt.lhs-boot
cabal sandbox init
make: cabal: Command not found
Makefile:23: recipe for target 'build' failed
make: *** [build] Error 127

But after using "curl -sSL https://get.haskellstack.org/ | sh " you may get another error like :

TEST FAILED: HaskellKernel

cabal sandbox init
Writing a default package environment file to
/home/ssrgv/Desktop/verification/l4v/spec/haskell/cabal.sandbox.config
Creating a new sandbox at
/home/ssrgv/Desktop/verification/l4v/spec/haskell/.cabal-sandbox
cabal install --dependencies-only -w "ghc"
Resolving dependencies...
cabal: Could not resolve dependencies:
trying: SEL4-ARM-1.4 (user goal)
next goal: base (dependency of SEL4-ARM-1.4)
rejecting: base-4.8.2.0/installed-0d6... (conflict: SEL4-ARM => base==4.7.*)
rejecting: base-4.9.0.0, 4.8.2.0, 4.8.1.0, 4.8.0.0, 4.7.0.2, 4.7.0.1, 4.7.0.0,
4.6.0.1, 4.6.0.0, 4.5.1.0, 4.5.0.0, 4.4.1.0, 4.4.0.0, 4.3.1.0, 4.3.0.0,
4.2.0.2, 4.2.0.1, 4.2.0.0, 4.1.0.0, 4.0.0.0, 3.0.3.2, 3.0.3.1 (global
constraint requires installed instance)
Dependency tree exhaustively searched.

Note: when using a sandbox, all packages are required to have consistent
dependencies. Try reinstalling/unregistering the offending packages or
recreating the sandbox.
Makefile:23: recipe for target 'build' failed
make: *** [build] Error 1

Solution: So after running curl -sSL https://get.haskellstack.org/ | sh, check the ghc version on your on ubuntu 16.04-1 LTL (Xenial Xerus) machine, if it was 7.10.* then that might be the reason for the above error.

Searching for a reason behind this indicated that ghc 7.10.* is currently unstable and sometimes does not work properly with cabal 1.22. So to use version cabal 1.20 and ghc 7.8.* together (as recommended in Sel4 pages) without problems on my machine I used the following steps:-

sudo apt-get update
sudo apt-get install -y software-properties-common
sudo add-apt-repository -y ppa:hvr/ghc
sudo apt-get update
sudo apt-get install -y cabal-install-1.20 ghc-7.8.3
cat >> /.bashrc <<EOF
export PATH=/.cabal/bin:/opt/cabal/1.20/bin:/opt/ghc/7.8.3/bin:$PATH
EOF
export PATH=~/.cabal/bin:/opt/cabal/1.20/bin:/opt/ghc/7.8.3/bin:$PATH
cabal update
cabal install alex happy

After this solution the test ran successfully!

If someone ran into similar problem I hope you will find this discussion useful.

Thanks!

HaskellKernel fails to build on OS X El Capitan

Due to this issue: commercialhaskell/stack#563

As far as I know the only option is to upgrade to GHC >= 7.10, how bad it will break? Cabal file mentions problems with newer base and mtl, which look to be easily fixable...

backport Lib enhancements from `rt` branch

The MCS proofs for AInvs and Refine produced a number of enhancements and additional lemmas in the Lib session.

We should backport these to master to reduce merge effort later and to make use of them in new proofs.