Skip to content

preview of current formatting progress #175

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 4 commits into
base: master
Choose a base branch
from

Conversation

pickx
Copy link

@pickx pickx commented Jun 10, 2025

No description provided.

Copy link
Contributor

@johspaeth johspaeth left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A few comments for feedback.

Comment on lines 13 to 16
use
// @notice Imports the invariant invInBase
// @notice Overriding the preserved block in base.spec
invariant invInBase;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

MUST: This seems off. Please check. There shouldn't be a line break after use. It's probably due to the comments here?

MUST: Where did the preserved block go?

Copy link
Author

@pickx pickx Jun 21, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

fixed the "MUST"s you pointed out.

the file still has somewhat suboptimal comment placement, and this is because invariant comment matching is kinda bad right now.
I have ideas how to fix this (based on previously-used strategies) but I don't think it's awful. not for the kind of output we expect at the moment.

env e;
address x;
assert x.foo(e) >= 1 && x.foo(e) <= 2;
}
}
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

you shouldn't be removing the newline-at-end-of-file

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

sure, let's go with that. 👍

Copy link
Author

@pickx pickx Jun 22, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

so do you think we should

  1. respect user's opinion (no new line if it doesn't end with a newline, keep newline if it does)
  2. always normalize to no newline (like the code used to generate this example)
  3. always normalize to newline

I see rustfmt went with 3 so I am now doing that too.
unless you think 1 is the better option and we should respect existing choices, in which case let's discuss this.

Copy link
Contributor

@christiane-certora christiane-certora left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's looking pretty good already, I think we're getting very close!

assert ecrecover(msgHashA, v, r, s) != 0 => ecrecover(msgHashB, v, r, s) == 0;
}

