1
0
Fork 0
mirror of synced 2025-09-23 12:18:44 +00:00

more tests

This commit is contained in:
dark64 2022-11-22 20:32:49 +01:00
parent 65ea034520
commit fd361d68f3
14 changed files with 173 additions and 27 deletions

View file

@ -400,6 +400,7 @@ impl<'ast, 'a, T: Field> ResultFolder<'ast, T> for Propagator<'ast, 'a, T> {
true => { true => {
let r: Option<TypedExpression<'ast, T>> = match embed_call.embed { let r: Option<TypedExpression<'ast, T>> = match embed_call.embed {
FlatEmbed::FieldToBoolUnsafe => Ok(None), // todo FlatEmbed::FieldToBoolUnsafe => Ok(None), // todo
FlatEmbed::BoolToField => Ok(None), // todo
FlatEmbed::BitArrayLe => Ok(None), // todo FlatEmbed::BitArrayLe => Ok(None), // todo
FlatEmbed::U64FromBits => Ok(Some(process_u_from_bits( FlatEmbed::U64FromBits => Ok(Some(process_u_from_bits(
&embed_call.arguments, &embed_call.arguments,

View file

@ -32,6 +32,7 @@ cfg_if::cfg_if! {
#[derive(Debug, Clone, PartialEq, Eq, Hash, Copy, PartialOrd, Ord, Serialize, Deserialize)] #[derive(Debug, Clone, PartialEq, Eq, Hash, Copy, PartialOrd, Ord, Serialize, Deserialize)]
pub enum FlatEmbed { pub enum FlatEmbed {
FieldToBoolUnsafe, FieldToBoolUnsafe,
BoolToField,
BitArrayLe, BitArrayLe,
Unpack, Unpack,
U8ToBits, U8ToBits,
@ -54,6 +55,9 @@ impl FlatEmbed {
FlatEmbed::FieldToBoolUnsafe => UnresolvedSignature::new() FlatEmbed::FieldToBoolUnsafe => UnresolvedSignature::new()
.inputs(vec![UnresolvedType::FieldElement.into()]) .inputs(vec![UnresolvedType::FieldElement.into()])
.output(UnresolvedType::Boolean.into()), .output(UnresolvedType::Boolean.into()),
FlatEmbed::BoolToField => UnresolvedSignature::new()
.inputs(vec![UnresolvedType::Boolean.into()])
.output(UnresolvedType::FieldElement.into()),
FlatEmbed::BitArrayLe => UnresolvedSignature::new() FlatEmbed::BitArrayLe => UnresolvedSignature::new()
.generics(vec![ConstantGenericNode::mock("N")]) .generics(vec![ConstantGenericNode::mock("N")])
.inputs(vec![ .inputs(vec![
@ -193,6 +197,9 @@ impl FlatEmbed {
FlatEmbed::FieldToBoolUnsafe => DeclarationSignature::new() FlatEmbed::FieldToBoolUnsafe => DeclarationSignature::new()
.inputs(vec![DeclarationType::FieldElement]) .inputs(vec![DeclarationType::FieldElement])
.output(DeclarationType::Boolean), .output(DeclarationType::Boolean),
FlatEmbed::BoolToField => DeclarationSignature::new()
.inputs(vec![DeclarationType::Boolean])
.output(DeclarationType::FieldElement),
FlatEmbed::BitArrayLe => DeclarationSignature::new() FlatEmbed::BitArrayLe => DeclarationSignature::new()
.generics(vec![Some(DeclarationConstant::Generic( .generics(vec![Some(DeclarationConstant::Generic(
GenericIdentifier::with_name("N").with_index(0), GenericIdentifier::with_name("N").with_index(0),
@ -300,6 +307,7 @@ impl FlatEmbed {
pub fn id(&self) -> &'static str { pub fn id(&self) -> &'static str {
match self { match self {
FlatEmbed::FieldToBoolUnsafe => "_FIELD_TO_BOOL_UNSAFE", FlatEmbed::FieldToBoolUnsafe => "_FIELD_TO_BOOL_UNSAFE",
FlatEmbed::BoolToField => "_BOOL_TO_FIELD",
FlatEmbed::BitArrayLe => "_BIT_ARRAY_LT", FlatEmbed::BitArrayLe => "_BIT_ARRAY_LT",
FlatEmbed::Unpack => "_UNPACK", FlatEmbed::Unpack => "_UNPACK",
FlatEmbed::U8ToBits => "_U8_TO_BITS", FlatEmbed::U8ToBits => "_U8_TO_BITS",

View file

@ -12,13 +12,7 @@ All constraints must be enclosed within an `asm` block. In an assembly block we
Assigning a value, in general, should be combined with adding a constraint: Assigning a value, in general, should be combined with adding a constraint:
```zok ```zok
def main(field a, field b) { {{#include ../../../zokrates_cli/examples/book/assembly/division.zok}}
field mut c = 0;
asm {
c <-- a / b;
a === b * c;
}
}
``` ```
> The operator `<--` can be sometimes misused, as this operator does not generate any constraints, resulting in unconstrained variables in the constraint system. > The operator `<--` can be sometimes misused, as this operator does not generate any constraints, resulting in unconstrained variables in the constraint system.
@ -77,18 +71,7 @@ Assembly is a low-level part of the compiler which does not have type safety. In
This call is unsafe because it is the responsibility of the user to constrain the field input: This call is unsafe because it is the responsibility of the user to constrain the field input:
```zok ```zok
from "EMBED" import field_to_bool_unsafe; {{#include ../../../zokrates_cli/examples/book/assembly/field_to_bool.zok}}
def main(field x) -> bool {
// we constrain `x` to be 0 or 1
asm {
x * (x - 1) === 0;
}
// we can treat `x` as `bool` afterwards, as we constrained it properly
// `field_to_bool_unsafe` call does not produce any extra constraints
bool out = field_to_bool_unsafe(x);
return out;
}
``` ```
### bool_to_field ### bool_to_field
@ -96,12 +79,5 @@ def main(field x) -> bool {
This call is safe as `bool` types are constrained by the compiler: This call is safe as `bool` types are constrained by the compiler:
```zok ```zok
from "EMBED" import bool_to_field; {{#include ../../../zokrates_cli/examples/book/assembly/bool_to_field.zok}}
def main(bool x) -> field {
// `x` is constrained by the compiler automatically so we can safely
// treat it as `field` with no extra cost
field out = bool_to_field(x);
return out;
}
``` ```

View file

@ -0,0 +1,8 @@
from "EMBED" import bool_to_field;
def main(bool x) -> field {
// `x` is constrained by the compiler automatically so we can safely
// treat it as `field` with no extra cost
field out = bool_to_field(x);
return out;
}

View file

@ -0,0 +1,7 @@
def main(field a, field b) {
field mut c = 0;
asm {
c <-- a / b;
a === b * c;
}
}

View file

@ -0,0 +1,12 @@
from "EMBED" import field_to_bool_unsafe;
def main(field x) -> bool {
// we constrain `x` to be 0 or 1
asm {
x * (x - 1) === 0;
}
// we can treat `x` as `bool` afterwards, as we constrained it properly
// `field_to_bool_unsafe` call does not produce any extra constraints
bool out = field_to_bool_unsafe(x);
return out;
}

View file

@ -1050,6 +1050,7 @@ impl<'ast, T: Field> Flattener<'ast, T> {
match embed { match embed {
FlatEmbed::FieldToBoolUnsafe => vec![params.pop().unwrap()], FlatEmbed::FieldToBoolUnsafe => vec![params.pop().unwrap()],
FlatEmbed::BoolToField => vec![params.pop().unwrap()],
FlatEmbed::U8ToBits => self.u_to_bits(params.pop().unwrap(), 8.into()), FlatEmbed::U8ToBits => self.u_to_bits(params.pop().unwrap(), 8.into()),
FlatEmbed::U16ToBits => self.u_to_bits(params.pop().unwrap(), 16.into()), FlatEmbed::U16ToBits => self.u_to_bits(params.pop().unwrap(), 16.into()),
FlatEmbed::U32ToBits => self.u_to_bits(params.pop().unwrap(), 32.into()), FlatEmbed::U32ToBits => self.u_to_bits(params.pop().unwrap(), 32.into()),

View file

@ -151,6 +151,10 @@ impl Importer {
id: symbol.get_alias(), id: symbol.get_alias(),
symbol: Symbol::Flat(FlatEmbed::FieldToBoolUnsafe), symbol: Symbol::Flat(FlatEmbed::FieldToBoolUnsafe),
}, },
"bool_to_field" => SymbolDeclaration {
id: symbol.get_alias(),
symbol: Symbol::Flat(FlatEmbed::BoolToField),
},
"bit_array_le" => SymbolDeclaration { "bit_array_le" => SymbolDeclaration {
id: symbol.get_alias(), id: symbol.get_alias(),
symbol: Symbol::Flat(FlatEmbed::BitArrayLe), symbol: Symbol::Flat(FlatEmbed::BitArrayLe),

View file

@ -0,0 +1,36 @@
{
"curves": ["Bn128"],
"max_constraint_count": 7,
"tests": [
{
"input": {
"values": ["2", "2"]
},
"output": {
"Ok": {
"value": false
}
}
},
{
"input": {
"values": ["4", "2"]
},
"output": {
"Ok": {
"value": false
}
}
},
{
"input": {
"values": ["2", "4"]
},
"output": {
"Ok": {
"value": true
}
}
}
]
}

View file

@ -0,0 +1,14 @@
from "EMBED" import field_to_bool_unsafe;
from "field" import FIELD_SIZE_IN_BITS;
from "./bitify" import bitify;
def less_than<N>(field a, field b) -> bool {
assert(N < FIELD_SIZE_IN_BITS - 1);
field[N + 1] bits = bitify(a + (1f << N) - b);
bool out = field_to_bool_unsafe(1 - bits[N]);
return out;
}
def main(field a, field b) -> bool {
return less_than::<4>(a, b);
}

View file

@ -0,0 +1,26 @@
{
"curves": ["Bn128"],
"max_constraint_count": 2,
"tests": [
{
"input": {
"values": [false]
},
"output": {
"Ok": {
"value": "0"
}
}
},
{
"input": {
"values": [true]
},
"output": {
"Ok": {
"value": "1"
}
}
}
]
}

View file

@ -0,0 +1,6 @@
from "EMBED" import bool_to_field;
def main(bool x) -> field {
field out = bool_to_field(x);
return out;
}

View file

@ -0,0 +1,38 @@
{
"curves": ["Bn128"],
"max_constraint_count": 2,
"tests": [
{
"input": {
"values": ["0"]
},
"output": {
"Ok": {
"value": false
}
}
},
{
"input": {
"values": ["1"]
},
"output": {
"Ok": {
"value": true
}
}
},
{
"input": {
"values": ["2"]
},
"output": {
"Err": {
"UnsatisfiedConstraint": {
"error": "UserConstraint"
}
}
}
}
]
}

View file

@ -0,0 +1,9 @@
from "EMBED" import field_to_bool_unsafe;
def main(field x) -> bool {
asm {
x * (x - 1) === 0;
}
bool out = field_to_bool_unsafe(x);
return out;
}