Conversation
Make the name of the procedure environment Gamma configurable. This enables operations on Gamma later. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Add option for providing the name of the procedure environment \Gamma. Useful when the C parser is instructed to create a custom name for the procedure environment. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- rename the procedure environment of the original kernel source from Gamma to Gamma0 so that we can introduce a new layer Gamma for procedures with bodies that depend on which core they run on. - override Gamma0 in kernel_all_substitute0 with a version where physBase depends on cpuNum - do the same for kernel_all_global_addresses - automatically prove *_impl theorems for the new Gamma in kernel_all_substitute - automatically prove *_modifies theorems for the new Gamma in kernel_all_substitute - remove *_modifies theorem generation from kernel_all_substitute0, since we don't need them there Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Adjust the automatic refinement proof to work for Gammas where one function is overridden. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- use kernel_all_global_addresses base locale for constants -- these are not modified by kernel_all_substitute and the base version is the most stable name. - assume `cpuNum = 0` in Machine_C for current unicore proof; use explicit cpuNum assumption in the one lemma before Machine_C that depends on cpuNum. - adjust theory imports + locale names and parameters as needed Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Adjust references to the C ADT to include the new cpuNum parameter. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Update the locale name to kernel_all_substitute0 and Gamma to Gamma0 for the step down to binary verification. Binary verification uses the parsed version of the kernel, not the parameterised version of the kernel since the binary is not parameterised. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Use the SIMPL procedure environment to make CKernel and CSpec parametric, adjusting the C proofs accordingly. The PR has an example of a parametric function
physBase_of_cpu.This is a milestone in the Dyvercon project for Cyberagentur. The current state is the version approved for public release. It will need to be rebased before it can be merged.
The current version manually takes the current value of
physBasein C. Before the PR can be merged, we should add a proof check against the actual C version, which is still available visible in the original procedure context.