rule dependencyOnS() {
rule dependencyOnS() //!= ecrecover(msgHash, v, r, s1) ;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this guy is still jumping funny - I guess maybe because he is before the } token? Might need a check as to how the comment is positioned relative to the children to make it go at the end.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'll try to implement the "prefer current scope" logic for matching, the assert statement should take precedence here based on that

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it would also be ok if it associates with the block, and you just have logic in the tokenize of the block to say "after proper children + before associated token => inside the block at the end"

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(while after children + after token => after the closing brace,
before children + before token => before the opening brace,
before children + after token => after the opening brace)

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

following offline discussion + some experimentation, I special cased comments in blocks as follows:

  • if comment binds after list, keep it as is.
  • if comment binds before list and the token it binds to is the block's terminating brace (which we can find without "parser knowledge", by assuming the range of the block ends with that brace), then insert it it as its own line. otherwise, insert it before the list.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

keeping this open for visibility.

// Summarization by a CVL function. The result is non-deterministic because the CVL function is not deterministic.
function reduceBalance(uint256 amount) internal returns (uint256) with (env e) => cvlReduceBalance(e, amount);
// Summarization by a CVL function. The result is non-deterministic because the CVL function is not deterministic.
function reduceBalance(uint256 amount) internal returns (uint256) with(env e) => cvlReduceBalance(e, amount);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this one makes a nice case for space after with - it would look more homogeneous with the returns

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It doesn't have the space here, although you did add it in other occurrences of with now, not sure why

Copy link
Contributor

@johspaeth johspaeth left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just some few comments and observations

Copy link
Contributor

@johspaeth johspaeth left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Minor nits. Overall looks mergable!

Comment on lines 30 to 44
function isSigned(
address _addr,
bytes32 msgHash,
uint8 v,
bytes32 r,
bytes32 s
) external returns (bool) envfree;
function executeMyFunctionFromSignature(
uint8 v,
bytes32 r,
bytes32 s,
address owner,
uint256 myParam,
uint256 deadline
) external;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do we really want these line breaks here? Looks strange to me?

Copy link
Author

@pickx pickx Jun 23, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

looks like typical formatters that I've used but regardless (as discussed) we will disable this feature (for now?)

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

My comment was a bit rushed - what I really meant:

By adding new line breaks here we explode the methods block and it's hard to read what we are summarizing a function with (the important info is typically after the =>). I just feel this could be something folks complain about sooner than later.

I don't have a strong opinion here. You can make the final call!

Copy link
Author

@pickx pickx Jun 23, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I definitely sympathize with both sides on this subject.

while programming in languages that have a formatter I find that they're often quite eager with doing expansions like this. sometimes I even choose to rewrite code in a certain way because it's just at the threshold of the formatter turning it into a multiline monstrosity, and I don't feel like it's warranted. and this is annoying, and adds friction with a feature that should feel seamless (the code formatter)

this also gives a bad first impression of this product if your source code is suddenly twice as long
so this feels like something we should tweak as we go along, with input from Nurit, Hristo etc.

Comment on lines +31 to +32
rule parametricRuleInBase(method f)
filtered { f -> filterDef(f) } {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

nit - maybe indent the filtered so that it's clear it still belongs to the invariant?

Copy link
Contributor

@christiane-certora christiane-certora left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Mostly nitpicking now to record what may still be nice to polish, not necessarily in this MS.

invariant specificPreservedInv()
base1.inExtension2 == 0 {

// Verify the specific preserved on an extension contract function works.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Here we're inserting an extra blank line now - not a dealbreaker for me, but just noting it for possible improvement (maybe not in this MS).

Copy link
Author

@pickx pickx Jun 23, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

these blank lines before/after are probably a simple fix. basically I have this code now that decides how to pad comments before/after the content, and I guess it doesn't do the right thing here.

}
use rule twoParametricRuleInBase // @notice Add a filter to g (using an overridden definition)

filtered { f -> isPlusSevenSomeUInt(f), g -> filterDef(g) } // @notice Override the filter of f
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is an interesting one, I have some suspicions about parts of what's going on here. Let me know if you want someone to discuss with to figure out how to make this case behave.

Copy link
Author

@pickx pickx Jun 23, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I haven't investigated this specific case yet, but here's my hunch based on similar issues I've already fixed

  1. it is indeed true that the issue with comments is that we don't push them deep enough.
  2. pushing them deep enough and then deciding to place them before/after the node, is enough to look okay in most cases. which surprised me, but I guess that's what you were saying all along.
  3. (usually) the reason we don't push them deep enough is that I didn't collect all the ranges, and so when we do the "find last" routine, we end up selecting something that is the parent of what we should have actually binded to.
  4. this range-to-node mapping is done with an "ast visitor" I wrote, except that sometimes I forgot to visit something, or sometimes I did visit it, but in the parser we don't define a range for the visited thing.
  5. or maybe none of this is relevant here and it's some other issue.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

my hunch is that in such comma-separated list cases the pushing down deep enough cannot quite do the thing we want, as the comma may not be part of the item (and its range), so you will find the "after a comma" comments associated with the parent, not the list element. The annoying thing is that if we want to keep the comments in the same position after the comma, we also can't place them from within the item tokenizer, we need to insert it after the comma in the parent one. So it's a question of how do we achieve putting them in the right spot given that situation, once we have a solution, it will probably apply in multiple places with such structure.


error dummy file:14:1: Illegal character: ​
error dummy file:18:1: Illegal character: ​
error dummy file:23:1: Illegal character: ​
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's still there in the current diff - is it just an artifact of how you run the formatting on the repos now?

// Summarization by a CVL function. The result is non-deterministic because the CVL function is not deterministic.
function reduceBalance(uint256 amount) internal returns (uint256) with (env e) => cvlReduceBalance(e, amount);
// Summarization by a CVL function. The result is non-deterministic because the CVL function is not deterministic.
function reduceBalance(uint256 amount) internal returns (uint256) with(env e) => cvlReduceBalance(e, amount);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It doesn't have the space here, although you did add it in other occurrences of with now, not sure why

@@ -14,7 +13,7 @@ hook ALL_TSTORE(uint loc, uint v) {
}
}

hook ALL_TLOAD(uint loc) uint v {
hook ALL_TLOAD(uint loc, uint v) {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

again, on the loads I think there's something wrong

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I thought I was being clever by unconditionally inserting all params into a single list and wrapping in parenthesis, but nope.


unresolved external in TrusterLenderPool.flashLoan(uint256,address,address,bytes) => DISPATCH(use_fallback=true) [
token.approve(address, uint256),
unresolved external in TrusterLenderPool.flashLoan(uint256, address, address, bytes) => DISPATCH(use_fallback)[
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

does this work without the =true?
I tried looking in the documentation and it only shows it with optimistic equal true or false, it doesn't even mention use_fallback, so I would not be surprised if it also doesn't list all ways of writing it...

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I fixed this in another file. I'll check this file as well.

Copy link
Author

@pickx pickx Jun 23, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

so, two things:

  1. there was still some more work needed here to get the tokenizer to correctly transform the code and still work after the roundtrip. hopefully now I have finally handled all the edge cases of this niche syntax.
    (EDIT: notice that we have this logic for both "DISPATCH" and "DISPATCHER" and the logic is subtly different for each one...)
  2. yes, this works, and indeed this seems like undocumented syntax. I don't know who is using this or why.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants