work: import existing documentation - #16
Draft
pgiarrusso-sl wants to merge 2 commits into
Draft
pgiarrusso-sl wants to merge 2 commits into
pgiarrusso-sl wants to merge 2 commits into
Conversation
Reformatted + added sections
pgiarrusso-sl
marked this pull request as draft
May 8, 2026 12:57
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | b9f28b5 |
| fmdeps/BRiCk/ | main | d94485e |
| fmdeps/auto/ | main | 63d5e05 |
| bluerock/NOVA/ | skylabs-proof | 6cbef03 |
| bluerock/bhv/ | skylabs-main | 448828c |
| fmdeps/brick-libcpp/ | main | 2014908 |
| fmdeps/ci/ | main | 680889d |
| vendored/elpi/ | skylabs-master | aa4475f |
| vendored/flocq/ | skylabs-master | cf9cc84 |
| fmdeps/fm-tools/ | main | fb160a9 |
| psi/protos/ | main | 8fe3e7c |
| psi/backend/ | main | 0b5fea6 |
| psi/ide/ | main | 6b596cf |
| psi/data/ | main | 76acc2f |
| vendored/rocq/ | skylabs-master | 2ede3c9 |
| fmdeps/rocq-agent-toolkit/ | main | ac7e4ec |
| vendored/rocq-elpi/ | skylabs-master | 103a742 |
| vendored/rocq-equations/ | skylabs-main | a8c4832 |
| vendored/rocq-ext-lib/ | skylabs-master | 94a6630 |
| vendored/rocq-iris/ | skylabs-master | 3ad4ddd |
| vendored/rocq-lsp/ | skylabs-main | a8b7272 |
| vendored/rocq-stdlib/ | skylabs-master | bc07423 |
| vendored/rocq-stdpp/ | skylabs-master | e01d802 |
| fmdeps/skylabs-fm/ | main | e8b88a7 |
| vendored/vsrocq/ | skylabs-main | 5b4527e |
Performance
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -0.18% | 125661.1 | 125439.4 | -221.7 | total |
| -0.18% | 221.7 | - | -221.7 | ├ disappeared files (13) |
| +0.00% | 125439.4 | 125439.4 | +0.0 | └ common files |
| +0.00% | 22788.6 | 22788.6 | +0.0 | ├ translation units |
| +0.00% | 102650.9 | 102650.9 | +0.0 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -0.18% | 125661.1 | 125439.4 | -221.7 | total |
| -0.18% | 221.7 | - | -221.7 | ├ disappeared files (13) |
| +0.00% | 125439.4 | 125439.4 | +0.0 | └ common files |
| +0.00% | 22788.6 | 22788.6 | +0.0 | ├ translation units |
| +0.00% | 102650.9 | 102650.9 | +0.0 | └ proofs and tests |
pgiarrusso-sl
commented
May 15, 2026
| form `Q ** F'`. | ||
| 3. If `P` and `Q` are unifiable, use *FRAME* to remove the common conjuncts | ||
| reducing the goal to solve the (smaller) entailment `F |-- F'`. | ||
| If the head formulas are not unifiable, then try another permutation. |
Contributor
Author
There was a problem hiding this comment.
(this is specific to workv2 so we don't want it now).
pgiarrusso-sl
commented
May 15, 2026
Comment on lines
+167
to
+187
| ## Iterated Triggers | ||
|
|
||
| In rare instances it is necessary to match multiple conjuncts on the right- or left-side, i.e. either the forward or backward trigger is non-atomic. This can be expressed using separation logic side conditions. As an example, `A ** B |-- X` for *concrete* `A`, `B`, and `X` can be applied using the following forward lemma. | ||
|
|
||
| F |-- B ** F' <-- treated as a side-condition | ||
| X ** F' |-- G | ||
| ---------------- | ||
| A ** F |-- G | ||
|
|
||
| Due to the way that `True` works in separation logic, we can also find duplicable assertions and use them without cancelling them. | ||
|
|
||
| F |-- B ** True <-- treated as a side-condition | ||
| X ** F |-- G | ||
| ---------------- | ||
| A ** F |-- G | ||
|
|
||
| If `B` is a persistent fact, then information from it can be used in the entailment without needing to consume the resource. Furthermore, the automation understands `True` and will immediately solve any goal with an `True` on the right hand side. | ||
|
|
||
| *N.B.*: Due to the specifics of how the automation works, it is best to phrase iterated triggers using the most discriminating triggers first. For example, if `A` occurs much more frequently than `B`, the first of the examples should be phrased with `B` and `A` exchanged. | ||
|
|
||
| Exercise: Write reasoning lemmas to expose the following fact to the automation: `A ** B ** C |-- D ** E`. Orient it as each of a cancellation lemma, a forward lemma, and a backward lemma. |
Contributor
Author
There was a problem hiding this comment.
Multi-match makes this irrelevant.
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.
These manuals existed in
autobut were not published yet.Fix https://github.com/SkyLabsAI/agent-foundation/issues/35.