Design of Weasel

[Laplace-Demon]

No description provided.

[redianthus]

Why should the function return an i32?

[Laplace-Demon]

It depends on what type we use for prop and how term values get converted to prop. Here the design is to 1. use i32 to encode prop, 2. use pure functions returning i32 as predicates.

[redianthus]

Yes but we could instead allow any function call as long as it is part of an expression returning an i32, for instance call $f = i64.const 42 ?

I'm not opposed to having only function returning an i32. I understand it is easier so it may be better to start like this and relax later if needed, but I just wanted to understand why you wanted such a restriction

[Laplace-Demon]

Oh, my mind went like this:

1. E-ACSL used int for prop
   -> 2. we should use int32 for prop
   -> 3. predicates should have return type i32

But I didn't realize one subtle point : 1. and 2. are only about internal representation, whereas 3. is about external representation.

So, I think it is better (more intuitive) to simply distinguish zero and non-zero numbers when representing prop externally, be it i32 or i64. That is:

Suggested change

	| "call" , ind , { term } ; (the function must return an i32)
	| "call" , ind , { term } ; (the function must return wasm_int_type)

[Laplace-Demon]

I added the pure clause in function contract which indicates the function should pass certain syntactic check to be recognized as a pure function, and is therefore in the scope of weasel function application. It has slight semantic difference with assigns nothing since the latter implies a runtime check via comparing the new and the old values.

In the following week I'll implement what's currently in the grammar. That involves the so-called "interval inference" (computing the smallest accommodatable numerical type), but also some type checking work, because:

• Weasel operators are polymorphic. They may be: 1. meaningful only on machine integers, 2. meaningful on machine integers and mathematical integers, 3. meaningful on machine integers, mathematical integers, and floating-point numbers, 4. meaningful only on floating-point numbers. So we need to validate Weasel expressions.
• Weasel propositions are also embedded in numerical types, say i32, and extra rules need to be introduced to specify the interaction between prop and term of type i32. My plan is to make clear distinction between them, except in logical predicates where i32 may be implicitly cast to prop.

[redianthus]

I added the pure clause in function contract which indicates the function should pass certain syntactic check to be recognized as a pure function, and is therefore in the scope of weasel function application. It has slight semantic difference with assigns nothing since the latter implies a runtime check via comparing the new and the old values.

Is this really needed? The way I understand this is : if a function is used in a contract, it must be pure. So we check it has the pure attribute, and in a separate phase, we check that every function with the pure attribute is actually pure.

Instead, we could simply check that every function used in a contract is pure directly, without going through an attribute (it may be useful for Owi to have this information anyway, even out of the Weasel context).

Weasel operators are polymorphic. They may be: 1. meaningful only on machine integers, 2. meaningful on machine integers and mathematical integers, 3. meaningful on machine integers, mathematical integers, and floating-point numbers, 4. meaningful only on floating-point numbers. So we need to validate Weasel expressions.

Makes sense.

Weasel propositions are also embedded in numerical types, say i32, and extra rules need to be introduced to specify the interaction between prop and term of type i32. My plan is to make clear distinction between them, except in logical predicates where i32 may be implicitly cast to prop.

Makes sense too. :)

[Laplace-Demon]

Is this really needed? The way I understand this is : if a function is used in a contract, it must be pure. So we check it has the pure attribute, and in a separate phase, we check that every function with the pure attribute is actually pure.

Instead, we could simply check that every function used in a contract is pure directly, without going through an attribute (it may be useful for Owi to have this information anyway, even out of the Weasel context).

Well, it's simply because Gospel has pure annotation so I had a path dependence :D As you said, both will work. But the way I was thinking about is in another direction: pure first registers one function in Weasel, so that Weasel can recognize it in expression.

One argument favoring pure can be: it might be desirable to distinguish Weasel scope and Wasm scope? The logical functions/predicates needed in annotation do not always exist in the code so it's likely that we need to define them, and a registration mechanism helps to reuse logical functions/predicates across several files. Consequently, this approach actually resembles writing logical functions/predicates directly in annotations.