https://github.com/mit-plv/fiat-crypto
Revision 32b3d8f86987f3622c19f7c5d1b948767ac80cea authored by jadep on 28 July 2020, 11:34:51 UTC, committed by jadep on 28 July 2020, 11:34:51 UTC
1 parent 1823a19
Tip revision: 32b3d8f86987f3622c19f7c5d1b948767ac80cea authored by jadep on 28 July 2020, 11:34:51 UTC
add length/eval lemmas so build works, fix up comments
add length/eval lemmas so build works, fix up comments
Tip revision: 32b3d8f
Crypto.Fancy.Montgomery256.montred256.expected
Montgomery256.montred256 =
fun var : API.type -> Type =>
λ x x0 : var (type.base (base.type.type_base Z)),
expr_let v := #ident_Z_cast @ ###uint256 @
(#ident_fancy_mulhl @
(###256,
(#ident_Z_cast @ ###uint256 @ $x,
###115792089210356248768974548684794254293921932838497980611635986753331132366849))) in
expr_let v0 := #ident_Z_cast @ ###uint256 @
(#ident_fancy_mullh @
(###256,
(#ident_Z_cast @ ###uint256 @ $x,
###115792089210356248768974548684794254293921932838497980611635986753331132366849))) in
expr_let v1 := #ident_Z_cast @ ###uint256 @
(#ident_fancy_mulll @
(###256,
(#ident_Z_cast @ ###uint256 @ $x,
###115792089210356248768974548684794254293921932838497980611635986753331132366849))) in
expr_let v2 := #ident_Z_cast2 @ (###uint256, ###r[0 ~> 1]) @
(#ident_fancy_add @
(###256, ###128,
(#ident_Z_cast @ ###uint256 @ $v1,
#ident_Z_cast @ ###uint256 @ $v0))) in
expr_let v3 := #ident_Z_cast2 @ (###uint256, ###r[0 ~> 1]) @
(#ident_fancy_add @
(###256, ###128,
(#ident_Z_cast @ ###uint256 @
(#ident_fst @
(#ident_Z_cast2 @ (###uint256, ###r[0 ~> 1]) @ $v2)),
#ident_Z_cast @ ###uint256 @ $v))) in
expr_let v4 := #ident_Z_cast @ ###uint256 @
(#ident_fancy_mulll @
(###256,
(###115792089210356248762697446949407573530086143415290314195533631308867097853951,
#ident_Z_cast @ ###uint256 @
(#ident_fst @
(#ident_Z_cast2 @ (###uint256, ###r[0 ~> 1]) @ $v3))))) in
expr_let v5 := #ident_Z_cast @ ###uint256 @
(#ident_fancy_mullh @
(###256,
(###115792089210356248762697446949407573530086143415290314195533631308867097853951,
#ident_Z_cast @ ###uint256 @
(#ident_fst @
(#ident_Z_cast2 @ (###uint256, ###r[0 ~> 1]) @ $v3))))) in
expr_let v6 := #ident_Z_cast @ ###uint256 @
(#ident_fancy_mulhl @
(###256,
(###115792089210356248762697446949407573530086143415290314195533631308867097853951,
#ident_Z_cast @ ###uint256 @
(#ident_fst @
(#ident_Z_cast2 @ (###uint256, ###r[0 ~> 1]) @ $v3))))) in
expr_let v7 := #ident_Z_cast @ ###uint256 @
(#ident_fancy_mulhh @
(###256,
(###115792089210356248762697446949407573530086143415290314195533631308867097853951,
#ident_Z_cast @ ###uint256 @
(#ident_fst @
(#ident_Z_cast2 @ (###uint256, ###r[0 ~> 1]) @ $v3))))) in
expr_let v8 := #ident_Z_cast2 @ (###uint256, ###r[0 ~> 1]) @
(#ident_fancy_add @
(###256, ###128,
(#ident_Z_cast @ ###uint256 @ $v4,
#ident_Z_cast @ ###uint256 @ $v6))) in
expr_let v9 := #ident_Z_cast2 @ (###uint256, ###r[0 ~> 1]) @
(#ident_fancy_addc @
(###256, ###(-128),
(#ident_Z_cast @ ###r[0 ~> 1] @
(#ident_snd @
(#ident_Z_cast2 @ (###uint256, ###r[0 ~> 1]) @ $v8)),
#ident_Z_cast @ ###uint256 @ $v7,
#ident_Z_cast @ ###uint256 @ $v6))) in
expr_let v10 := #ident_Z_cast2 @ (###uint256, ###r[0 ~> 1]) @
(#ident_fancy_add @
(###256, ###128,
(#ident_Z_cast @ ###uint256 @
(#ident_fst @
(#ident_Z_cast2 @ (###uint256, ###r[0 ~> 1]) @ $v8)),
#ident_Z_cast @ ###uint256 @ $v5))) in
expr_let v11 := #ident_Z_cast2 @ (###uint256, ###r[0 ~> 1]) @
(#ident_fancy_addc @
(###256, ###(-128),
(#ident_Z_cast @ ###r[0 ~> 1] @
(#ident_snd @
(#ident_Z_cast2 @ (###uint256, ###r[0 ~> 1]) @ $v10)),
#ident_Z_cast @ ###uint256 @
(#ident_fst @
(#ident_Z_cast2 @ (###uint256, ###r[0 ~> 1]) @ $v9)),
#ident_Z_cast @ ###uint256 @ $v5))) in
expr_let v12 := #ident_Z_cast2 @ (###uint256, ###r[0 ~> 1]) @
(#ident_fancy_add @
(###256, ###0,
(#ident_Z_cast @ ###uint256 @ $x,
#ident_Z_cast @ ###uint256 @
(#ident_fst @
(#ident_Z_cast2 @ (###uint256, ###r[0 ~> 1]) @ $v10))))) in
expr_let v13 := #ident_Z_cast2 @ (###uint256, ###r[0 ~> 1]) @
(#ident_fancy_addc @
(###256, ###0,
(#ident_Z_cast @ ###r[0 ~> 1] @
(#ident_snd @
(#ident_Z_cast2 @ (###uint256, ###r[0 ~> 1]) @ $v12)),
#ident_Z_cast @ ###uint256 @ $x0,
#ident_Z_cast @ ###uint256 @
(#ident_fst @
(#ident_Z_cast2 @ (###uint256, ###r[0 ~> 1]) @ $v11))))) in
expr_let v14 := #ident_Z_cast @ ###uint256 @
(#ident_fancy_selc @
(#ident_Z_cast @ ###r[0 ~> 1] @
(#ident_snd @
(#ident_Z_cast2 @ (###uint256, ###r[0 ~> 1]) @ $v13)),
###0,
###115792089210356248762697446949407573530086143415290314195533631308867097853951)) in
expr_let v15 := #ident_Z_cast2 @ (###uint256, ###r[0 ~> 1]) @
(#ident_fancy_sub @
(###256, ###0,
(#ident_Z_cast @ ###uint256 @
(#ident_fst @
(#ident_Z_cast2 @ (###uint256, ###r[0 ~> 1]) @ $v13)),
#ident_Z_cast @ ###uint256 @ $v14))) in
expr_let v16 := #ident_Z_cast @ ###uint256 @
(#ident_fancy_addm @
(#ident_Z_cast @ ###uint256 @
(#ident_fst @
(#ident_Z_cast2 @ (###uint256, ###r[0 ~> 1]) @ $v15)),
###0,
###115792089210356248762697446949407573530086143415290314195533631308867097853951)) in
#ident_Z_cast @ ###uint256 @ $v16
: API.Expr
(type.base (base.type.type_base Z) ->
type.base (base.type.type_base Z) ->
type.base (base.type.type_base Z))
Computing file changes ...
