Skip to content
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

[Feature] Enable cast.lossy for all literal types. #2273

Merged
merged 3 commits into from
Jan 9, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions circuit/program/src/data/literal/cast/integer.rs
Original file line number Diff line number Diff line change
Expand Up @@ -79,7 +79,7 @@ impl<E: Environment, I0: IntegerType, I1: IntegerType> Cast<Integer<E, I1>> for
// Then instantiate the new integer from the lower bits.
false => {
Boolean::assert_bits_are_zero(&bits_le[(I1::BITS.saturating_sub(1) as usize)..]);
Integer::<E, I1>::from_bits_le(&bits_le[..(I1::BITS.saturating_sub(1) as usize)])
Integer::<E, I1>::from_bits_le(&bits_le[..(I1::BITS as usize)])
}
},
// If the source type is signed and the destination type is unsigned, perform the required checks.
Expand All @@ -88,7 +88,7 @@ impl<E: Environment, I0: IntegerType, I1: IntegerType> Cast<Integer<E, I1>> for
// Then instantiate the new integer from the lower bits.
true => {
E::assert(!&bits_le[I0::BITS.saturating_sub(1) as usize]);
Integer::<E, I1>::from_bits_le(&bits_le[..(I0::BITS.saturating_sub(1) as usize)])
Integer::<E, I1>::from_bits_le(&bits_le)
}
// If the source type is larger than the destination type, check that the upper bits are zero.
// Then instantiate the new integer from the lower bits.
Expand Down
22 changes: 21 additions & 1 deletion synthesizer/process/src/stack/finalize_types/initialize.rs
Original file line number Diff line number Diff line change
Expand Up @@ -581,7 +581,27 @@ impl<N: Network> FinalizeTypes<N> {
}
}
}
"cast.lossy" => bail!("Instruction '{instruction}' is not supported yet."),
"cast.lossy" => {
// Retrieve the cast operation.
let operation = match instruction {
Instruction::CastLossy(operation) => operation,
_ => bail!("Instruction '{instruction}' is not a cast.lossy operation."),
};

// Ensure the instruction has one destination register.
ensure!(
instruction.destinations().len() == 1,
"Instruction '{instruction}' has multiple destinations."
);

// Ensure the casted register type is valid and defined.
match operation.cast_type() {
CastType::Plaintext(PlaintextType::Literal(_)) => {
ensure!(instruction.operands().len() == 1, "Expected 1 operand.");
}
_ => bail!("`cast.lossy` is only supported for casting to a literal type."),
}
}
_ => bail!("Instruction '{instruction}' is not for opcode '{opcode}'."),
},
Opcode::Command(opcode) => {
Expand Down
22 changes: 21 additions & 1 deletion synthesizer/process/src/stack/register_types/initialize.rs
Original file line number Diff line number Diff line change
Expand Up @@ -540,7 +540,27 @@ impl<N: Network> RegisterTypes<N> {
}
}
}
"cast.lossy" => bail!("Instruction '{instruction}' is not supported yet."),
"cast.lossy" => {
// Retrieve the cast operation.
let operation = match instruction {
Instruction::CastLossy(operation) => operation,
_ => bail!("Instruction '{instruction}' is not a cast.lossy operation."),
};

// Ensure the instruction has one destination register.
ensure!(
instruction.destinations().len() == 1,
"Instruction '{instruction}' has multiple destinations."
);

// Ensure the casted register type is valid and defined.
match operation.cast_type() {
CastType::Plaintext(PlaintextType::Literal(_)) => {
ensure!(instruction.operands().len() == 1, "Expected 1 operand.");
}
_ => bail!("`cast.lossy` is only supported for casting to a literal type."),
}
}
_ => bail!("Instruction '{instruction}' is not for opcode '{opcode}'."),
},
Opcode::Command(opcode) => {
Expand Down
29 changes: 23 additions & 6 deletions synthesizer/program/src/logic/instruction/operation/cast.rs
Original file line number Diff line number Diff line change
Expand Up @@ -206,9 +206,12 @@ impl<N: Network, const VARIANT: u8> CastOperation<N, VARIANT> {
stack: &(impl StackMatches<N> + StackProgram<N>),
registers: &mut (impl RegistersSigner<N> + RegistersLoad<N> + RegistersStore<N>),
) -> Result<()> {
// TODO (howardwu & d0cd): Re-enable after stabilizing.
// If the variant is `cast.lossy`, then check that the `cast_type` is a `PlaintextType::Literal`.
if VARIANT == CastVariant::CastLossy as u8 {
bail!("cast.lossy is not supported (yet)")
ensure!(
matches!(self.cast_type, CastType::Plaintext(PlaintextType::Literal(..))),
"`cast.lossy` is only supported for casting to a literal type"
)
}

// Load the operands values.
Expand Down Expand Up @@ -333,9 +336,12 @@ impl<N: Network, const VARIANT: u8> CastOperation<N, VARIANT> {
stack: &(impl StackMatches<N> + StackProgram<N>),
registers: &mut (impl RegistersSignerCircuit<N, A> + RegistersLoadCircuit<N, A> + RegistersStoreCircuit<N, A>),
) -> Result<()> {
// TODO (howardwu & d0cd): Re-enable after stabilizing.
// If the variant is `cast.lossy`, then check that the `cast_type` is a `PlaintextType::Literal`.
if VARIANT == CastVariant::CastLossy as u8 {
bail!("cast.lossy is not supported (yet)")
ensure!(
matches!(self.cast_type, CastType::Plaintext(PlaintextType::Literal(..))),
"`cast.lossy` is only supported for casting to a literal type"
)
}

use circuit::{Eject, Inject};
Expand Down Expand Up @@ -582,9 +588,12 @@ impl<N: Network, const VARIANT: u8> CastOperation<N, VARIANT> {
stack: &(impl StackMatches<N> + StackProgram<N>),
registers: &mut (impl RegistersLoad<N> + RegistersStore<N>),
) -> Result<()> {
// TODO (howardwu & d0cd): Re-enable after stabilizing.
// If the variant is `cast.lossy`, then check that the `cast_type` is a `PlaintextType::Literal`.
if VARIANT == CastVariant::CastLossy as u8 {
bail!("cast.lossy is not supported (yet)")
ensure!(
matches!(self.cast_type, CastType::Plaintext(PlaintextType::Literal(..))),
"`cast.lossy` is only supported for casting to a literal type"
)
}

// Load the operands values.
Expand Down Expand Up @@ -641,6 +650,14 @@ impl<N: Network, const VARIANT: u8> CastOperation<N, VARIANT> {
stack: &impl StackProgram<N>,
input_types: &[RegisterType<N>],
) -> Result<Vec<RegisterType<N>>> {
// If the variant is `cast.lossy`, then check that the `cast_type` is a `PlaintextType::Literal`.
if VARIANT == CastVariant::CastLossy as u8 {
ensure!(
matches!(self.cast_type, CastType::Plaintext(PlaintextType::Literal(..))),
"`cast.lossy` is only supported for casting to a literal type"
)
}

// Ensure the number of operands is correct.
ensure!(
input_types.len() == self.operands.len(),
Expand Down
62 changes: 62 additions & 0 deletions synthesizer/tests/expectations/process/execute/lossy_casts.out
Original file line number Diff line number Diff line change
@@ -0,0 +1,62 @@
errors: []
outputs:
- - 93754672984613362290390329026198290544u128
- 93754672984613362290390329026198290544i128
- 16982649547548967024u64
- -1464094526160584592i64
- 446349424u32
- 446349424i32
- 49264u16
- -16272i16
- 112u8
- 112i8
- 'false'
- 4764330560507562969049837239139509827871889319573451509694277586124473432540group
- - 0u128
- 0i128
- 0u64
- 0i64
- 0u32
- 0i32
- 0u16
- 0i16
- 0u8
- 0i8
- 'false'
- 0group
- - 1u128
- 1i128
- 1u64
- 1i64
- 1u32
- 1i32
- 1u16
- 1i16
- 1u8
- 1i8
- 'true'
- 1540945439182663264862696551825005342995406165131907382295858612069623286213group
- - 0u128
- 0i128
- 0u64
- 0i64
- 0u32
- 0i32
- 0u16
- 0i16
- 0u8
- 0i8
- 'false'
- 340282366920938463463374607431768211456group
- - 1u128
- 1i128
- 1u64
- 1i64
- 1u32
- 1i32
- 1u16
- 1i16
- 1u8
- 1i8
- 'true'
- 2207376757013908562861143127796680436121374163712359508096962653679714303999group
50 changes: 50 additions & 0 deletions synthesizer/tests/tests/process/execute/lossy_casts.aleo
Original file line number Diff line number Diff line change
@@ -0,0 +1,50 @@
/*
randomness: 902384
cases:
- program: lossy_casts.aleo
function: test_lossy_cast
inputs: [79363714989903307245735717098563574705733591463163614225748337416674727625843187853442697973404985688481508350822field]
- program: lossy_casts.aleo
function: test_lossy_cast
inputs: [0field]
- program: lossy_casts.aleo
function: test_lossy_cast
inputs: [1field]
- program: lossy_casts.aleo
function: test_lossy_cast
inputs: [340_282_366_920_938_463_463_374_607_431_768_211_456field]
- program: lossy_casts.aleo
function: test_lossy_cast
inputs: [340_282_366_920_938_463_463_374_607_431_768_211_457field]


*/

program lossy_casts.aleo;

function test_lossy_cast:
input r0 as field.private;
cast.lossy r0 into r1 as u128;
cast.lossy r0 into r2 as i128;
cast.lossy r0 into r3 as u64;
cast.lossy r0 into r4 as i64;
cast.lossy r0 into r5 as u32;
cast.lossy r0 into r6 as i32;
cast.lossy r0 into r7 as u16;
cast.lossy r0 into r8 as i16;
cast.lossy r0 into r9 as u8;
cast.lossy r0 into r10 as i8;
cast.lossy r0 into r11 as boolean;
cast.lossy r0 into r12 as group;
output r1 as u128.private;
output r2 as i128.private;
output r3 as u64.private;
output r4 as i64.private;
output r5 as u32.private;
output r6 as i32.private;
output r7 as u16.private;
output r8 as i16.private;
output r9 as u8.private;
output r10 as i8.private;
output r11 as boolean.private;
output r12 as group.private;