add some doc#114
Open
KimayaBedarkar wants to merge 15 commits into
Open
Conversation
mtzguido
reviewed
Jun 3, 2026
| @@ -0,0 +1,16 @@ | |||
| This doc explains how structs are modelled in pal. Whenever you define a struct `foo`, PAL generates a file `Struct_foo.fst`. This file contains the following: | |||
|
|
|||
| 1. `noeq type struct_foo`: This is the F* record that is the lightweight representation of the struct. | |||
Member
There was a problem hiding this comment.
What is "lightweight"? Maybe a running example through the file would help too!
Collaborator
Author
There was a problem hiding this comment.
Yeah. I am hesitant to use the word "refinement" since it is very overloaded in this context
| This doc explains how structs are modelled in pal. Whenever you define a struct `foo`, PAL generates a file `Struct_foo.fst`. This file contains the following: | ||
|
|
||
| 1. `noeq type struct_foo`: This is the F* record that is the lightweight representation of the struct. | ||
| 2. `noeq type struct_foo__spec`: A collection of all the data that pointers in the struct point to. Marked `[@@erasable]` (ghost-only). If the struct has no pointer fields, this type — together with its `pred_unfold`/`pred_fold` ghost fns — is omitted and `struct_foo__pred` collapses to `emp`. |
Member
There was a problem hiding this comment.
If the struct has no pointer fields, this type — together with its
pred_unfold/pred_foldghost fns — is omitted andstruct_foo__predcollapses toemp.
Is this true? I thought that for a struct like struct foo { int x; int y; } the __spec type would be something like type foo__spec = { x : Int32.t; y : Int32.t }. I.e., it still exists even if there are no pointers.
Collaborator
Author
There was a problem hiding this comment.
This is true. I double checked.
Member
There was a problem hiding this comment.
ok! I'm probably just confused. Perhaps a running example of a struct with fields of type int/int*/int** would help.
| ## See also | ||
|
|
||
| - `structs.md` / `unions.md` — what gets generated per struct / union. | ||
| - `arrays.md` — the array representation, points-to flavors, and the `_array` / `_arrayptr` distinction. |
Member
There was a problem hiding this comment.
missing arrays.md and unions.md?
KimayaBedarkar
force-pushed
the
kimaya/doc
branch
from
500a982 to
dce6bf0
Compare
Contributor
|
@KimayaBedarkar please merge when you think it's ready |
Replace doc/skill.md with the handwritten guide (my_skill.md). Antiquotation syntax is documented in pal_surface_syntax.md instead.
Add an Antiquotation subsection under Pulse interop: a reference table of every $-form ($(expr), $&(expr), $type, $field, $`tick, $declare, $fold/$unfold incl. -uninit and union U::f) plus notes on context sensitivity, pointer-view suppression, and the special names this/return. Update the brief line-47 mention to point at it.
KimayaBedarkar
force-pushed
the
kimaya/doc
branch
from
138b225 to
6825ac9
Compare
- Title: 'Proof-oriented Annotation Language' -> 'Proof Annotated Language for C', matching the project README. - _out no longer described as merely returning ownership (that is the default). It requires only uninitialized storage (pts_to_uninit precondition) and returns it initialized (pts_to postcondition).
functioncal->functional, defintions/definitons->definitions, seperate(ly)->separate(ly), 'by declared'->'be declared', 'the the'->'the', accessble->accessible, 'names constants'->'named constants', _ghost_smtm()->_ghost_stmt(), and a stray double space.
- \xc2\xa74 subsections: demote '##' to '###' and de-duplicate the two '4.1' headings (now 4.1-4.5). - \xc2\xa77 subsections renumbered from a stale 13.1-13.5 to 7.1-7.5; fix the '(two common situations)' lead-in. - Remove references to sections that do not exist in this guide (\xc2\xa77, \xc2\xa78.1, \xc2\xa74 matcher, \xc2\xa710.1/10.2/10.7/10.13); reword the affected sentences to stand on their own.
Replace the partial (and slightly divergent) antiquotation list in 5.1 with a pointer to the canonical Antiquotation section in pal_surface_syntax.md, keeping only the Pulse ghost-fn body syntax that is specific to writing proofs.
- README index: 'structs.md (and unions, briefly)' becomes separate structs.md and unions.md entries, plus a new 'Proving and internals' section linking skill.md and internals.md. - structs.md: the brief unions note now points to unions.md for detail. (unions.md is referenced but not yet added.)
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
3 participants
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.
No description provided.